6 hours ago
- Formal methods are divided into formal specification (writing precise specs) and formal verification (proving correctness), with further splits into code and design domains.
- Code verification is difficult and costly, historically relying on manual proofs, with progress through SMT solvers like Z3, but full verification remains slow (e.g., ~4 lines/day).
- Partial code verification (e.g., proving no crashes) is more practical and can be embedded in type systems (e.g., Rust for memory safety).
- Design verification is easier than code verification, often using model checkers to brute-force state spaces, but faces cultural resistance and lack of perceived value.
- Key barriers include the difficulty of proofs, the challenge of validating specs against user needs, and social reluctance to adopt non-code artifacts.
- Many high-assurance techniques (e.g., Cleanroom) achieve near-perfect software without full formal verification, making it unnecessary for most industry use.