Formal Methods: Foundations and Applications
日本語
  1. Home
  2. Appendices
  3. Appendix e: references and further reading paths

Appendix E: References and Further Reading Paths

This appendix is a reader-facing guide to primary sources for the methods, tools, and case studies introduced in the main text. Use it when you want to deepen a chapter, verify a claim against an official source, or decide which tool family to study next.
As of January 2026, it reflects naming changes and current mainstream references such as Coq → Rocq, CVC4 → cvc5, the Alloy 6 series, and Apalache in the TLA+ ecosystem.

How to Use This Appendix

  • After a specific chapter: start with the entry that names the chapter you just finished, then follow the official site before the release page or mirror.
  • When evaluating a tool: read the purpose line first, then jump to the official site or repository to confirm current installation, release, and documentation details.
  • When citing the book in engineering work: prefer the primary or quasi-primary links here over secondary summaries, especially for tool capabilities, case studies, and reported results.
  • When planning a second pass through the book: use the reading paths below to choose between modeling, model checking, theorem proving, program verification, and industrial adoption.

Fast Reading Paths

  • Learn lightweight modeling first: Chapter 4 → Alloy → Chapter 8 for counterexample-oriented thinking.
  • Strengthen concurrency and distributed-systems reasoning: Chapter 7 → TLA+ / TLC → Apalache → industrial TLA+ case studies.
  • Move from proofs to mechanized assurance: Chapter 9 → Rocq or Lean → Chapter 10 for program-verification payoff.
  • Evaluate tools for engineering adoption: Chapters 10–12 → Dafny / CBMC / SPARK / Z3 / cvc5.
  • Study business-facing evidence: Chapter 13 → Paris Metro Line 14, Amazon s2n, and industrial TLA+ reports.

How Sources Were Chosen

  • Reported values (measurements / case data): cite primary or quasi-primary sources such as papers, official blogs, or official reports.
  • Illustrative examples: mark them as examples so readers do not mistake them for generally established values.
  • Uncertain estimates: avoid them where possible. If one is unavoidable, state that it is uncertain and record the assumptions, including scope and measurement conditions.

1) Specification Languages and Modeling Tools (Alloy / TLA+ / Z / CSP)

Alloy (Alloy 6.x)

TLA+ (TLC)

Z (Z notation)

  • Purpose: rigorously describing state-based specifications with sets, relations, and mappings so they can serve as a basis for review and verification
  • Best after reading: Chapter 5, “State-Based Specification — Fundamentals of Z Notation”
  • Primary sources (implementations and tools):

CSP

  • Purpose: handling communication, synchronization, deadlock, and related properties in concurrent processes
  • Best after reading: Chapter 6, “Process-Centric Specification — Concurrency with CSP”
  • Primary sources (tool example):

2) Model Checking and State-Space Exploration (TLC / Apalache / SPIN / NuSMV)

Apalache (Additional checking for TLA+, SMT-based)

  • Purpose: checking properties of TLA+ specifications through SMT-based exploration and constraint solving, as a complement to TLC
  • Best after reading: Chapter 7, “Specifying Time — Introduction to TLA+”; Chapter 8, “Introduction to Model Checking”; Chapter 12, “Tools and Automation”
  • Primary sources:

SPIN (Promela)

  • Purpose: model checking of concurrent systems written in Promela, including counterexample traces
  • Best after reading: Chapter 6, “Process-Centric Specification — Concurrency with CSP”; Chapter 8, “Introduction to Model Checking”
  • Primary sources:

NuSMV

  • Purpose: model checking over state-transition models, including CTL and LTL
  • Best after reading: Chapter 8, “Introduction to Model Checking”
  • Primary sources:

3) Theorem Proving and Proof Assistants (Rocq / Lean / Isabelle / Agda)

Rocq (formerly Coq)

  • Purpose: proof assistance based on type theory and kernel checking, together with integrated development of proofs and programs
  • Best after reading: Chapter 9, “Fundamentals of Theorem Proving”
  • Primary sources:

Lean (Lean 4)

Isabelle

  • Purpose: proof assistance with Isabelle/HOL and related environments, proof documentation, and tool integration
  • Best after reading: Chapter 9, “Fundamentals of Theorem Proving”
  • Primary sources:

Agda

  • Purpose: theorem proving and program description based on dependent types
  • Best after reading: Chapter 9, “Fundamentals of Theorem Proving”, as auxiliary context for type theory
  • Primary sources:

4) Program Verification and Static Assurance (Dafny / Frama-C / CBMC / VeriFast / SPARK)

Dafny

  • Purpose: integrating specification and verification through contracts and automated checking based on SMT
  • Best after reading: Chapter 10, “Program Verification”; Chapter 12, “Tools and Automation”
  • Primary sources:

Frama-C

  • Purpose: static analysis and verification for C, including annotations and plugins
  • Best after reading: Chapter 10, “Program Verification”
  • Primary sources:

CBMC

  • Purpose: bounded model checking for C and C++, including bug finding, safety checking, and assertions
  • Best after reading: Chapter 8, “Introduction to Model Checking”; Chapter 10, “Program Verification”
  • Primary sources:

VeriFast

  • Purpose: verification based on separation logic for languages such as C and Java
  • Best after reading: Chapter 10, “Program Verification”
  • Primary sources:

SPARK (Ada)

  • Purpose: contracts, static analysis, and proof for high-assurance Ada development, especially in safety-critical contexts
  • Best after reading: Chapter 11, “Integrating Formal Methods into Development Processes”; Chapter 12, “Tools and Automation”
  • Primary sources:

5) SMT Solvers and Verification Backends (Z3 / cvc5)

Z3

  • Purpose: a foundation for constraint solving and automated reasoning, often used as a backend for verifiers
  • Best after reading: Chapter 10, “Program Verification”; Chapter 12, “Tools and Automation”
  • Primary sources:

cvc5 (successor to the CVC line, formerly CVC4)

6) Industrial Case Studies and Adoption Evidence

Paris Metro Line 14 (B-Method)

Amazon s2n (verification of a cryptographic implementation)

Industrial use of TLA+

7) AI and Formal Methods (Further Reading and Boundaries)

Use this section after Chapters 9–12 if you want to separate promising AI-assisted workflows from assurance mechanisms that remain fundamentally non-negotiable.
LLMs are useful for drafting specifications, proofs, and counterexample interpretations and for assisting exploration. They are not, however, a source of final assurance. This book recommends treating LLM output as untrusted input and always closing the loop with mechanical verification such as model checking, type checking, or SMT-based verification.