Glossary
Translation status: Partial. Reviewed against Japanese source commit
ef10023d987aon 2026-07-19. Some content, headings, examples, tables, or references remain partially synchronized. Track the remaining work.
This glossary collects technical terms and abbreviations that appear repeatedly throughout the book. The definitions prioritize the way each term is used in this book. When stricter distinctions matter, refer to the appendices or to primary sources.
How to Use This Glossary
This glossary is designed for fast re-entry. If you return to the book after a break, use it to recover the meaning of a term, re-establish the distinction between similar ideas, and jump back to the relevant chapter. Definitions are kept short on purpose. When the technical boundary matters, the listed chapter should be treated as the primary explanation. Use Appendix B when the term is mainly about tool setup, Appendix C when the issue is notation, and Appendix E when you need primary sources.
0) Acronyms
- SAT: Satisfiability. The satisfiability problem for propositional logic. Some tools such as Alloy reduce internal checks to SAT solving.
- SMT: Satisfiability Modulo Theories. A framework that combines satisfiability checking with theories such as equality, arithmetic, and arrays.
- LTL / CTL: Linear Temporal Logic and Computation Tree Logic. Temporal logics used to describe properties in model checking.
- DTMC / CTMC / MDP: Discrete-time Markov chain, continuous-time Markov chain, and Markov decision process. In PRISM they respectively represent step probabilities, transition rates, and nondeterministic choices followed by probability distributions.
- PCTL / CSL: Temporal logics for probabilistic reachability, timing, and long-run properties. PCTL is a basis for reading DTMC / MDP properties, while CSL serves the corresponding role for CTMCs.
- CI: Continuous Integration. Automated validation gates used for pull requests, nightly checks, and release preparation.
- HOL: Higher-Order Logic. A family of logics used by systems such as Isabelle/HOL.
- RMW: Read-Modify-Write. A common concurrent update pattern that can lead to lost updates.
A
Abstraction: The act of omitting details in order to focus on the properties relevant to reasoning or verification. A useful model is abstract enough to be analyzable but concrete enough to preserve the question being asked. See Chapters 3, 4, and 8.
Attack trace: A violating trace containing adversary knowledge, message operations, and protocol events. In tools such as Tamarin, it is the retained explanation for a falsified lemma. See Chapter 13 and Appendix C.
Alloy: A representative lightweight formal-methods tool. It combines a relational modeling language with an analyzer that searches for counterexamples. See Chapter 4.
Alethe: An SMT proof-certificate format in the SMT-LIB ecosystem. It is
used to exchange unsat certificates from proof-producing solvers to
independent checkers or reconstruction frameworks such as Carcara. Coverage and
compatibility are tool-pair specific. See Chapter 12 and Appendix E.
Apalache: An SMT-based checker for TLA+ specifications. It is useful when you want symbolic or bounded exploration in addition to TLC’s explicit-state model checking. See Chapters 7, 8, and Appendix B.
Assume / assert / cover (RTL formal): assume restricts the environment
traces under analysis, assert states a property that must not fail on those
traces, and cover searches for one trace reaching a condition. Review
over-strong assumptions for vacuity, and do not interpret cover reachability as
a safety proof. See Chapter 8 and Appendix C.
Assertion: A statement of a property that should hold. In Alloy this is
expressed with assert; in program verification it can also mean an explicit
check embedded in an implementation. See Chapters 4 and 10.
Runtime assertion: A check evaluated at a specific point during execution, with a violation producing a stop, exception, or log event. Distinguish its local scope and failure coupling from runtime verification by an external event monitor. See Chapter 11.
B
BDD (Binary Decision Diagram): A data structure for representing Boolean functions efficiently. It is used in symbolic model checking. See Chapter 8.
C
CAP theorem: In an asynchronous model that permits messages to be lost by a network partition, linearizable consistency and availability for every request to a non-failing node cannot both be guaranteed during that partition. It is not a rule to choose one of three letters at all times. See Chapter 7 and Appendix E.
Completeness: A metaproperty relating a deductive system to a semantics: every formula valid in that semantics is derivable. Completeness of first-order logic for its standard semantics must not be generalized without qualification to higher-order logic or dependent type theory. See Chapter 9.
Contract: An explicit statement of what must hold before an operation and what is guaranteed after it. Contracts often make preconditions and postconditions visible to both implementers and reviewers. See Chapters 3 and 10.
Counterexample: A concrete execution, trace, or state assignment that shows why a claimed property does not hold. In practice, counterexamples are often the most valuable output of a verifier because they direct debugging and model revision. See Chapters 4, 7, and 8.
CSP (Communicating Sequential Processes): A framework for describing concurrent systems as compositions of processes and communication events. See Chapter 6.
CTL (Computation Tree Logic): A branching-time temporal logic used to express reachability and branching properties. See Chapter 8.
Curry-Howard correspondence: The view that propositions correspond to types, and proofs correspond to programs. See Chapter 9.
D
Dafny: A verification-oriented programming language and toolchain for writing implementations together with contracts, invariants, and proofs. See Chapters 9, 10, and 12.
Dolev–Yao adversary model: A symbolic network model in which an attacker can intercept, modify, replay, and compose messages and use known keys, but does not break cryptography without the needed key. Compromise and side channels require explicit modeling. See Chapter 13 and Appendix E.
DRAT: A clausal proof ecosystem for showing unsat of propositional CNF.
A checker such as DRAT-trim validates a DRAT proof against DIMACS CNF, but it
does not directly validate the original SMT problem, the source specification,
or the encoder. See Chapter 12 and Appendix E.
Deadlock: A state in which multiple processes wait on one another and no further progress is possible. See Chapters 6 and 8.
F
Finite-trace semantics: Semantics that define satisfaction, violation, or an inconclusive result over an acquired finite event sequence and its end. Infinite-trace temporal logic must not be transferred silently onto a finite log. See Chapter 11 and Appendix C.
FLP impossibility result: Under complete asynchrony, deterministic processes, and at most one crash-stop failure, no consensus protocol guarantees termination in every admissible execution. Partial synchrony, failure detectors, and randomization address the problem by changing assumptions. See Chapter 7 and Appendix E.
Fairness: An assumption about action selection used when reasoning about liveness. In TLA+, weak fairness rules out ignoring an action that remains continuously enabled, while strong fairness also covers an action enabled infinitely often. It is an assumption on behaviors, not a guarantee that the implementation’s scheduler is fair; an overly strong assumption can make a liveness claim appear to hold only because of that assumption. See Chapter 7.
Formal specification: A mathematically precise description of required system behavior. Its purpose is to reduce ambiguity, expose hidden assumptions, and support systematic analysis. See Chapters 3-7.
H
Hoare logic: A logical system for reasoning about program correctness using preconditions, commands, and postconditions. See Chapter 10.
Hoare triple: An expression of the form {P} S {Q}, where P is a
precondition, S is a program fragment, and Q is a postcondition. See
Chapter 10.
I
Invariant: A property that must always hold. In model checking, violations are typically shown as counterexamples. See Chapters 3, 7, and 8.
Isabelle/HOL: A proof assistant centered on higher-order logic. It is often used for mechanized proofs, proof documentation, and larger proof libraries. See Chapters 9 and 10.
K
K-induction: A proof method combining finite base cases with an induction
step stating that if the property holds for k steps, it also holds at the
next step. Success is relative to initialization, the transition relation,
properties, assumptions, and engine configuration. See Chapter 8 and Appendix
C.
L
Lean 4: A proof assistant and programming language based on dependent type theory. In this book, it is presented as an engineering option for maintainable proof assets rather than as the only proof workflow. See Chapter 9 and Appendix B.
Liveness: A property stating that “something good eventually happens.” Liveness claims are often sensitive to assumptions such as fairness. See Chapter 8.
LTL (Linear Temporal Logic): A temporal logic for expressing properties along a single line of time. See Chapters 7 and 8.
LFSC: A proof format and checking framework based on the LF logical framework with computational side conditions. cvc5 can emit LFSC proofs, but unsupported internal rules may still appear as trust steps. See Chapter 12 and Appendix E.
LRAT: A propositional-CNF unsat certificate format designed to carry more
explicit checking hints than DRAT. It still validates the post-encoding CNF
problem rather than the original specification. See Chapter 12 and Appendix E.
Loop invariant: A condition that remains true during every iteration of a loop. It is central to proving partial and total correctness. See Chapter 10.
M
Model checking: A technique that explores the state space of a specified model and checks selected properties. Exhaustiveness is relative to the model, property, search configuration, fairness, and completion status; it is not a claim about every behavior of the real system. See Chapter 8.
Model / witness: A concrete satisfying assignment or execution returned by
a solver for a sat result. It shows that the encoded constraints are
satisfiable, but it does not by itself validate the natural-language
requirement or the original specification. See Chapter 12 and Appendix C.
Monitorability: The ability, under chosen semantics, to decide satisfaction or violation of a property from an observed finite prefix. Evaluate it separately from observability, which asks whether the required events can be obtained. See Chapter 11 and Appendix C.
O
Observability: The degree to which system state and causal relations needed for a decision can be reconstructed from events, metrics, and traces. Even a monitorable property lacks evidence when required events are missing. See Chapter 11.
P
Partial correctness: The property that if a program terminates, the result satisfies the required postcondition. It does not by itself prove termination. See Chapter 10.
Postcondition: A condition that must hold after an operation or program fragment finishes, assuming the precondition held at the start. See Chapters 3 and 10.
Precondition: A condition that must hold before an operation or program fragment starts for the promised result to be valid. See Chapters 3 and 10.
Prime notation (TLA+): Notation used inside an action to relate two states:
x is the current-state value and x' is the next-state value. It is distinct
from the LTL next-time operator X / ○. See Chapter 7.
PRISM: A model checker for probabilistic and quantitative properties of DTMCs, CTMCs, and MDPs. Its results are relative to model assumptions, schedulers, engines, and numerical precision; they do not establish that a real-world probability model is valid. See Chapter 8 and Appendices B and E.
Probabilistic model checking: Computing or checking reachability probabilities, thresholds, steady-state probabilities, and expected rewards over a transition model that contains probabilities or rates. It is distinct from statistical model checking based only on sampled paths. See Chapter 8.
Proof assistant: A software system that supports the construction and checking of formal proofs. Examples discussed in this book include Rocq, Lean, and Isabelle/HOL. See Chapters 9 and 12.
Proof obligation: A logical claim that must be discharged for a proof or verification argument to go through. Tools may generate proof obligations automatically from contracts, invariants, or program structure. See Chapters 8, 9, and 10.
Proof certificate: A machine-readable artifact emitted so that an unsat
claim can be rechecked by a separate implementation. What it establishes
depends on the format and checker; it does not automatically validate the
natural-language requirement. See Chapter 12 and Appendix E.
Proof checker: A checker or kernel that mechanically validates a proof certificate or proof term against an input problem and proof rules. Checker success applies to the encoded statement under those rules; it does not replace requirement review. See Chapter 12 and Appendix E.
Promela: The modeling language used by SPIN for concurrent systems. It is suited to describing processes, communication, and interleavings. See Chapters 6 and 8.
R
Refinement: The process of developing a concrete specification while
proving that, after applying a refinement mapping and hiding internal variables,
its behavior satisfies the abstract specification. Conceptually, the
implication runs as ConcreteSpec => AbstractSpec. See Chapters 3, 5, and 7.
Reward property: A probabilistic property over values such as attempts, time, energy, or cost attached to states or transitions. A reachability reward can be infinite when the target is missed with positive probability. See Chapter 8 and Appendix C.
Rocq: The proof assistant formerly known as Coq. Its kernel type-checks
proof terms constructed by tactics and other automation in the current logical
environment. Print Assumptions inventories dependent axioms and assumptions;
statement adequacy and extracted programs require separate review. See Chapters
9, 10, and Appendix E.
RTLola: A runtime-verification language and toolchain that specifies typed streams and triggers over online or offline events. This book guarantees only the pinned CLI 0.1.2 contract over finite offline CSV traces. See Chapter 11 and Appendices B and E.
Runtime verification: Checking executing or retained event traces against formal properties to produce violation, non-violation, or inconclusive verdicts over observed traces. Zero detected violations must not be generalized to correctness of all possible executions. See Chapter 11 and Appendix C.
S
Soundness: A metaproperty relating a deductive system to a semantics: every derivable formula is valid in that semantics. The relevant logic and semantics must be stated. See Chapter 9.
Sorry / admit: Mechanisms such as Lean sorry / admit and Rocq
Admitted that temporarily close a proof with an axiom-like hole. In Rocq,
inspect the dependency with Print Assumptions; CI should reject it or record a
time-bounded exception. See Chapters 9 and 12 and Appendix F.
Scheduler / adversary: A policy that resolves an MDP’s nondeterministic
choices, potentially from the execution history. Best- and worst-case
probabilities and rewards depend on the scheduler class and the min / max
direction. See Chapter 8 and Appendix C.
Statistical model checking: Approximating a property from randomly sampled paths. The result depends on sample count, confidence, error width, and maximum path length, and it does not automatically represent a worst-case MDP scheduler. See Chapter 8.
Safety: A property stating that “something bad never happens.” Such properties are often expressed as invariants. See Chapter 8.
Schema: In Z notation, a structured unit that groups declarations and constraints. Schemas are used to describe states, operations, and related conditions. See Chapter 5.
Specification: A precise statement of what a system must do, independent of how that behavior is implemented. In this book, specification is the bridge between informal requirements and verifiable properties. See Chapters 3-7.
SPIN: A model checker for concurrent systems centered on the Promela language. See Chapters 6 and 8.
SymbiYosys (sby): A front end for an open-source RTL formal flow centered on Yosys. It connects BMC, prove, and cover tasks to engines and backends; results are relative to the RTL, properties, assumptions, mode, depth, and toolchain. See Chapter 8 and Appendices B and E.
State space: The set of states a system can take. Its size is a central concern in verification. See Chapter 8.
State explosion problem: The problem that the number of reachable states can grow exponentially, making verification difficult. See Chapter 8.
State transition: A change from one system state to another caused by an operation, command, or event. State-transition thinking is central to TLA+, model checking, and many verification arguments in this book. See Chapters 7, 8, and 10.
T
Tamarin Prover: A symbolic security-protocol verifier using multiset-rewriting rules, facts, events, and trace lemmas under an active adversary. Results are relative to the equational theory, assumptions, lemmas, and proof configuration. See Chapter 13 and Appendices B and E.
TLA+: A specification language for distributed and concurrent systems. It uses actions to relate current and next states and temporal formulas to describe complete behaviors, normally in a stuttering-permitting form. Prime notation is not the LTL next-time operator. See Chapter 7.
Temporal logic: A family of logics used to describe how properties evolve
over time. LTL and CTL are representative examples; in TLA+, [], <>, and
~> describe behavior properties, while prime notation belongs to actions.
See Chapters 7 and 8.
Theorem proving: A style of verification that establishes correctness by constructing a proof rather than exhaustively exploring a state space. See Chapter 9.
TLC: An explicit-state model checker that enumerates reachable states of a
concrete finite model of a TLA+ specification. TLA+ has no conventional static
type system; predicates commonly named TypeOK or TypeInvariant assert that
values belong to expected sets. Results depend on the .cfg, properties,
fairness, state constraints, and completion status. See Chapters 7 and 8.
Trusted kernel: The small core that checks whether a proof term has the theorem statement as its type under the foundational logic and current environment. Acceptance does not establish statement adequacy; added axioms, unfinished holes, unchecked solver paths, extraction, and code generation form additional trust boundaries. See Chapter 9.
Trusted computing base (TCB): The full set of trusted assumptions behind a final assurance claim. Depending on the workflow, this can include the kernel, added axioms, unchecked translations, external solver paths, proof reconstruction, extraction, code generation, and approved exceptions. See Chapters 9 and 12.
Total correctness: The claim that a program not only satisfies the required postcondition when it terminates, but also does terminate. See Chapter 10.
Trace: A sequence of state transitions. Counterexamples are often presented as traces; security-protocol verification may present one as an attack trace that includes adversary operations. See Chapters 8 and 13.
Type theory: A logical foundation used by many proof assistants, where types and propositions are closely connected. It is central to Rocq, Lean, and the discussion in Chapter 9. See Chapter 9.
V
Vacuity: A property can hold trivially because an over-strong assumption or unreachable premise removed the executions that mattered, rather than because the intended behavior was established. Assumption review and meaningful cover targets help expose this failure mode. See Chapter 8 and Appendix C.
Verification condition: A logical obligation generated from a program or specification that must be proved for a correctness claim to hold. See Chapter 10.
Z
Z notation: A state-based formal specification language that uses schemas to describe states and operations. See Chapter 5.