[emmab]

> Formal Verification: Get an absolute 100% guarantee that your contracts are free of errors

This is not actually possible, there could have been an issue with your threat model. e.g. side-channel attacks could be out of scope.

[bpicolo]

Formal verification only ever verifies as far as your spec specifies

[mannykannot]

That is true, but it should not be assumed that a spec. is a thing of fixed validity. A formal spec. has a reasonable likelihood of being less ambiguous, incomplete or self-contradictory than an informal one, or whatever substitutes for a spec. in an agile approach.

[masklinn]

That only tells me a spec and its formal verification are necessary but not sufficient assets. Not "we can't prove everything so we'll keep our millions riding on half-assed piles of garbage.