Blog :: What I've Learned About Formal Methods In Half a Year

formal-methodssoftware-verificationmodel-checkingtheorem-provinglean

Abstraction: Practical introduction to formal methods via model checking and theorem proving

Key points:

Lightweight formal methods (Alloy/Forge): model properties as predicates, translate to SAT/SMT, exhaustively check bounded state spaces; used for system modeling and access-control policy analysis (Margrave)
Heavyweight formal methods (Lean, Isabelle, Coq): dependent-typed proof assistants where proofs are programs; no automatic proof search in general
seL4 microkernel proved fully correct using Isabelle/HOL — specification, C implementation, and GCC compilation all verified
SAT is NP-complete; SMT generalizes to integers/bit-vectors (Z3 is an SMT solver); Alloy/Forge translate specs to SAT instances
Cloud providers (Amazon, Microsoft) actively recruiting formal methods researchers away from academia
If the specification itself is wrong, verification is worthless ("FM is useless if your spec is bad")

Connections: Z3 · Lean Prover · Formal Methods · Formal Verification · Model Checking