English
Formal methods use mathematical descriptions to specify systems and establish properties of their behavior. A specification states the requirement, a model describes the system, and a verification argument connects them. The model may be source code, a transition system, or an abstract design. The connection between that model and the deployed system is part of the reasoning that must remain visible.
Consider two workers updating a shared counter. Each reads zero, adds one locally, and writes one back. Two increments have occurred, but the final value is one. A test might miss that interleaving. A model checker can search the permitted interleavings; a program proof can establish conditions under which the implementation preserves the intended count. Both need a definition of which actions are atomic.
Testing, model checking, static analysis, and theorem proving answer overlapping questions with different costs and guarantees. Exhaustive testing is possible for a sufficiently small finite input space; sampled tests usually cover only some executions. Formal reasoning can cover an entire modeled family of executions, while testing can expose problems in assumptions, environments, and implementations outside that model. The useful starting point is a specific property, not a competition among techniques.
From Program Correctness to Industrial Verification
Floyd’s work on program assertions and Hoare’s 1969 logic made correctness claims precise enough to derive from program structure. Loop invariants described what remains true across iterations. Dijkstra’s predicate-transformer approach connected desired outcomes to the conditions needed before execution. These developments made program construction and mathematical reasoning interact more directly; they did not remove the need to choose a suitable specification.
The LCF approach addressed another problem: how to trust a large interactive prover. Powerful tactics could search for proofs, but theorem values could be created only through a small collection of trusted inference operations. ML was developed in this proof-management setting. The HOL project’s history explains how this architecture used the programming language’s type abstraction to protect theorem construction. Search could evolve without making every search heuristic part of the logical foundation.
Model checking emerged in the early 1980s through work by Clarke and Emerson and by Queille and Sifakis. Finite-state systems could be checked algorithmically against temporal properties. Symbolic representations such as binary decision diagrams, followed by SAT-based techniques, allowed more systems to be explored without listing every state explicitly. They reduced some representation costs, while state-space growth remained a central difficulty.
Industrial examples demonstrate different scopes of verification. CompCert proves semantic preservation for its verified compiler passes between specified source and target representations; this is not a proof of every frontend, assembler, or deployed execution environment. The original seL4 functional-correctness work connected its C implementation to an abstract specification through intermediate models. Security properties require their own definitions and arguments. AWS’s report on TLA+ describes finding design errors by checking system models. These cases teach different ways to choose a tractable and useful verification target.
Specification, Verification, and the Techniques Between Them
Keep three things separate: the behavior the specification allows, the behavior the model describes, and the evidence that the latter stays within the former. A specification may deliberately permit several implementations. Refinement then means reducing the permitted behavior while preserving the required guarantees, rather than reproducing one prescribed execution exactly.
What Specifications Are and Why Writing Them Is Hard
A useful specification states relationships, including what may remain unchanged. For a transfer of amount a between two accounts, conservation of the total balance is necessary but insufficient: doing nothing also conserves it. A successful transfer should decrease the source by a, increase the destination by a, and preserve unrelated accounts. Preconditions or explicit failure cases must address insufficient funds, invalid amounts, and authorization where those belong to the system’s requirements.
An invariant holds initially and is preserved by every permitted step. To prove that a balance never becomes negative, establish it at initialization and show that every operation, including failure and concurrent cases, preserves it. Merely observing that the final balance is nonnegative does not establish the invariant throughout execution.
Safety rules out a bad event, such as two processes owning the same exclusive lock. Liveness requires progress, such as every accepted request eventually receiving a response. A system that never accepts a request might satisfy a poorly written implication vacuously. A system that stops forever can satisfy many safety properties while violating progress. Liveness arguments often need fairness assumptions: an enabled process cannot be ignored indefinitely by the scheduler.
Check the specification itself by asking for examples and counterexamples. Does any initial state satisfy it? Can a normal operation complete? Does a deliberately broken implementation satisfy it anyway? An inconsistent precondition makes any implication from it true, while an overly weak postcondition admits unwanted behavior. Finding these errors early is one of the practical benefits of formalization.
Model Checking: Exhaustive Verification of Finite Systems
A finite-state model consists of states, initial states, and allowed transitions. To check an invariant, a model checker explores reachable states and tests the property. In the counter example above, it can produce the trace read₁(0), read₂(0), write₁(1), write₂(1). The trace explains the failure more directly than a bare “false.” Replacing each read-modify-write sequence with one atomic increment removes that interleaving from this model; whether the implementation provides that atomicity is a separate obligation.
Temporal properties concern paths through the graph. LTL describes properties along a path, such as “every request is eventually followed by a response”; standard LTL model checking requires the property on all system paths. CTL combines temporal operators with explicit path quantifiers, allowing distinctions such as “from each reachable state, some recovery path exists.” The ability to recover on some path does not mean every scheduled execution will recover.
A finite graph can have infinitely long executions because it contains cycles. Algorithms analyze the graph and suitable acceptance conditions; they do not literally enumerate all infinite runs. State explosion arises because independent components multiply the number of possible combined states. Symbolic representations, partial-order reductions, symmetry, and abstraction can reduce the work when their conditions apply.
Bounded model checking asks about executions up to a chosen depth. Finding no counterexample within that depth is not generally an unbounded proof, unless a completeness argument supplies a sufficient bound. Likewise, checking a fixed number of processes establishes the property for that model size; extending it to arbitrary numbers requires another argument. These qualifications identify the exact result obtained, while the counterexamples remain useful for finding real design errors.
Theorem Proving: General Properties and Checked Evidence
Theorem proving can establish a property for an unbounded family of inputs through a finite argument. To verify a summation loop, for example, use an invariant connecting the accumulator to the prefix already processed. Initialization establishes the empty-prefix case; one iteration extends the prefix and adds its next element; termination connects the invariant to the desired full sum. If the arithmetic uses bounded machine integers, the specification must also address overflow.
A proof assistant checks the formal argument. Tactics may automate steps, SMT solvers may discharge selected obligations, and libraries may supply reusable lemmas. The resulting guarantee depends on the statements checked, the axioms assumed, and the checking architecture. A small trusted kernel reduces the part of the system that must implement logical inference correctly; it does not make the specification, hardware, or every imported claim automatically trustworthy.
Induction handles arbitrarily long lists or executions by proving a base case and a general step. Refinement proofs relate implementations at different levels, and separation logic supports local reasoning about memory. These techniques help divide a large verification into reusable obligations. Proof maintenance remains engineering work: a changed representation or requirement can invalidate an earlier lemma or its applicability.
Static Analysis: Automated Verification of Limited Properties
Static analysis reasons about programs without executing each concrete case. Abstract interpretation makes one approach precise: compute over descriptions of sets of states. An interval analysis may record x ∈ [0,10] instead of eleven separate possible values. Sound transfer operations ensure that the abstract result includes every concrete result represented by the input.
Approximation loses information. If x and y are always equal and both lie in [0,10], independent intervals may give x−y ∈ [−10,10], although the actual difference is always zero. An alarm about a negative result can therefore be spurious. A relational domain that records x=y can eliminate it, at greater analysis cost. This example explains the tradeoff between precision and tractability without treating every warning as either a real bug or a useless result.
For a sound analysis of a stated property, absence of an alarm supports that property within the model. Some industrial analyzers deliberately sacrifice soundness or analyze only selected paths, so their guarantees differ. Annotations, contracts, and assumptions about external calls also matter. “Static” describes when and how the analysis operates; it does not by itself specify what has been proved.
What Studying This Changes
The practical change is to ask for a precise claim and an inspectable justification. “Verified” becomes incomplete information until the property, model, assumptions, and checked artifact are named. This also makes a small verification useful: a clear invariant for a critical component can be more actionable than an ambitious claim about an unspecified whole system.
Start by modeling the two-worker counter, obtaining a failing trace, and changing the atomicity assumption. Then write and check a loop invariant for a small sequential program. Compare what each exercise establishes and which implementation details remain outside it. The comparison gives a concrete basis for choosing a technique on a larger project.
Resources
Books and Texts
Software Foundations provides a Rocq/Coq-based sequence: Logical Foundations for logic and proof construction, Programming Language Foundations for semantics, types, and Hoare logic, and Verified Functional Algorithms for algorithm verification. For Lean, Theorem Proving in Lean 4 teaches the proof environment, while Functional Programming in Lean teaches programming. They cover different parts of the preparation and are not interchangeable verification curricula.
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 one 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 teaches relational specification through Alloy. Modeling a small address book or file system lets you examine how constraints interact and find counterexamples within a chosen scope. This provides specification practice without first constructing a full implementation proof.
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 a possible 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 teaches semantics, Hoare logic, abstract interpretation, and compiler correctness through Isabelle/HOL. It offers a higher-order-logic route alongside the dependent-type-based Rocq/Coq materials. The formal definitions and exercises make the differences between the foundations concrete.
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.
Reynolds’s Theories of Programming Languages develops program reasoning. For separation logic, use his 2002 survey paper, Separation Logic: A Logic for Shared Mutable Data Structures, and related work by O’Hearn and collaborators. Follow a local heap example through the separating conjunction and frame rule before studying larger verification systems.
| 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.
Software Foundations can also serve as a self-paced course. Complete the proof exercises rather than only reading completed solutions, and keep a record of the invariants, induction hypotheses, and helper lemmas needed for each result.
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
Use a tool to check a property you can state precisely. Begin with a small model, inspect a counterexample, and revise either the design or the specification based on what the trace shows. Record which change actually removes the failure.
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 gives a concrete example of 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.
Infer demonstrates automated analysis of program properties. Run it on a supported small code example with a known defect, then inspect both the reported issue and a corrected version. Consult the selected analysis’s assumptions before interpreting a clean report as a guarantee.
Dafny combines executable code with specifications, loop invariants, and SMT-assisted verification. Verus supports verification of Rust programs. Their examples provide ways to practice writing obligations and interpreting verification failures; follow each project’s documentation for the supported language subset and trusted interfaces.
The article How AWS Uses Formal Methods describes using TLA+ to examine distributed-system designs. Read it after a small modeling exercise and identify what was modeled, which properties were checked, and how the results influenced the design.
Learn TLA+ (learntla.com), by Hillel Wayne, provides tutorials and modeling examples. Reproduce an example, introduce a deliberate error, and explain the counterexample before extending the model.
| 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 |
|---|---|---|
| Proving an incomplete requirement | Conservation alone permits a transfer that does nothing. | Check the intended input-output relation and deliberately broken implementations. |
| Equating safety with progress | A stopped system can avoid every forbidden event. | State liveness properties and the fairness assumptions they need. |
| Treating bounded exploration as a general proof | Unchecked depths or larger configurations may behave differently. | Report bounds and provide a completeness or generalization argument if available. |
| Confusing a checked design model with verified deployed code | The model-to-implementation connection may remain informal. | Identify each translation and environmental assumption. |
| Treating every static warning as a real execution | Overapproximation may introduce impossible states. | Inspect the abstract domain and refine the model when needed. |
| Assuming machine-checked proofs need no trust analysis | Kernels, axioms, specifications, and interfaces still determine the claim. | Inspect the checked statement and its dependencies. |
中文
形式化方法使用数学描述来规定系统，并建立其行为性质。规约陈述要求，模型描述系统，验证论证连接二者。模型可以是源代码、转移系统或抽象设计。模型与实际部署系统之间的联系，也是必须明确保留的论证内容。
考虑两个工作线程更新共享计数器：它们各自读到零，在本地加一，再把一写回。发生了两次递增，最终值却是一。测试可能错过这种交错；模型检查器可以搜索允许的交错，程序证明则可以建立实现在哪些条件下维持预期计数。二者都需要明确哪些动作是原子的。
测试、模型检查、静态分析和定理证明会回答相互重叠的问题，但成本与保证不同。足够小的有限输入空间可以穷尽测试；抽样测试通常只覆盖部分执行。形式推理可以覆盖模型中的整族执行，测试则可以暴露模型之外的假设、环境与实现问题。有用的起点是一项具体性质，而不是给这些技术排高低。
从程序正确性到工业验证
Floyd 关于程序断言的工作，以及 Hoare 在 1969 年提出的逻辑，使正确性主张精确到能够依据程序结构进行推导。循环不变式描述迭代过程中持续成立的性质；Dijkstra 的谓词变换方法把预期结果与执行前所需条件联系起来。这些发展让程序构造与数学推理更直接地配合，但没有免除选择合适规约的责任。
LCF 方法处理另一个问题：怎样信任一个庞大的交互式证明器？功能丰富的策略可以搜索证明，但定理值只能通过一小组可信推理操作产生。ML 正是在这种证明管理需求中发展起来的。HOL 项目的历史解释了这种结构怎样利用编程语言的类型抽象保护定理构造。搜索方法可以演进，而不必把每种搜索启发式都纳入逻辑基础。
模型检查在二十世纪八十年代初形成，相关工作包括 Clarke 与 Emerson，以及 Queille 与 Sifakis 的研究。有限状态系统能够针对时序性质进行算法检查。二叉决策图等符号表示，以及后来的基于 SAT 的技术，使更多系统能够在不显式列出全部状态的情况下得到探索。它们降低了一些表示成本，但状态空间增长仍是核心困难。
工业案例展示了不同的验证范围。CompCert证明其已验证编译阶段在指定源表示与目标表示之间保持语义，并不是证明每个前端、汇编器或部署环境都正确。seL4 最初的功能正确性工作通过中间模型，把 C 实现连接到抽象规约；安全性质需要各自的定义与论证。AWS 的 TLA+ 报告则描述了通过检查系统模型发现设计错误的实践。这些案例提供了选择可处理且有用的验证目标的不同方法。
规约、验证以及二者之间的技术
需要分清三件事：规约允许的行为，模型描述的行为，以及后者没有超出前者的证据。规约可以有意允许多种实现。精化意味着在维持所需保证的同时收窄允许的行为，而不是精确复现某一次指定执行。
规约是什么，为什么写它很难
有用的规约陈述各种关系，包括哪些部分应保持不变。把金额 a 从一个账户转到另一个账户，总余额守恒是必要条件，却不是充分条件：什么都不做也守恒。成功转账应使来源账户减少 a、目标账户增加 a，并保持无关账户不变。对于余额不足、无效金额，以及属于系统需求的授权问题，需要前置条件或明确的失败情况。
不变式在初始状态成立，并被每个允许步骤保持。要证明余额永不为负，应先证明初始化满足它，再证明每个操作，包括失败与并发情况，都保持它。仅观察最终余额非负，并不能建立整个执行中的不变式。
安全性排除坏事件，例如两个进程同时持有同一把排他锁。活性要求取得进展，例如每个已接受的请求最终都得到响应。一个从不接受请求的系统，可能空洞地满足写得不好的蕴涵条件；一个永远停止的系统，也可能满足许多安全性条件却没有进展。活性论证通常需要公平性假设，例如调度器不能无限期忽略某个持续可执行的进程。
通过寻找例子与反例检查规约本身：是否存在满足它的初始状态？正常操作能否完成？刻意写错的实现是否仍然满足它？相互矛盾的前置条件会使从它推出的任意蕴涵为真；过弱的后置条件则允许不想要的行为。尽早发现这些错误，是形式化的实际收益之一。
模型检查：有限系统的穷尽验证
有限状态模型包含状态、初始状态和允许的转移。检查不变式时，模型检查器探索可达状态并检查性质。在前面的计数器例子中，它可以产生轨迹 read₁(0), read₂(0), write₁(1), write₂(1)。这条轨迹比一个简单的“假”更直接地解释失败。把每个读—改—写序列替换成一次原子递增，会在这个模型中排除该交错；实现是否提供这种原子性，则是另一项论证责任。
时序性质描述图中的路径。LTL 表达一条路径上的性质，例如“每个请求最终都得到响应”；标准 LTL 模型检查要求性质在系统的所有路径上成立。CTL 把时序算子与显式路径量词结合起来，能够表达“从每个可达状态出发，都存在某条恢复路径”等区别。某条路径可以恢复，并不意味着每种调度下的执行都会恢复。
有限图也可以因为包含环而产生无限长执行。算法分析图及适当的接受条件，并不逐条枚举所有无限运行。状态爆炸来自独立组件可能状态数的相乘。符号表示、偏序归约、对称性与抽象，在满足相应条件时可以减少工作。
有界模型检查询问指定深度以内的执行。该深度内没有找到反例，一般不等于无界证明，除非另有完备性论证给出充分深度。同样，检查固定数量的进程，只能建立该模型规模的性质；推广到任意数量需要额外论证。这些限定明确了实际得到的结果，而找到的反例仍然有助于发现真实的设计错误。
定理证明：一般性质与可检查的证据
定理证明可以通过有限论证，建立无界输入族的性质。例如，验证求和循环时，可以用不变式连接累加器与已经处理的前缀。初始化建立空前缀情况；一次迭代扩展前缀，并加上下一元素；终止时，不变式连接到所需的完整求和结果。如果使用有界机器整数，规约还必须处理溢出。
证明助手检查这个形式论证。策略可以自动完成步骤，SMT 求解器可以解决部分义务，库可以提供可复用的引理。得到的保证依赖实际检查的陈述、采用的公理与检查结构。较小的可信内核减少了必须正确实现逻辑推理的系统部分，但不会使规约、硬件或每个导入的主张自动可信。
归纳法通过基本情况与一般步骤，处理任意长的列表或执行。精化证明连接不同层次的实现；分离逻辑支持关于内存的局部推理。这些方法帮助把大型验证分解为可复用的义务。维护证明仍然是工程工作：表示或需求改变时，既有引理或其适用性也可能失效。
静态分析：有限性质的自动验证
静态分析不逐一执行所有具体情况，而是直接推理程序。抽象解释把其中一种方法精确化：在状态集合的描述上计算。区间分析可以记录 x ∈ [0,10]，而不分别保存十一个可能值。可靠的转移操作确保抽象结果包含输入所代表的所有具体结果。
近似会丢失信息。如果 x 与 y 始终相等，且都在 [0,10] 中，分别保存区间可能得到 x−y ∈ [−10,10]，实际差值却始终为零。因此，关于负结果的警告可能是伪警报。记录 x=y 的关系型抽象域可以消除它，但分析成本更高。这个例子解释了精度与可处理性之间的取舍，不必把每个警告都当成真实缺陷或无用结果。
对于针对指定性质的可靠分析，没有警报可以支持该性质在模型内成立。一些工业分析器会有意牺牲可靠性，或只分析部分路径，其保证因此不同。注解、契约与关于外部调用的假设也很重要。“静态”描述分析何时、怎样进行，本身并没有说明已经证明了什么。
学习这个主题会改变什么
实际的改变，是要求一个精确主张，以及可以检查的论证。只说“经过验证”并不足够，还需指明性质、模型、假设和检查产物。这也使小范围验证具有价值：关键组件的一条明确不变式，往往比针对未说明范围的整个系统提出宏大保证更便于使用。
可以先建立双线程计数器模型，得到失败轨迹，再修改原子性假设。随后，为一个小型顺序程序编写并检查循环不变式。比较两项练习分别建立了什么、哪些实现细节仍在范围之外。这种比较为较大项目选择方法提供具体依据。
资源
书籍与文本
Software Foundations 提供基于 Rocq/Coq 的学习顺序：Logical Foundations 教逻辑与证明构造，Programming Language Foundations 教语义、类型和 Hoare 逻辑，Verified Functional Algorithms 教算法验证。Lean 方面，Theorem Proving in Lean 4 教证明环境，Functional Programming in 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 通过 Alloy 教授关系规约。建立小型地址簿或文件系统模型，可以检查约束之间的相互作用，并在选定范围内寻找反例。这提供了规约练习，不必先构造完整实现的证明。
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 通过 Isabelle/HOL 教授语义、Hoare 逻辑、抽象解释和编译器正确性。它提供高阶逻辑路线，可与基于依赖类型的 Rocq/Coq 材料对照。形式定义与练习使基础之间的区别变得具体。
Leino 的 Program Proofs（MIT Press，付费）通过 Dafny 教授规约和程序验证。它比 Coq 或 Isabelle 文本更面向工程师：例子是带前置条件、后置条件、不变量和 SMT 辅助证明的可执行程序。限制在于，它专门教授 Dafny 风格，因此应当作为一般形式化方法基础的补充，而不是替代。
Reynolds 的 Theories of Programming Languages 讨论程序推理。学习分离逻辑时，可使用他的 2002 年综述论文 Separation Logic: A Logic for Shared Mutable Data Structures，以及 O’Hearn 与合作者的相关工作。先用局部堆的例子推演分离合取和框架规则，再研究较大的验证系统。
| 书籍 | 作用 | 类型 |
|---|---|---|
| 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 也可以作为自学课程。应完成证明练习，而不只阅读已有解答，并记录每项结果所需的不变式、归纳假设和辅助引理。
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。它尤其适合验证通信协议和并发算法。
Infer 展示对程序性质的自动分析。可以在一个受支持、具有已知缺陷的小代码例子上运行它，再检查报告与修正后的版本。把无警报报告解释为保证之前，应查明选定分析采用的假设。
Dafny 把可执行代码与规约、循环不变式、SMT 辅助验证结合起来。Verus 支持 Rust 程序验证。它们的例子提供了编写证明义务和解释验证失败的练习；应按照项目文档了解支持的语言子集与可信接口。
How AWS Uses Formal Methods 描述了使用 TLA+ 检查分布式系统设计的实践。可以在完成小型建模练习后阅读，识别建模对象、检查的性质，以及结果怎样影响设计。
Hillel Wayne 的 Learn TLA+（learntla.com）提供教程与建模例子。可以复现例子，刻意引入错误，并在扩展模型前解释所得反例。
| 资源 | 平台 | 类型 |
|---|---|---|
| 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 | 入门 |
陷阱
| 陷阱 | 为什么会误导 | 更好的做法 |
|---|---|---|
| 证明不完整的需求 | 仅要求守恒，允许转账什么都不做。 | 检查预期输入输出关系，并尝试刻意写错的实现。 |
| 把安全性等同于进展 | 停止的系统可以避免所有禁止事件。 | 写出活性性质及其所需的公平性假设。 |
| 把有界探索当成一般证明 | 未检查的深度或更大配置可能行为不同。 | 报告边界；有完备性或推广论证时一并给出。 |
| 混淆已检查的设计模型与已验证的部署代码 | 模型到实现的联系可能仍是非形式的。 | 指明每次转换与环境假设。 |
| 把每个静态警报都当成真实执行 | 过近似可能引入不可能出现的状态。 | 检查抽象域，必要时细化模型。 |
| 认为机器检查的证明不再需要分析信任范围 | 内核、公理、规约与接口仍然决定主张范围。 | 检查实际证明的陈述及其依赖。 |