[twinkletwinkle]

Formal verification all the way down.

I'm a complete layman in this field, but mustn't it bump against the Incompleteness Theorem at some point? There's no way to prove your definitions.

[progman]

The critical point is specification vs. implementation. Any difference creates a loophole which can be abused.