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

Appendix E: References and Further Reading Paths

Translation status: Partial. Reviewed against Japanese source commit 269d1c49b552 on 2026-07-19. Some content, headings, examples, tables, or references remain partially synchronized. Track the remaining work.

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 July 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 Read the Execution Guarantees

Listing a tool in this appendix does not mean that the repository executes or guarantees it. The sources of truth are tools/tool-manifest.json and the lane inventory in Appendix B. Alloy, TLC, Apalache, and Dafny run in pr-quick; SPIN, NuSMV, CBMC, Quint, PRISM, Tamarin, SymbiYosys, cvc5 / Carcara, and RTLola run in nightly; and Kani runs only through explicit optional/manual dispatch. Every other tool listed here is documentation-only: the book does not guarantee a pinned version, execution environment, or result for it.

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 / PRISM / SymbiYosys)

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)

NuSMV / nuXmv

PRISM (Probabilistic and Quantitative Model Checking)

SymbiYosys (Open-Source RTL Formal Verification)

Tamarin Prover (Symbolic Protocol Verification under an Active Adversary)

Runtime Verification (RTLola / MonPoly / RV-Monitor)

This comparison was rechecked against official repositories, distribution pages, and documentation on 2026-07-16. Although all three belong to runtime verification, stream specifications, metric temporal logic over logs, and Java instrumentation create different integration boundaries.

Candidate Primary integration form Observed official distribution and maintenance facts Decision for this book
RTLola Apply typed input/output streams and triggers to online or offline events rtlola-cli 0.1.2 crates.io package, offline CSV, JSON output, and upstream updates during 2025 were confirmed Selected. An immutable package digest, embedded commit and Cargo.lock, pinned Rust, and structured verdict can form one nightly contract
MonPoly Check timestamped logs against metric first-order temporal logic SourceForge lists 1.1.10 dated 2020-11-25 as the latest distribution Not selected here. It fits offline log monitoring, but this repository would still need a JSON-verdict, provenance, and current CI-maintenance contract
RV-Monitor Generate Java monitors from specifications and instrument an application The official GitHub repository has no release; the latest commit visible at review time was 2020-12-18; MIT license Not selected here. Java generation and instrumentation create a wider build and integration scope than replaying a fixed CSV teaching trace

RTLola was selected because it connected most narrowly to this repository’s pinned offline trace and structured-artifact contract, not because of a blanket feature ranking. This is not a claim that MonPoly or RV-Monitor is inferior; a different property language, instrumentation method, or operating platform can change the choice.

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

Rocq (formerly Coq)

Lean (Lean 4)

Logical Soundness, Completeness, and Semantics

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

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)

Independent rechecking of SMT proof certificates (Alethe / LFSC / DRAT / LRAT)

  • Execution boundary for the pinned example contract:
    • cvc5 1.3.4 is pinned to release tag cvc5-1.3.4, release commit f3b21c4483d3b88dc63cb7cd3e5eb092eee5e341, and official asset cvc5-Linux-x86_64-static.zip with SHA-256 dcdbfada0ce493ee98259c0816e0daafc561c223aadb3af298c2968e73ea39c6
    • Carcara 1.1.0 is referenced at the release level, but the compatibility commit pinned by cvc5’s contrib/get-carcara-checker is 394edbb15ba95c47893f1d821fddde7e016af178
    • The SHA-256 of that pinned source archive is 28562432ca7413a662d25f03e328cab4b7b9bf649b2ca69268a255a44a5ddee6
    • The build boundary for Carcara is the pinned Rust/Cargo 1.87.0 toolchain
  • The cvc5 1.3.4 Alethe documentation lists equality with uninterpreted functions, linear arithmetic, bit-vectors, and parts of strings, with or without quantifiers, as the currently supported area. This is not universal compatibility; check each solver/checker pair and logic fragment explicitly
  • The cvc5 1.3.4 release note says Alethe proof support was improved to full translation for the CPC fragment for logics in AUFNIRA. That is useful provenance, but not a basis for claiming blanket proof-format coverage
  • The cvc5 LFSC documentation says there is basic support over all supported theories, while also warning that unsupported internal proof rules may be printed as trust steps. In a strict checking pipeline, unresolved trust steps are non-success
  • DRAT and LRAT are propositional CNF proof ecosystems. They validate unsatisfiability of the post-encoding CNF problem, not directly the original SMT problem, the source specification, the encoder, or omitted assumptions
  • Primary sources:

6) Distributed-Systems Theory (CAP / FLP and Changed Assumptions)

7) Industrial Case Studies and Adoption Evidence

Paris Metro Line 14 (B-Method)

Amazon s2n (verification of a cryptographic implementation)

Industrial use of TLA+

8) 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.