←back to thread

Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods

(queue.acm.org)
167 points yarapavan | 1 comments | 01 Apr 25 14:59 UTC | HN request time: 0s | source
Show context
gqgs ◴[01 Apr 25 19:17 UTC] No.43550402[source]▶
A key concern I've consistently had regarding formal verification systems is: how does one confirm the accuracy of the verifier itself?

This issue appears to present an intrinsically unsolvable problem, implying that a formally verified system could still contain bugs due to potential issues in the verification software.

While this perspective doesn't necessarily render formal verification impractical, it does introduce certain caveats that, in my experience, are not frequently addressed in discussions about these systems.

replies(8): >>43550610 #>>43550706 #>>43550740 #>>43552467 #>>43553529 #>>43553826 #>>43554265 #>>43558410 #
1. newAccount2025 ◴[01 Apr 25 23:51 UTC] No.43552467[source]▶
A deeply considered take: this is theoretically interesting but in practice matters very little.

It’s like worrying about compiler bugs instead of semantic programming errors. If you are getting to the point where you have machine checked proofs, you are already doing great. It’s way more likely that you have a specification bug or modeling error than an error in the solver.

If you are worried about it, many people have solutions that are very compelling. There are LCF style theorem provers like HOL Light with tiny kernels. But for any real world systems, none of this matters, use any automated solvers you like, it will be fine.