English
A specification is a precise description of what a system is supposed to do. A formal method is a mathematically grounded technique for writing such descriptions and for establishing, through proof rather than through testing, that an implementation satisfies them. The distinction matters because testing and proof answer different questions. Testing asks: does the system behave correctly on these inputs? Proof asks: does the system behave correctly on all inputs? No finite number of tests can establish the second claim; a valid proof does.
The discipline has three main branches that use different techniques for different system properties. Model checking automatically exhausts the state space of finite-state systems to verify temporal properties — “the system never reaches a deadlocked state,” “every request is eventually serviced.” Theorem proving uses interactive proof assistants to verify properties that model checking cannot reach, requiring human guidance but producing stronger guarantees about infinite systems and full functional correctness. Static analysis automatically checks limited but important properties — memory safety, type safety, null pointer dereferences — with varying degrees of precision and automation. A mature formal methods practitioner knows which technique fits which situation and what each costs.
Formal methods is the applied end of the Theory Axis. Logic (§3.1) provides the inference systems. Type theory (§3.5) provides the type-theoretic foundations that proof assistants are built on. PLT (§3.4) provides the semantic frameworks in which specifications are interpreted. What formal methods does is take these theoretical foundations and use them to verify real systems: operating system kernels, cryptographic libraries, distributed protocols, compilers, and — increasingly — the protocols used in everyday software infrastructure.
Prerequisites: Logic (§3.1) — inference rules and temporal logic. Type theory (§3.5) — proof assistant use requires familiarity with dependent types and the Curry-Howard correspondence. PLT (§3.4) — Hoare logic and operational semantics. Algorithms and data structures (§2.6) — for model checking complexity.
From Program Correctness to Industrial Verification
The idea that programs could be proved correct — rather than merely tested — is about sixty years old, and its development from philosophical proposal to industrial practice is one of the more dramatic stories in computer science.
Robert Floyd’s 1967 paper “Assigning Meanings to Programs” introduced the idea of attaching logical assertions to the edges of a program’s flowchart. If an assertion is true when control reaches a particular edge, and the program’s transitions preserve the assertions, then the final assertion is guaranteed to hold when the program terminates. Floyd’s insight was to treat program correctness as a property that could be expressed in first-order logic and established by induction over the program’s execution. Tony Hoare’s 1969 paper “An Axiomatic Basis for Computer Programming” converted Floyd’s flowchart approach into a logic of commands: the Hoare triple {P} C {Q} asserts that if predicate P holds before command C executes and C terminates, then Q holds after. Hoare gave inference rules for each command type — assignment, sequencing, conditionals, loops — composable into proofs of program correctness. The framework was clean, the proofs were mathematical, and the gap between theory and practice was obvious: the proofs were done by hand, they were tedious, and nothing prevented the specification from being wrong while the program was verified against it.
Edsger Dijkstra’s contribution, developed through the 1970s and consolidated in A Discipline of Programming (1976), was the weakest precondition calculus. Given a postcondition Q and a command C, the weakest precondition wp(C, Q) is the most general condition that, if it holds before C, guarantees Q holds after C terminates. This turned verification into a calculational activity: derive the wp backwards from the postcondition through each program statement, and the resulting formula is what must be established at the program’s start. Dijkstra’s methodology produced the concept of programming-by-refinement: start with a specification, refine it through correctness-preserving steps into an implementation, and the implementation is correct by construction. The idea was intellectually compelling and practically demanding — the discipline required was severe, and hand proofs at any scale were infeasible.
The first practical breakthrough came from a different direction. Edmund Clarke and E. Allen Emerson, at Harvard, and independently Joseph Sifakis, at IMAG in Grenoble, developed model checking in 1981. The core insight was that for finite-state systems, the question of whether a system satisfies a temporal property — whether a condition is always true, whether some condition is eventually reached, whether one event always precedes another — can be answered by systematic exploration of all reachable states. No human guidance is needed; the model checker exhaustively checks every execution. The temporal logics CTL (Clarke-Emerson) and LTL (linear time) provided the specification language; the model checkers provided the automation. Clarke, Emerson, and Sifakis received the Turing Award in 2007 for this contribution.
Model checking worked beautifully for small systems and failed catastrophically for large ones. The state space of a real concurrent system with n boolean variables has 2ⁿ states; checking all of them is exponential in n. The state explosion problem was the fundamental obstacle, and the 1980s were spent developing techniques to mitigate it. Bryant’s Binary Decision Diagrams (BDDs) in 1986 provided a compact symbolic representation of state sets that allowed model checkers to handle systems with millions of states in milliseconds — an exponential improvement in practice even though the worst case remained exponential. Counterexample-Guided Abstraction Refinement (CEGAR), SAT-based bounded model checking, and other techniques extended the reach further. By the mid-1990s, model checking was being used industrially at Intel, Motorola, and IBM to find bugs in hardware designs before manufacturing — bugs that once found in silicon cost tens of millions of dollars to correct, but that model checking found in simulation for nearly nothing.
Leslie Lamport developed TLA+ (Temporal Logic of Actions) in the 1990s as a specification language for concurrent and distributed systems. TLA+ uses first-order logic and a simple temporal layer to specify system behavior as state transitions, and the TLA+ tools check that specifications are internally consistent and that implementations refine their specifications. TLA+ occupied a different niche from both model checking and theorem proving: it was designed for specifying distributed algorithms and protocols at a level of abstraction that makes the essential correctness arguments visible without requiring full formalization. Lamport and collaborators used it to specify and check the correctness of Paxos and other distributed algorithms. In 2014, Amazon Web Services published an account of using TLA+ to find subtle bugs in distributed protocols underlying S3, DynamoDB, and EBS — bugs that had resisted years of testing and code review, found by writing formal specifications and running the model checker. This account, more than any academic result, demonstrated to the software industry that formal specification had practical value.
The proof assistant side developed more slowly. The fundamental challenge is that full functional verification — proving that a system satisfies a complete specification of its behavior, not just selected properties — requires human guidance that is expensive to provide. Coq, based on the Calculus of Constructions, had been developed at INRIA since the mid-1980s and was capable of substantial verified reasoning. The question was whether it was capable of verifying something real.
Xavier Leroy answered this in 2006 with CompCert: a verified optimizing compiler for a substantial subset of C. Every optimization pass in CompCert is accompanied by a Coq proof that it preserves program semantics — that the compiled output has the same observable behavior as the source. The CompCert proofs took several person-years of work and consist of approximately 70,000 lines of Coq. The result was a compiler that had been tested in ways that random testing and code review cannot provide: formal proof that every optimization is semantics-preserving. CompCert has been deployed in safety-critical contexts where compiler bugs could have fatal consequences.
Three years later, in 2009, Gerwin Klein and colleagues at NICTA (now CSIRO’s Data61) announced the verification of seL4, the first mathematically verified operating system kernel. seL4 is a microkernel — a minimal kernel that provides only fundamental services — and its verification establishes that the C implementation correctly implements the Haskell specification, and that the Haskell specification has the desired security properties. The proof spans approximately 200,000 lines of Isabelle script. seL4 runs in production systems in safety-critical aerospace applications where the cost of an operating system bug is measured in lives.
The contemporary period has brought both the maturation of established tools and new directions. The Lean proof assistant, redesigned as Lean 4 and released in 2021, has attracted a large community of mathematicians and software engineers. The HACLlibrary — verified cryptographic primitives in F, a dependently typed language with automated verification — is integrated into Firefox, Chrome, and the Linux kernel. Project Everest, a joint effort across Microsoft Research, INRIA, and other institutions, has produced a verified implementation of TLS 1.3. The scale of verified software has increased from individual algorithms to complete protocol stacks.
The question that remains open is whether the cost of formal verification can be reduced enough to make it routine rather than exceptional. Automated proof synthesis, proof repair, and the integration of AI assistance into proof workflows are active research areas. Current large language models can generate proof sketches in Lean and Coq, suggest lemmas, and sometimes discharge proof obligations automatically. Whether this will reduce the cost of formal verification by a factor of two or by a factor of twenty — and what that would mean for the boundary between formally verified and informally tested software — is a genuinely open question.
Specification, Verification, and the Techniques Between Them
What Specifications Are and Why Writing Them Is Hard
A specification is a mathematical description of system behavior. The difficulty is that most systems are specified informally — in prose requirements documents, API documentation, or the shared understanding of a development team — and formalizing informal specifications is genuinely hard. Not because formalization is technically difficult, but because the process of formalization reveals that the informal specification was ambiguous, incomplete, or internally inconsistent.
A formal specification must answer questions that informal specifications leave open. What happens if the function is called with an argument outside its specified domain? What behavior is guaranteed when the network is partitioned? If two clients write to the same key concurrently, what is the result? Informal specifications routinely leave such questions unaddressed, relying on the reader to infer “reasonable” behavior. Formal specifications must commit to one answer, and the process of making that commitment often reveals that different stakeholders had different expectations.
Specification languages provide different trade-offs between expressiveness and automation. TLA+ uses set theory and temporal logic — expressive enough to specify most distributed algorithms, with model checking automation for finite instances. Alloy uses relational logic and provides automatic analysis of small models, revealing counterexamples to claimed properties without requiring proofs. Z and B use set-theoretic notation and support refinement-based development. Hoare logic and its descendants — including separation logic for heap-manipulating programs and concurrent separation logic for shared-memory concurrent programs — express specifications as pre- and post-conditions of individual procedures. Temporal logics (LTL, CTL, CTL*) specify system properties that unfold over time — safety properties (“nothing bad ever happens”) and liveness properties (“something good eventually happens”). Each formalism is the right choice for different systems and different properties.
The meta-lesson is that specification adequacy cannot be verified automatically. A specification that is internally consistent and that the implementation satisfies can still be wrong if it fails to capture what the stakeholders actually wanted. The discipline of specification — learning to write specifications that faithfully capture intent — is acquired through practice, through the uncomfortable process of formalizing existing informal descriptions and discovering that they were more ambiguous than they appeared.
Model Checking: Exhaustive Verification of Finite Systems
Model checking works by representing a system as a mathematical model — typically a Kripke structure, a directed graph where nodes are system states and edges are transitions — and checking that every path through the model satisfies a temporal property. For finite models, this is decidable: the model checker runs through all reachable states and all possible behaviors. For a property P and a model M, the model checker either produces a certificate that M satisfies P or a counterexample — an execution trace that violates P.
The power of model checking is that counterexamples are concrete execution traces, not abstract impossibility proofs. When a model checker reports that a distributed protocol can deadlock, it produces a specific sequence of messages and actions that leads to the deadlock — directly actionable information for the protocol designer. This concreteness is what made model checking immediately useful in hardware verification, where engineers could take the counterexample and understand exactly what circuit behavior had been overlooked.
The fundamental limitation is the state explosion problem. A concurrent system with n independent components, each with k states, has k^n global states. For n = 100 components each with k = 2 states, the state space has 2^100 states — far beyond any computer’s capacity to enumerate. The techniques for managing state explosion are central to practical model checking: BDD-based symbolic representation can handle millions of states; partial order reduction exploits the fact that many interleavings of independent events lead to the same final state; counterexample-guided abstraction refinement starts with a coarse model and refines only where needed; bounded model checking uses SAT solvers to check properties up to a bounded number of steps. Each technique extends the range of systems that model checking can handle; none eliminates the fundamental exponential dependence on system size.
The temporal logic used for specification determines what properties can be expressed and what algorithms apply. CTL (computation tree logic) specifies branching-time properties — properties that quantify over possible futures from each state. LTL (linear temporal logic) specifies linear-time properties — properties that quantify over all possible executions. The two logics are incomparable in expressiveness: some CTL properties have no LTL equivalent, and vice versa. CTL model checking is polynomial in the size of the model; LTL model checking is PSPACE-complete. In practice, the choice between CTL and LTL is driven by which properties are natural to express and which tools are available, not by the complexity theory.
Theorem Proving: Full Functional Verification
Model checking handles finite systems automatically. When a system is infinite — when it involves unbounded data structures, when the correctness property quantifies over all possible inputs, when the specification is a complete functional correctness statement rather than a temporal property — theorem proving is the appropriate technique.
Theorem proving in the formal methods sense means using a proof assistant interactively: the human writes proof scripts, the system checks each step, and the result is a machine-verified proof that the implementation satisfies the specification. The interaction is labor-intensive — proof scripts for a substantial system can run to hundreds of thousands of lines — but the output is a certificate of correctness that is not subject to human verification error.
Proof assistants used in formal methods divide broadly into two families. Higher-order logic (HOL) proof assistants — Isabelle/HOL, HOL4, HOL Light — provide a foundational logic (higher-order predicate logic) with a rich library of proved mathematics and software theorems. The emphasis is on automation: powerful tactics, powerful SMT backend integration, and substantial pre-proved libraries reduce the human proof burden. Dependent type theory proof assistants — Coq, Lean, Agda — provide type systems powerful enough to express specifications directly in types, using the Curry-Howard correspondence to unify programming and proving. The emphasis is on expressiveness and on the integration of specifications with implementations.
The choice between proof assistants is partly a matter of the application domain and partly a matter of community. seL4 was verified in Isabelle/HOL. CompCert was verified in Coq. The HACLlibrary is verified in F. Each choice reflects the strengths of the tool and the preferences of the team. For learners, the pragmatic advice is to pick one tool, work through it deeply, and recognize that the skills transfer substantially across tools.
Separation logic, developed by John Reynolds, Samin Ishtiaq, and Peter O’Hearn in the early 2000s, is the framework that makes verification of heap-manipulating programs tractable. Classic Hoare logic requires specifying the entire heap state in every pre- and post-condition, producing specifications that scale poorly with program size. Separation logic’s separating conjunction P * Q asserts that P and Q hold for disjoint parts of the heap, allowing specifications to be local: a function’s specification says what it does to its own memory and leaves the rest of the heap unmentioned. This locality makes it possible to verify large heap-manipulating programs compositionally, verifying each function in isolation. Concurrent separation logic extends this to concurrent programs, supporting the verification of race-free shared-memory programs and the concurrent data structures used in production systems.
Static Analysis: Automated Verification of Limited Properties
Static analysis checks properties of programs automatically, without requiring human-written specifications or proofs, at the cost of checking only limited properties and potentially reporting false positives. Abstract interpretation, developed by Patrick and Radhia Cousot in 1977, provides the mathematical foundation: the program is analyzed over an abstract domain (intervals, convex polyhedra, types) that approximates the concrete semantics, and properties are checked in the abstract domain. Every property established in the abstract domain holds in the concrete domain (soundness), but the abstract domain may fail to establish properties that do hold concretely (incompleteness).
Modern static analyzers built on abstract interpretation — Astrée (which verified the absence of runtime errors in Airbus A380 flight control software), Frama-C (for C programs), and various academic systems — can verify memory safety, integer overflow absence, and other properties automatically for large programs. Facebook’s Infer, a static analyzer based on separation logic, scales to codebases with millions of lines and is integrated into the CI pipelines of major technology companies, finding memory safety bugs before they reach production.
The trade-off between automation and strength is fundamental. Type systems are lightweight static analyses — they check properties automatically with no annotations — but can only establish type-safety, not functional correctness. Model checking is heavier but handles temporal properties of finite-state systems automatically. Theorem proving is the heaviest and handles functional correctness of infinite systems but requires substantial human effort. The art of formal methods practice is matching technique to property: using type systems for the ubiquitous properties they handle well, model checking for the concurrent and protocol properties it handles well, and theorem proving for the deep functional correctness properties that only it can establish.
What Studying This Changes
Formal methods produces practical changes in how practitioners think about and build software, even when they are not doing formal verification.
The first change is the specification discipline. The experience of writing formal specifications — and discovering what informal specifications left unspecified — permanently changes how practitioners approach specification. The questions a formal methods practitioner asks when reading requirements: what happens in this corner case? what is the behavior when these two operations are concurrent? is this property a safety property or a liveness property? These questions are not asked because formal methods is being applied; they are asked because the discipline of formalization makes their importance visible. The result is clearer requirements, better API contracts, and more carefully designed systems.
The second change is the understanding of what testing can and cannot establish. Testing demonstrates the presence of bugs on tested inputs; it cannot establish their absence on all inputs. A practitioner who has worked with formal verification has internalized this distinction and has developed complementary strategies: using formal methods where the cost of undetected bugs is highest, using testing where formal methods costs exceed their benefits, and understanding clearly which properties have been formally established and which have only been empirically tested.
The third change is access to the formal verification tools. Model checkers, proof assistants, and static analyzers are the most powerful available tools for establishing software correctness properties, and using them requires understanding their foundations. A practitioner who has studied formal methods can use TLA+ to check a distributed protocol design before implementation, can use a proof assistant to verify a critical security property, can read the proofs that accompany verified system components. This access is what makes formal verification a practical option rather than an academic aspiration.
The fourth change is the ability to read the formal verification literature. The papers describing CompCert, seL4, HACL*, and other verified systems are important technical documents that demonstrate what is possible and how it is done. A practitioner who has studied formal methods can read these papers and understand what was verified, what was assumed, and what techniques were used — information that is relevant when deciding whether to build on these verified components or to perform similar verification for new systems.
Resources
Books and Texts
For theorem proving through proof assistants, Pierce et al.’s Software Foundations series (free at softwarefoundations.cis.upenn.edu) is the standard entry. Volume 1 (Logical Foundations) teaches Coq and logic simultaneously. Volume 2 (Programming Language Foundations) formalizes operational semantics, type systems, and Hoare logic in Coq — connecting directly to §3.4. Volume 3 (Verified Functional Algorithms) extends to algorithm verification. The series is well-paced, actively maintained, and the exercises build genuine competence. For learners who prefer Lean, Theorem Proving in Lean 4 (free at lean-lang.org) and the Functional Programming in Lean book (free at lean-lang.org/functional_programming_in_lean) provide the Lean equivalents.
For TLA+ and distributed systems specification, Lamport’s Specifying Systems (free at lamport.azurewebsites.net) is the definitive reference by the tool’s designer. It develops TLA+ systematically with the philosophical justification for the design choices. Wayne’s Practical TLA+ (Apress, 2018) is more accessible for working engineers, covering TLA+ with practical examples and without requiring the full logical background. Reading Wayne first then Lamport is the most efficient path for practitioners who want to use TLA+ rather than understand it foundationally.
For model checking, Baier and Katoen’s Principles of Model Checking (MIT Press, 2008) is the standard graduate textbook. It covers Kripke structures, temporal logics (LTL, CTL, CTL*), model checking algorithms, BDD-based symbolic model checking, and partial order reduction, with full proofs. Clarke, Grumberg, and Peled’s Model Checking (MIT Press, 1999) is the earlier standard reference by the technique’s inventors, now partially superseded by Baier-Katoen but still useful for historical context and original perspectives.
Jackson’s Software Abstractions (MIT Press, revised ed., 2012) teaches formal specification through Alloy, a lightweight relational logic with an automatic analyzer. Jackson’s argument is that most systems should be specified and analyzed at a level of abstraction below full theorem proving — specifying the key data relationships and checking them against small instances to find design errors before implementation. The approach is more accessible than full verification and catches a significant class of design bugs.
Chlipala’s Certified Programming with Dependent Types (MIT Press, 2013, free online) develops verification of substantial programs in Coq, going beyond the introductory level of Software Foundations. It is the right next step for learners who have completed Software Foundations and want to verify nontrivial systems. Bertot and Castéran’s Interactive Theorem Proving and Program Development: Coq’Art (Springer, 2004) is the comprehensive Coq reference, appropriate as a reference throughout Coq-based work.
Nipkow and Klein’s Concrete Semantics with Isabelle/HOL (free online; paid Springer edition) teaches programming language semantics, Hoare logic, abstract interpretation, and compiler correctness through Isabelle/HOL. It is the best Isabelle-based counterpart to the Coq path provided by Software Foundations and is especially valuable for readers who want a higher-order logic proof assistant rather than a dependent type theory proof assistant.
Leino’s Program Proofs (MIT Press, paid) teaches specification and program verification through Dafny. It is more engineer-facing than Coq or Isabelle texts: the examples are executable programs with preconditions, postconditions, invariants, and SMT-assisted proofs. The limitation is that it teaches the Dafny style specifically, so it should complement rather than replace general formal methods foundations.
For Hoare logic and separation logic at depth, Reynolds’s Theories of Programming Languages (Cambridge, 1998) provides the foundational treatment. O’Hearn’s various papers on separation logic — particularly the 2019 Turing Award lecture “Separation Logic” — are the best introductions to the subject from its developer.
| Book | Role | Type |
|---|---|---|
| Pierce et al., Software Foundations Vols. 1–3 (free) | Standard Coq-based entry to FM and verification | Entry |
| Lamport, Specifying Systems (free) | Canonical TLA+ reference by its designer | Entry |
| Wayne, Practical TLA+ | Engineer-oriented TLA+ introduction | Entry |
| Baier & Katoen, Principles of Model Checking | Standard model checking textbook | Depth |
| Clarke, Grumberg & Peled, Model Checking | Original model checking reference | Reference |
| Jackson, Software Abstractions (revised ed.) | Lightweight formal methods through Alloy | Entry |
| Coq verification chapters in Chlipala, Certified Programming with Dependent Types (free) | Coq-based verification beyond introductory level | Entry |
| Bertot & Castéran, Coq’Art | Comprehensive Coq reference | Reference |
| Nipkow & Klein, Concrete Semantics with Isabelle/HOL (free; paid print) | Isabelle-based semantics and verification | Practice |
| Leino, Program Proofs (paid) | Dafny-based program verification | Entry |
Courses and Lectures
MIT 6.5840 (Distributed Systems, formerly 6.824, free materials) is not a formal methods course, but its lab assignments — implementing Raft, MapReduce, and fault-tolerant key-value storage — provide the distributed systems context that TLA+ verification is most valuable in. The combination of implementing distributed systems and specifying them in TLA+ is more educationally productive than either alone.
The Software Foundations series, when worked through as a self-paced course (using the exercises as problem sets), constitutes one of the best free courses on formal verification available. The Coq Proof Assistant exercises, Hoare logic formalization, and type system soundness proofs together cover the key techniques.
CMU 15-414/615 (Bug Catching: Automated Program Verification and Testing) is a graduate course with freely available materials that covers model checking, SMT-based verification, abstract interpretation, and symbolic execution — a good complement to the theorem-proving focus of Software Foundations.
OPLSS lectures on formal verification (free on YouTube) — particularly lectures by Adam Chlipala on certified programming, by Andrew Appel on program verification, and by various speakers on separation logic — cover advanced formal methods at graduate depth.
| Course | Platform | Type |
|---|---|---|
| Software Foundations (Coq exercises, free) | softwarefoundations.cis.upenn.edu | Practice |
| CMU 15-414/615 Bug Catching (free) | CMU course site | Depth |
| OPLSS formal verification lectures (free) | YouTube / OPLSS site | Depth |
| MIT 6.5840 Distributed Systems labs (free) | MIT course site | Auxiliary |
Practice, Tools, and Current Sources
The tools are the subject. Engaging with formal methods requires hands-on work; reading about it is insufficient.
TLA+ Toolbox or VS Code TLA+ extension (free at lamport.azurewebsites.net): install, work through the tutorial in Wayne’s Practical TLA+, and write a TLA+ specification for a small concurrent algorithm. Seeing the model checker find a counterexample to a plausible-seeming invariant is the most direct way to understand what TLA+ is useful for.
Coq (free at coq.inria.fr) with the Proof General Emacs interface or VSCoq for VS Code: install, work through Volume 2 of Software Foundations, and formalize the type soundness proof for the STLC. The experience of having Coq reject a proof because a case is missing makes type soundness concrete in a way that reading does not.
Alloy Analyzer (free at alloytools.org): install, work through Jackson’s Software Abstractions Chapters 1-5, and model a small file system or address book. The automatic counterexample generation makes specification errors immediately visible.
SPIN (free at spinroot.com) is the standard model checker for concurrent systems specified in Promela. It is particularly effective for verifying communication protocols and concurrent algorithms.
Facebook’s Infer (free at fbinfer.com) demonstrates what automated static analysis at industrial scale looks like. Running Infer on an existing C or Java codebase and examining its output is more educational than any tutorial.
Dafny (free) is the most accessible SMT-assisted verification language for learning program proofs with ordinary functional and imperative code. It gives immediate feedback on specifications, loop invariants, and proof hints without requiring the learner to manage every proof step manually. Verus (free) brings a similar verification ambition to Rust systems code and is worth watching for readers interested in ownership, linear reasoning, and low-level verification, though it is still a more advanced and younger ecosystem.
The CACM article How AWS Uses Formal Methods is the best short industrial case study for TLA+ in distributed systems design. It should be read after a first TLA+ tutorial, when the learner can recognize why finding design bugs before implementation changes the economics of reliability.
Hillel Wayne maintains excellent TLA+ tutorials (learntla.com, free) that are the most accessible introduction to TLA+ beyond Wayne’s book, covering common patterns and pitfalls in writing TLA+ specifications.
| Resource | Platform | Type |
|---|---|---|
| TLA+ Toolbox / VS Code TLA+ extension (free) | lamport.azurewebsites.net | Practice |
| Coq + Proof General or VSCoq (free) | coq.inria.fr | Practice |
| Alloy Analyzer (free) | alloytools.org | Practice |
| Model checking practice with SPIN (free) | spinroot.com | Practice |
| Facebook Infer (free) | fbinfer.com | Practice |
| Dafny (free) | dafny.org | Practice |
| Verus (free) | verus-lang.github.io | Auxiliary |
| AWS, How AWS Uses Formal Methods (free article) | CACM / AWS | Auxiliary |
| learntla.com — TLA+ tutorials (free) | learntla.com | Entry |
Traps
| Trap | Why it misleads | Better response |
|---|---|---|
| Treating formal methods as proof of absolute correctness | A formally verified system is verified with respect to a specification, against a model of its environment, using tools that themselves embody assumptions. The specification can be wrong; the model can fail to capture real-world conditions; the tools can have bugs (though proof assistant kernels are small and carefully maintained). Saying a system is “proven correct” without these qualifications is misleading. | State verification claims precisely: “CompCert is verified to produce object code with the same behavior as the source, assuming the C semantics in the Coq formalization.” Know what was verified, what was assumed, and what the tool’s trusted computing base includes. Honest claim-making is one of formal methods’ most valuable contributions to engineering culture. |
| Skipping specification to reach verification | Some learners want to immediately verify programs without investing time in writing specifications. This reverses the productive order: a verified program satisfies its specification, and if the specification doesn’t capture what is wanted, verification provides no assurance about what matters. | Spend as much time on specification as on verification, or more. Write a specification for a system you know well — a concurrent queue, a small protocol — and ask a colleague to find cases your specification doesn’t handle. The gaps that emerge teach specification more than any tutorial. |
| Approaching formal methods through a single tool | TLA+ is not interchangeable with Coq, which is not interchangeable with Alloy, which is not interchangeable with SPIN. Each tool is appropriate for different kinds of properties of different kinds of systems. A practitioner who knows only one tool reaches for it regardless of fit — using TLA+ for full functional verification that Coq would handle better, or using Coq for protocol checking that TLA+ would handle more naturally. | Learn at least two tools from different paradigms: one for model checking or specification (TLA+, Alloy, SPIN) and one for theorem proving (Coq, Lean, Isabelle). The contrast between them makes the strengths and limitations of each visible in ways that single-tool exposure cannot. |
| Underestimating the specification problem | Most formal verification failures are specification failures: the implementation satisfies the specification, but the specification doesn’t capture what was intended. Learners who focus on verification techniques while treating specification as straightforward preparation are surprised by how much of the difficulty lies in specification. | Work through examples where specifications turn out to be wrong: write a specification, have the model checker check it, and then introduce a property you believe should hold and watch it be violated. The violations reveal what the specification left unspecified. This exercise builds specification intuition that reading cannot. |
| Expecting formal methods to be universally applicable | Full functional verification is expensive — CompCert took person-years of Coq proof work; seL4 took approximately 20 person-years. For most software, this cost is not justified. Learners who approach formal methods as the right approach to all software development are disappointed by the cost and conclude formal methods is impractical. | Match technique to context. Type checking is free and should be used everywhere. Static analysis (Infer, Coverity, Astrée) costs little and catches significant bugs. Model checking a protocol design costs days and catches design errors before implementation. Full theorem proving costs person-months and is appropriate for critical infrastructure. Learn the full spectrum and apply it at the appropriate level. |
| Not engaging with the major verified systems | CompCert, seL4, HACL*, and the verified TLS implementation from Project Everest are existence proofs that formal methods works at scale. Learners who know the techniques without studying these systems miss the demonstration that the techniques actually produce something — and miss the design decisions and tradeoffs that make large-scale verification tractable. | Read the papers describing CompCert (Leroy 2006, 2009) and seL4 (Klein et al. 2009). They are directly accessible after completing Software Foundations and explain what was verified, how long it took, what tools were used, and what the proof structure looks like. The papers are concretely inspiring in ways that abstract technique descriptions are not. |
中文
规约是对系统应当做什么的精确描述。形式化方法则是建立在数学基础上的技术，用于书写这类描述，并通过证明而不是测试来确立实现满足这些描述。这个区别很重要，因为测试和证明回答的是不同问题。测试问的是：系统在这些输入上是否表现正确？证明问的是：系统在所有输入上是否表现正确？有限数量的测试无法确立第二个主张；有效证明可以。
这门学科有三个主要分支，用不同技术处理不同系统性质。模型检查会自动穷尽有限状态系统的状态空间，以验证时序性质——“系统永远不会到达死锁状态”“每个请求最终都会被服务”。定理证明使用交互式证明助手验证模型检查无法覆盖的性质，需要人类指导，但能对无限系统和完整函数正确性提供更强保证。静态分析会自动检查有限但重要的性质——内存安全、类型安全、空指针解引用——并在精确性和自动化程度之间有不同取舍。成熟的形式化方法实践者知道哪种技术适合哪种情境，也知道每种技术的成本。
形式化方法是理论轴的应用端。逻辑（§3.1）提供推理系统。类型论（§3.5）提供证明助手建立其上的类型论基础。PLT（§3.4）提供解释规约的语义框架。形式化方法所做的，是把这些理论基础拿来验证真实系统：操作系统内核、密码学库、分布式协议、编译器，以及越来越多日常软件基础设施中使用的协议。
前置知识：逻辑（§3.1）——推理规则和时序逻辑。类型论（§3.5）——使用证明助手需要熟悉依赖类型和 Curry-Howard 对应。PLT（§3.4）——Hoare logic 和操作语义。算法与数据结构（§2.6）——用于理解模型检查复杂度。
从程序正确性到工业验证
程序可以被证明正确——而不只是被测试——这个想法大约有六十年历史。它从哲学性提案发展到工业实践，是计算机科学中较具戏剧性的故事之一。
Robert Floyd 1967 年的论文 “Assigning Meanings to Programs” 引入了一个想法：把逻辑断言附加到程序流程图的边上。如果控制到达某条边时一个断言为真，并且程序的转移会保持这些断言，那么程序终止时最终断言就保证成立。Floyd 的洞见是，把程序正确性视为一种可以用一阶逻辑表达、并通过对程序执行做归纳来确立的性质。Tony Hoare 1969 年的论文 “An Axiomatic Basis for Computer Programming” 把 Floyd 的流程图方法转化为命令逻辑：Hoare 三元组 {P} C {Q} 断言，如果命令 C 执行前谓词 P 成立，并且 C 终止，那么执行后 Q 成立。Hoare 为每种命令类型给出推理规则——赋值、顺序组合、条件、循环——这些规则可以组合成程序正确性证明。这个框架干净，证明是数学性的，而理论与实践之间的鸿沟也很明显：证明要手工完成，过程繁琐，而且即使程序相对于规约被验证，仍然无法防止规约本身是错的。
Edsger Dijkstra 的贡献是在 1970 年代发展并在 A Discipline of Programming（1976）中系统化的最弱前置条件演算。给定后置条件 Q 和命令 C，最弱前置条件 wp(C, Q) 是最一般的条件；只要它在 C 执行前成立，就能保证 C 终止后 Q 成立。这把验证变成一种计算活动：从后置条件出发，沿着程序语句向后推导 wp，最终得到的公式就是程序开始时必须建立的内容。Dijkstra 的方法论产生了按精化编程的概念：从规约开始，通过保持正确性的步骤逐步精化为实现，而实现由构造过程保证正确。这个想法在智识上很有吸引力，但实践上要求很高——所需纪律极其严格，而任何规模上的手工证明都不可行。
第一个实践突破来自另一个方向。Edmund Clarke 和 E. Allen Emerson 在 Harvard，以及 Joseph Sifakis 在 Grenoble 的 IMAG，各自独立于 1981 年发展出模型检查。核心洞见是，对于有限状态系统，系统是否满足某个时序性质——某条件是否总为真、某条件是否最终到达、某事件是否总在另一事件之前发生——可以通过系统探索所有可达状态来回答。无需人类指导；模型检查器会穷尽检查每一种执行。时序逻辑 CTL（Clarke-Emerson）和 LTL（线性时间）提供规约语言；模型检查器提供自动化。Clarke、Emerson 和 Sifakis 因此贡献获得 2007 年图灵奖。
模型检查在小系统上运行极好，在大系统上则灾难性失败。一个拥有 n 个布尔变量的真实并发系统具有 2ⁿ 个状态；检查全部状态在 n 上是指数级的。状态爆炸问题是根本障碍，1980 年代大量工作都用于发展缓解它的技术。Bryant 1986 年提出的二叉决策图（BDD）提供了一种紧凑的符号化状态集合表示，使模型检查器可以在毫秒级处理数百万状态——虽然最坏情况仍是指数级，但实践中获得了指数级改善。反例引导抽象精化（CEGAR）、基于 SAT 的有界模型检查以及其他技术进一步扩展了可处理范围。到 1990 年代中期，Intel、Motorola 和 IBM 已经在工业中使用模型检查，在制造前发现硬件设计中的 bug——这些 bug 一旦进入硅片，修复成本可能高达数千万美元；而模型检查几乎可以在仿真中免费发现它们。
Leslie Lamport 在 1990 年代发展出 TLA+（Temporal Logic of Actions），作为并发和分布式系统的规约语言。TLA+ 使用一阶逻辑和一个简单时序层，把系统行为规定为状态转移；TLA+ 工具则检查规约内部一致性，并检查实现是否精化其规约。TLA+ 占据了不同于模型检查和定理证明的生态位：它被设计用于在一种抽象层级上规定分布式算法和协议，使核心正确性论证可见，而不要求完整形式化。Lamport 及合作者用它规定并检查 Paxos 和其他分布式算法的正确性。2014 年，Amazon Web Services 发表文章说明如何用 TLA+ 发现支撑 S3、DynamoDB 和 EBS 的分布式协议中的细微 bug——这些 bug 经多年测试和代码审查仍然存在，却通过书写形式规约并运行模型检查器被发现。比起任何学术结果，这篇文章更有力地向软件行业证明了形式规约的实践价值。
证明助手这一侧发展得更慢。根本挑战在于，完整函数验证——证明系统满足其行为的完整规约，而不是只证明若干选定性质——需要昂贵的人类指导。Coq 基于构造演算，自 1980 年代中期以来一直由 INRIA 开发，并已经能够完成大量验证推理。问题在于，它是否能验证真实系统。
Xavier Leroy 在 2006 年用 CompCert 回答了这个问题：这是一个针对 C 的相当大子集的已验证优化编译器。CompCert 中每个优化 pass 都伴随一个 Coq 证明，证明它保持程序语义——也就是编译输出与源程序具有相同可观察行为。CompCert 证明耗费数人年工作，包含大约 70,000 行 Coq。结果是一个以随机测试和代码审查无法提供的方式被测试过的编译器：形式证明每个优化都保持语义。CompCert 已经被部署在安全关键场景中，在那里编译器 bug 可能导致致命后果。
三年后，2009 年，Gerwin Klein 及其 NICTA（现为 CSIRO 的 Data61）同事宣布完成 seL4 验证，这是第一个经过数学验证的操作系统内核。seL4 是微内核——只提供基本服务的最小内核——其验证确立了 C 实现正确实现了 Haskell 规约，并且 Haskell 规约具有所需安全性质。该证明包含大约 200,000 行 Isabelle 脚本。seL4 已经运行在安全关键航空航天应用的生产系统中；在那里，操作系统 bug 的代价以生命衡量。
当代时期带来了成熟工具的发展，也带来了新方向。Lean 证明助手被重新设计为 Lean 4，并于 2021 年发布，吸引了大量数学家和软件工程师。HACL* library——用 F* 验证的密码学原语库，F* 是一种带自动验证的依赖类型语言——已经集成进 Firefox、Chrome 和 Linux 内核。Project Everest 是 Microsoft Research、INRIA 及其他机构的联合项目，产出了 TLS 1.3 的已验证实现。已验证软件的规模已经从单个算法增长到完整协议栈。
仍然开放的问题是：形式验证成本能否降低到足以使其成为常规实践，而不是例外。自动证明合成、证明修复，以及把 AI 辅助整合进证明工作流，都是活跃研究方向。当前大语言模型可以在 Lean 和 Coq 中生成证明草图，建议引理，并且有时能自动完成证明义务。这究竟会让形式验证成本降低两倍还是二十倍——以及这会如何改变形式验证软件与非形式测试软件之间的边界——是一个真正开放的问题。
规约、验证以及二者之间的技术
规约是什么，为什么写它很难
规约是对系统行为的数学描述。困难在于，大多数系统都是非形式地被规定的——通过散文式需求文档、API 文档，或开发团队共享理解。把非形式规约形式化确实很难。不是因为形式化在技术上困难，而是因为形式化过程会揭示：非形式规约原本是含糊的、不完整的，或内部不一致的。
形式规约必须回答非形式规约留下的问题。如果函数被用指定定义域之外的参数调用，会发生什么？网络分区时保证什么行为？如果两个客户端并发写入同一个 key，结果是什么？非形式规约经常让这类问题无人处理，依赖读者推断什么是“合理”行为。形式规约必须承诺一个答案，而做出这个承诺的过程常常揭示：不同利益相关者原本有不同期待。
规约语言在表达力和自动化之间提供不同取舍。TLA+ 使用集合论和时序逻辑——足以表达大多数分布式算法，并且能对有限实例进行模型检查自动化。Alloy 使用关系逻辑，并提供小模型的自动分析，在不要求证明的情况下揭示所声称性质的反例。Z 和 B 使用集合论记号，并支持基于精化的开发。Hoare logic 及其后继者——包括用于堆操作程序的 separation logic，以及用于共享内存并发程序的 concurrent separation logic——把规约表达为单个过程的前置条件和后置条件。时序逻辑（LTL、CTL、CTL*）规定随时间展开的系统性质——安全性质（“坏事永远不会发生”）和活性性质（“好事最终会发生”）。每种形式系统都适合不同系统和不同性质。
元教训是：规约充分性无法自动验证。一个内部一致、且实现满足的规约，如果没有捕捉利益相关者真正想要的东西，仍然可以是错的。规约的纪律——学习书写忠实捕捉意图的规约——来自实践，来自那种令人不适的过程：把既有非形式描述形式化，并发现它们比看起来更含糊。
模型检查：有限系统的穷尽验证
模型检查通过把系统表示为数学模型来工作——通常是 Kripke 结构，即一个有向图，节点是系统状态，边是转移——并检查模型中的每条路径是否满足某个时序性质。对于有限模型，这是可判定的：模型检查器会遍历所有可达状态和所有可能行为。对于性质 P 和模型 M，模型检查器要么产生 M 满足 P 的证书，要么产生一个反例——一条违反 P 的执行轨迹。
模型检查的力量在于，反例是具体执行轨迹，而不是抽象不可能性证明。当模型检查器报告一个分布式协议可能死锁时，它会给出导致死锁的具体消息和动作序列——这是协议设计者可以直接采取行动的信息。这种具体性，正是模型检查在硬件验证中立刻有用的原因；工程师可以拿着反例准确理解自己忽略了哪种电路行为。
根本限制是状态爆炸问题。一个拥有 n 个独立组件、每个组件有 k 个状态的并发系统，具有 k^n 个全局状态。如果 n = 100 且每个组件有 k = 2 个状态，那么状态空间有 2^100 个状态——远远超过任何计算机可以枚举的能力。管理状态爆炸的技术，是实践模型检查的核心：基于 BDD 的符号表示可以处理数百万状态；偏序归约利用这样一个事实，即独立事件的许多交错最终会到达同一状态；反例引导抽象精化从粗糙模型开始，并只在需要处精化；有界模型检查使用 SAT 求解器检查有限步数内的性质。每种技术都会扩展模型检查可处理系统的范围；但没有任何技术能消除对系统大小的根本指数依赖。
用于规约的时序逻辑，决定了哪些性质可以被表达，以及哪些算法适用。CTL（computation tree logic）规定分支时间性质——也就是对每个状态之后的可能未来进行量化的性质。LTL（linear temporal logic）规定线性时间性质——也就是对所有可能执行进行量化的性质。二者在表达力上不可比较：有些 CTL 性质没有 LTL 等价物，反之亦然。CTL 模型检查在模型大小上是多项式时间；LTL 模型检查是 PSPACE-complete 的。实践中，选择 CTL 还是 LTL，更多取决于哪些性质自然表达，以及有哪些工具可用，而不是复杂性理论本身。
定理证明：完整函数验证
模型检查可以自动处理有限系统。当系统是无限的——涉及无界数据结构，正确性性质对所有可能输入量化，或者规约是完整函数正确性陈述，而不是时序性质——定理证明就是合适技术。
形式化方法意义上的定理证明，是指交互式使用证明助手：人类书写证明脚本，系统检查每一步，最终产出一个机器验证证明，证明实现满足规约。这种交互劳动密集——一个较大系统的证明脚本可能有数十万行——但产出的是不会受到人类验证错误影响的正确性证书。
形式化方法中使用的证明助手大致分为两个家族。高阶逻辑（HOL）证明助手——Isabelle/HOL、HOL4、HOL Light——提供一种基础逻辑，即高阶谓词逻辑，并配有丰富的已证明数学和软件定理库。它们强调自动化：强大的 tactics、强大的 SMT 后端集成，以及大量预先证明的库，可以减少人类证明负担。依赖类型论证明助手——Coq、Lean、Agda——提供足够强的类型系统，可以直接在类型中表达规约，并通过 Curry-Howard 对应统一编程和证明。它们强调表达力，以及规约与实现的整合。
证明助手之间的选择，部分取决于应用领域，部分取决于共同体。seL4 使用 Isabelle/HOL 验证。CompCert 使用 Coq 验证。HACL* library 使用 F* 验证。每个选择都反映了工具优势和团队偏好。对学习者而言，实际建议是选择一个工具，深入学习，并认识到这些技能在不同工具之间有相当程度的迁移性。
Separation logic 由 John Reynolds、Samin Ishtiaq 和 Peter O’Hearn 在 2000 年代初发展出来，是使堆操作程序验证变得可处理的框架。经典 Hoare logic 要求在每个前置条件和后置条件中规定整个堆状态，这会产生随程序规模增长而难以扩展的规约。Separation logic 的 separating conjunction P * Q 断言 P 和 Q 分别在堆的不相交部分上成立，从而允许规约保持局部性：一个函数的规约只说它对自己的内存做什么，而不提堆的其余部分。这种局部性使得大型堆操作程序可以组合式验证，即隔离验证每个函数。Concurrent separation logic 把这一点扩展到并发程序，支持验证无数据竞争的共享内存程序，以及生产系统中使用的并发数据结构。
静态分析：有限性质的自动验证
静态分析在不需要人类书写规约或证明的情况下，自动检查程序性质；代价是它只能检查有限性质，并且可能报告误报。Patrick 和 Radhia Cousot 在 1977 年发展出的抽象解释提供了数学基础：程序会在一个抽象域上被分析，例如区间、凸多面体、类型；这个抽象域近似具体语义，而性质则在抽象域中被检查。抽象域中建立的每个性质都在具体域中成立（可靠性），但抽象域可能无法建立某些在具体层面成立的性质（不完备性）。
建立在抽象解释之上的现代静态分析器——Astrée（验证了 Airbus A380 飞控软件不存在运行时错误）、Frama-C（用于 C 程序）以及各种学术系统——可以为大型程序自动验证内存安全、整数溢出不存在以及其他性质。Facebook 的 Infer 是一个基于 separation logic 的静态分析器，可以扩展到数百万行代码库，并集成进大型科技公司的 CI 流水线，在 bug 进入生产环境前发现内存安全问题。
自动化和强度之间的取舍是根本性的。类型系统是轻量级静态分析——它们无需标注即可自动检查性质——但只能建立类型安全，不能建立函数正确性。模型检查更重，但能自动处理有限状态系统的时序性质。定理证明最重，能够处理无限系统的函数正确性，但需要大量人类努力。形式化方法实践的技艺，正在于让技术匹配性质：用类型系统处理它们擅长的普遍性质，用模型检查处理它擅长的并发与协议性质，用定理证明处理只有它才能建立的深层函数正确性性质。
学习这个主题会改变什么
形式化方法会实际改变实践者如何思考和构建软件，即使他们并不进行形式验证。
第一种变化，是规约纪律。书写形式规约，并发现非形式规约留下了什么未规定内容，这种经验会永久改变实践者处理规约的方式。形式化方法实践者阅读需求时会提出的问题是：这个边界情况会发生什么？当这两个操作并发时行为是什么？这个性质是安全性质还是活性性质？这些问题并不是因为正在应用形式化方法才被提出；而是因为形式化纪律使其重要性变得可见。结果是更清晰的需求、更好的 API 契约和设计更谨慎的系统。
第二种变化，是理解测试能确立什么、不能确立什么。测试展示的是被测试输入上 bug 的存在；它无法确立所有输入上 bug 的不存在。做过形式验证的实践者会内化这个区别，并发展出互补策略：在未发现 bug 代价最高处使用形式化方法，在形式化方法成本超过收益处使用测试，并且清楚理解哪些性质已经被形式证明，哪些只是被经验测试。
第三种变化，是进入形式验证工具。模型检查器、证明助手和静态分析器，是目前确立软件正确性性质的最强工具；使用它们需要理解其基础。学习过形式化方法的实践者，可以在实现前用 TLA+ 检查分布式协议设计，可以用证明助手验证关键安全性质，也可以阅读已验证系统组件附带的证明。这种进入能力，会使形式验证成为实践选项，而不是学术愿望。
第四种变化，是能够阅读形式验证文献。描述 CompCert、seL4、HACL* 和其他已验证系统的论文，是重要技术文档，展示了什么是可能的，以及它如何被完成。学习过形式化方法的实践者可以阅读这些论文，并理解哪些内容被验证了，哪些内容被假设了，使用了哪些技术——这些信息在决定是否基于已验证组件构建，或是否为新系统进行类似验证时都相关。
资源
书籍与文本
对于通过证明助手进行定理证明，Pierce 等人的 Software Foundations 系列（softwarefoundations.cis.upenn.edu 免费）是标准入口。第一卷 Logical Foundations 同时教授 Coq 和逻辑。第二卷 Programming Language Foundations 在 Coq 中形式化操作语义、类型系统和 Hoare logic——直接连接 §3.4。第三卷 Verified Functional Algorithms 延伸到算法验证。这个系列节奏良好、积极维护，习题会建立真正能力。对于偏好 Lean 的学习者，Theorem Proving in Lean 4（lean-lang.org 免费）和 Functional Programming in Lean（lean-lang.org/functional_programming_in_lean 免费）提供 Lean 对应路径。
对于 TLA+ 和分布式系统规约，Lamport 的 Specifying Systems（lamport.azurewebsites.net 免费）是由工具设计者撰写的权威参考。它系统发展 TLA+，并解释其设计选择背后的哲学理由。Wayne 的 Practical TLA+（Apress，2018）对工作工程师更易进入，用实践例子讲解 TLA+，不要求完整逻辑背景。对于想使用 TLA+、而不是从基础层面理解它的实践者，先读 Wayne 再读 Lamport 是最高效路径。
对于模型检查，Baier 和 Katoen 的 Principles of Model Checking（MIT Press，2008）是标准研究生教材。它覆盖 Kripke 结构、时序逻辑（LTL、CTL、CTL*）、模型检查算法、基于 BDD 的符号模型检查，以及偏序归约，并给出完整证明。Clarke、Grumberg 和 Peled 的 Model Checking（MIT Press，1999）是由该技术发明者撰写的更早标准参考，如今部分被 Baier-Katoen 取代，但仍然适合获得历史语境和原始视角。
Jackson 的 Software Abstractions（MIT Press，修订版，2012）通过 Alloy 教授形式规约。Alloy 是一种轻量级关系逻辑，带有自动分析器。Jackson 的观点是，多数系统应当在低于完整定理证明的抽象层级上被规定和分析——规定关键数据关系，并在小实例上检查，以在实现前发现设计错误。这种路径比完整验证更易进入，也能捕捉一大类设计 bug。
Chlipala 的 Certified Programming with Dependent Types（MIT Press，2013，在线免费）在 Coq 中发展较大程序的验证，超越 Software Foundations 的入门层级。完成 Software Foundations 并想验证非平凡系统的学习者，可以把它作为下一步。Bertot 和 Castéran 的 Interactive Theorem Proving and Program Development: Coq’Art（Springer，2004）是综合 Coq 参考，适合在基于 Coq 的工作中持续查阅。
Nipkow 和 Klein 的 Concrete Semantics with Isabelle/HOL（在线免费；Springer 纸质版付费）通过 Isabelle/HOL 教授编程语言语义、Hoare logic、抽象解释和编译器正确性。它是 Coq 路线中 Software Foundations 的最佳 Isabelle 对应文本，尤其适合想使用高阶逻辑证明助手、而不是依赖类型论证明助手的读者。
Leino 的 Program Proofs（MIT Press，付费）通过 Dafny 教授规约和程序验证。它比 Coq 或 Isabelle 文本更面向工程师：例子是带前置条件、后置条件、不变量和 SMT 辅助证明的可执行程序。限制在于，它专门教授 Dafny 风格，因此应当作为一般形式化方法基础的补充，而不是替代。
对于 Hoare logic 和 separation logic 的深入学习，Reynolds 的 Theories of Programming Languages（Cambridge，1998）提供基础处理。O’Hearn 关于 separation logic 的多篇论文——尤其是 2019 年图灵奖演讲 “Separation Logic”——是由开发者提供的最佳入门。
| 书籍 | 作用 | 类型 |
|---|---|---|
| Pierce 等，Software Foundations Vols. 1–3（免费） | 基于 Coq 的 FM 与验证标准入口 | 入门 |
| Lamport，Specifying Systems（免费） | 由设计者撰写的 TLA+ 经典参考 | 入门 |
| Wayne，Practical TLA+ | 面向工程师的 TLA+ 入门 | 入门 |
| Baier & Katoen，Principles of Model Checking | 标准模型检查教材 | 深入 |
| Clarke、Grumberg & Peled，Model Checking | 原始模型检查参考 | 参考 |
| Jackson，Software Abstractions（修订版） | 通过 Alloy 学轻量级形式化方法 | 入门 |
| Chlipala，Certified Programming with Dependent Types（免费）中的 Coq 验证章节 | 超越入门层级的 Coq 验证 | 入门 |
| Bertot & Castéran，Coq’Art | 综合 Coq 参考 | 参考 |
| Nipkow & Klein，Concrete Semantics with Isabelle/HOL（免费；纸质版付费） | 基于 Isabelle 的语义与验证 | 实践 |
| Leino，Program Proofs（付费） | 基于 Dafny 的程序验证 | 入门 |
课程与讲座
MIT 6.5840（Distributed Systems，原 6.824，材料免费）不是形式化方法课程，但其实验作业——实现 Raft、MapReduce 和容错键值存储——提供了 TLA+ 验证最有价值的分布式系统语境。实现分布式系统并用 TLA+ 规定它们，比只做其中任何一项都更有教育价值。
把 Software Foundations 系列当作自定节奏课程学习（把习题当作 problem sets），就是目前最好的免费形式验证课程之一。Coq 证明助手练习、Hoare logic 形式化和类型系统可靠性证明合在一起，覆盖了核心技术。
CMU 15-414/615（Bug Catching: Automated Program Verification and Testing）是一门研究生课程，材料免费，覆盖模型检查、基于 SMT 的验证、抽象解释和符号执行——它很好地补充了 Software Foundations 对定理证明的侧重。
OPLSS formal verification lectures（YouTube 免费）——尤其是 Adam Chlipala 关于 certified programming 的讲座、Andrew Appel 关于程序验证的讲座，以及若干关于 separation logic 的讲座——在研究生深度上覆盖高级形式化方法。
| 课程 | 平台 | 类型 |
|---|---|---|
| Software Foundations（Coq 练习，免费） | softwarefoundations.cis.upenn.edu | 实践 |
| CMU 15-414/615 Bug Catching（免费） | CMU 课程网站 | 深入 |
| OPLSS formal verification lectures（免费） | YouTube / OPLSS 网站 | 深入 |
| MIT 6.5840 Distributed Systems labs（免费） | MIT 课程网站 | 辅助 |
实践、工具与当前来源
工具就是这个主题本身。进入形式化方法必须动手；只阅读是不够的。
TLA+ Toolbox 或 VS Code TLA+ extension（可在 lamport.azurewebsites.net 免费获取）：安装工具，完成 Wayne 的 Practical TLA+ 教程，并为一个小型并发算法写 TLA+ 规约。看到模型检查器为一个看起来可信的不变量找到反例，是理解 TLA+ 有什么用的最直接方式。
Coq（coq.inria.fr 免费）搭配 Proof General Emacs 界面或 VSCoq for VS Code：安装后完成 Software Foundations 第二卷，并形式化 STLC 的类型可靠性证明。Coq 因为遗漏一个情形而拒绝证明的经验，会以阅读无法做到的方式使类型可靠性变得具体。
Alloy Analyzer（alloytools.org 免费）：安装后完成 Jackson 的 Software Abstractions 第 1–5 章，并建模一个小文件系统或通讯录。自动反例生成会让规约错误立即可见。
SPIN（spinroot.com 免费）是并发系统的标准模型检查器，其规约语言是 Promela。它尤其适合验证通信协议和并发算法。
Facebook 的 Infer（fbinfer.com 免费）展示了工业规模自动静态分析是什么样子。把 Infer 跑在一个已有 C 或 Java 代码库上，并检查其输出，比任何教程更有教育意义。
Dafny（免费）是最易进入的 SMT 辅助验证语言，适合用普通函数式和命令式代码学习程序证明。它会对规约、循环不变量和证明提示给出即时反馈，不需要学习者手动管理每一个证明步骤。Verus（免费）则把类似验证目标带到 Rust 系统代码中；对所有权、线性推理和低层验证感兴趣的读者值得关注，尽管它仍然是更高级且更年轻的生态。
CACM 文章 How AWS Uses Formal Methods 是 TLA+ 在分布式系统设计中的最佳短篇工业案例研究。它应当在完成第一个 TLA+ 教程之后阅读；那时学习者已经能识别为什么在实现前发现设计 bug 会改变可靠性的经济学。
Hillel Wayne 维护的 TLA+ tutorials（learntla.com，免费）质量很高，是 Wayne 书之外最易进入的 TLA+ 入门材料，覆盖书写 TLA+ 规约的常见模式和陷阱。
| 资源 | 平台 | 类型 |
|---|---|---|
| TLA+ Toolbox / VS Code TLA+ extension（免费） | lamport.azurewebsites.net | 实践 |
| Coq + Proof General 或 VSCoq（免费） | coq.inria.fr | 实践 |
| Alloy Analyzer（免费） | alloytools.org | 实践 |
| 用 SPIN 练习模型检查（免费） | spinroot.com | 实践 |
| Facebook Infer（免费） | fbinfer.com | 实践 |
| Dafny（免费） | dafny.org | 实践 |
| Verus（免费） | verus-lang.github.io | 辅助 |
| AWS，How AWS Uses Formal Methods（免费文章） | CACM / AWS | 辅助 |
| learntla.com——TLA+ tutorials（免费） | learntla.com | 入门 |
陷阱
| 陷阱 | 为什么会误导 | 更好的回应 |
|---|---|---|
| 把形式化方法当作绝对正确性的证明 | 一个形式验证系统，是相对于某个规约、针对某个环境模型、并在一组工具假设下被验证的。规约可能错误；模型可能没有捕捉真实世界条件；工具可能有 bug（尽管证明助手内核通常很小且维护谨慎）。不加限定地说一个系统“被证明正确”，具有误导性。 | 精确陈述验证主张：“CompCert 被验证为在 Coq 形式化的 C 语义假设下，生成与源代码具有相同行为的目标代码。”知道什么被验证了，什么被假设了，工具的可信计算基包含什么。诚实陈述主张，是形式化方法对工程文化最有价值的贡献之一。 |
| 跳过规约，直接奔向验证 | 有些学习者想立刻验证程序，却不愿投入时间书写规约。这颠倒了有效顺序：已验证程序满足其规约；如果规约没有捕捉想要的东西，验证就无法保证真正重要的内容。 | 在规约上投入与验证一样多的时间，甚至更多。为一个你很熟悉的系统写规约——一个并发队列、一个小协议——然后请同事寻找你的规约没有处理的情况。暴露出的缺口，比任何教程都更能教授规约。 |
| 只通过单一工具进入形式化方法 | TLA+ 不能与 Coq 互换，Coq 不能与 Alloy 互换，Alloy 不能与 SPIN 互换。每种工具适合不同系统的不同性质。只知道一个工具的实践者，会不顾适配性地使用它——例如用 TLA+ 做 Coq 更适合的完整函数验证，或用 Coq 做 TLA+ 更自然的协议检查。 | 至少学习来自不同范式的两个工具：一个用于模型检查或规约（TLA+、Alloy、SPIN），一个用于定理证明（Coq、Lean、Isabelle）。二者之间的对比，会让每个工具的强项和限制变得清楚；这是单一工具暴露无法提供的。 |
| 低估规约问题 | 多数形式验证失败其实是规约失败：实现满足规约，但规约没有捕捉意图。只关注验证技术、把规约当作简单准备工作的学习者，会对规约中实际包含多少困难感到意外。 | 做一些规约出错的练习：写一个规约，让模型检查器检查它，然后引入一个你相信应该成立的性质，并观察它被违反。违反处会揭示规约漏掉了什么。这个练习会建立阅读无法获得的规约直觉。 |
| 期待形式化方法普遍适用 | 完整函数验证很昂贵——CompCert 花费数人年的 Coq 证明工作；seL4 花费约 20 人年。对多数软件来说，这种成本并不合理。把形式化方法看作所有软件开发正确路径的学习者，会因为成本而失望，并得出形式化方法不实用的结论。 | 让技术匹配语境。类型检查免费，应该到处使用。静态分析（Infer、Coverity、Astrée）成本低，可以捕捉大量重要 bug。对协议设计做模型检查花费数天，可以在实现前捕捉设计错误。完整定理证明花费数人月，适合关键基础设施。学习完整谱系，并在合适层级应用它。 |
| 不接触主要已验证系统 | CompCert、seL4、HACL* 和 Project Everest 的已验证 TLS 实现，是形式化方法可以在规模上工作的存在性证明。只知道技术而不研究这些系统的学习者，会错过技术确实能产出东西的证明，也会错过使大规模验证变得可处理的设计决策和取舍。 | 阅读描述 CompCert（Leroy 2006、2009）和 seL4（Klein 等，2009）的论文。完成 Software Foundations 后，这些论文可以直接进入，并且会解释什么被验证了、花费多长时间、使用什么工具、证明结构是什么样子。这些论文以抽象技术描述无法做到的方式具体地令人受启发。 |