Three ways formally verified code can go wrong in practice
18 hours ago
- #programming
- #correctness
- #formal verification
- Formally verified code can still have bugs due to invalid proofs, incorrect properties, or wrong assumptions.
- A proof is invalid if the theorem prover has a bug or if shortcuts in the proof are left unchecked.
- Properties can be wrong if the specification is incomplete, too hard to prove, or misaligned with actual requirements.
- Assumptions can be wrong if environmental factors change or if verified code depends on unverified components.
- Understanding what 'correct' means in formal verification is crucial to avoid miscommunication and misuse of proven code.