Hacker News Reader

> 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.

View on HN

Formal verification only ever verifies as far as your spec specifies

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.

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.

Reply on news.ycombinator.com