[heavenlyblue]

Then it means that they had to formally verify the specification itself.

It’s not that hard by the way. And they did that, but handwaved the critique - the typical approach of “my guts are probably more correct than maths”.

[nicoburns]

Formal verificatiom can't tell you if you're assumptions are off. It can only work from those assumptions.