←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: 0.2s | 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. trenchgun ◴[02 Apr 25 16:24 UTC] No.43558410[source]▶
Verifiers can be based on a small proven kernel. That is not really the issue.

The issue is writing the formal specification. Formal verification is in nutshell just proving the equivalence of two different formal constructs: one that is called the spec and one that is called the system (or program). Writing specs is hard.