This. In my very limited experience (i didn't write the code or specs), I've seen the runtime code find more bugs in the formal specs than the formal specs finding bugs in the runtime code.