Skip to content

Software Quality

Theorem proving

Theorem proving establishes that a program meets a specification by machine-checked proof. The proof is itself a piece of code (in Coq, Lean, Isabelle, F*, or Dafny). In Coq, Lean and Isabelle a small kernel is what is trusted; everything else is checked against the kernel's rules. The result is the strongest guarantee on the verification spectrum: a verified program cannot violate the proven property under the assumed semantics. The cost is also the highest.

What it catches

  • Wrong-code bugs in verified components. About six CPU-years of Csmith testing found no wrong-code bugs in the CompCert verified compiler's middle-end (Yang et al. 2011)1.
  • Memory-safety, functional-correctness, and security properties. Once proved, the bug class is gone — not tested for and not found.
  • Spec/implementation disagreement that no testing pipeline can find. A refinement proof forces every gap between the code and its spec to surface as an unmet obligation.
  • Cross-implementation correctness for crypto. Fiat-Crypto's proof eliminates an entire class of arithmetic-correctness bugs (timing-side-channel safety is separate — it comes from the generated code being constant-time, not from the proof).

Theorem proving does not catch bugs outside the spec. A verified-correct implementation of a wrong spec is verified against the wrong thing. This is the spec-gap risk and it is the operative limit on the technique.

Tools

Interactive proof assistants

  • Coq / Rocq — a general-purpose proof assistant; the basis for a large body of verified systems software, including CompCert (Leroy 2009)2, CertiKOS, and Fiat-Crypto (Erbsen et al. 2019)3.
  • Lean 4 — a proof assistant whose dependent-type foundation suits both mathematics and program verification; mathlib4 is a large library of formalized mathematics.
  • Isabelle/HOL — the seL4 specification language; the C kernel was refined against a HOL spec (Klein et al. 2009)4.
  • Agda — dependently typed; used more in teaching than in production.

SMT-assisted, semi-automated

  • Dafny — verification-oriented language; SMT-backed; used for the AWS encryption SDK.
  • F* — dependent types + SMT; Project Everest's verified TLS stack and QUIC packet encryption.
  • Verus — Rust-flavored verification language; SMT-backed; a research project aimed at making proof-carrying Rust ergonomic.
  • Why3 — multi-prover frontend; dispatches goals to Coq, Alt-Ergo, Z3, CVC5.
  • Lean's automated tactics (omega, polyrith, decide, aesop) — reduce the amount of manual proof in Lean developments.

Correct-by-construction refinement

The B-method and Event-B are a development style rather than a separate method: the program is built by stepwise refinement from an abstract specification, and each step emits proof obligations whose discharge shows the refinement preserves behavior, so the code is correct by construction rather than proven after the fact. Atelier B and Rodin are the toolchains, and the approach's record is in railway signaling — the Paris Métro line 14 controller. The verification underneath is the same machine-checked proof; refinement organizes the development around it.

Trusted base

  • SMT solvers are part of the trusted base in F*, Dafny and Why3: a goal the solver discharges is accepted without a separately checked proof. Coq and Lean instead re-check SMT-generated proof certificates or run the proof against the trusted kernel.
  • Z3, CVC5, Yices2, Alt-Ergo are the dominant SMT back-ends.

When to use, when not

Use:

  • Components with high blast radius and small surface: OS kernels, hypervisors, bootloaders, crypto primitives, TLS stacks, formally verified compilers. The ratio of cost to defects-eliminated favors verification at this end.
  • Spec writing for any system that must outlive its implementation. The proof is a durable artifact; the implementation may not be.
  • After a major incident attributable to a class of bug a proof could have eliminated. The cost of the incident often justifies the cost of the verification afterwards.

Don't:

  • For business logic, CRUD, glue code. The cost ratio is wrong. Use contracts for the same shape at orders of magnitude less effort.
  • As a substitute for testing the spec itself. Test the spec at least as hard as the code; Csmith against CompCert is the canonical pairing.
  • Without a long-term commitment. An abandoned proof leaves the code with unmet obligations and no guarantee.

Evidence

  • seL4. Formal verification of an 8,700-LOC microkernel against an Isabelle/HOL spec; 144 defects found during proof; ~11 person-years for the proof itself (≈20 including tooling and research) (Klein et al. 2009)4.
  • CompCert. Compiler correctness proved end to end in Coq (Leroy 2009)2.
  • Fiat-Crypto. Machine-checked elliptic-curve field arithmetic, generated in Coq and deployed in Chrome and Android (Erbsen et al. 2019)3.
  • Project Everest. Verified TLS 1.3 stack and crypto primitives in F*; verification surfaced TLS 1.3 spec ambiguities that were fed back into the IETF process. HACL* / EverCrypt is deployed in Mozilla NSS (Firefox), the Linux kernel and Python's hashlib; EverParse-generated parsers run in Windows Hyper-V.
  • AWS Cedar. A Dafny implementation of the authorization-policy language is proved to satisfy security properties, and the production Rust implementation is differentially tested against it (Brooker and Desai 2024)5.

The empirical record is concentrated in deployments where the cost/benefit is unusually favorable: kernels, crypto, compilers. At those targets the empirical support is direct and repeated across independent projects.

Oracle: predicate

All four answer the same question — does property P hold? — and differ only in how that answer is obtained, from cheapest-and-weakest to strongest:

  • Runtime contracts — check P during execution, on the inputs you actually run, and crash if it's violated.
  • Property-based testing — check P on many generated inputs; empirical, with no guarantee past what was sampled.
  • Refinement & dependent types — encode P in the type, so the compiler rejects any program that could violate it (sound within what the type can express).
  • Theorem proving — prove P holds for all inputs, ahead of time.

Classification

  • Quality dimensions: Functionality, Security (proves adversarial security properties — kernel isolation and information-flow non-interference (seL4)).
  • Area: OS kernels and hypervisors, verified compilers, crypto primitives and TLS stacks, safety-critical embedded software.
  • Guarantee: Mathematical — within the assumed semantics, no failure exists at all.

Referenced by

References

  1. Yang, Xuejun, Yang Chen, Eric Eide, and John Regehr. 2011. "Finding and Understanding Bugs in C Compilers." Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11), 283–94. https://doi.org/10.1145/1993498.1993532. ↩

  2. Leroy, Xavier. 2009. "Formal Verification of a Realistic Compiler." Communications of the ACM 52 (7): 107–15. https://doi.org/10.1145/1538788.1538814. ↩↩

  3. Erbsen, Andres, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. "Simple High-Level Code for Cryptographic Arithmetic: With Proofs, Without Compromises." IEEE Symposium on Security and Privacy (s&p '19), 1202–19. https://doi.org/10.1109/SP.2019.00005. ↩↩

  4. Klein, Gerwin, Kevin Elphinstone, Gernot Heiser, et al. 2009. "seL4: Formal Verification of an OS Kernel." Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP '09), 207–20. https://doi.org/10.1145/1629575.1629596. ↩↩

  5. Brooker, Marc, and Ankush Desai. 2024. "Systems Correctness Practices at Amazon Web Services." Communications of the ACM, ahead of print. https://doi.org/10.1145/3729175. ↩