From my understanding, NICTA's proofs are basically algorithms to show that Haskell models and C code is equivalent. They can then go on to do proofs with their Haskell models.