IM Engineer Study Notes
← Back to list
SW Engineering & Management
#정형기법#정형검증#모델체킹#정리증명#추상해석
Last updated · 2026-10-10

Formal Methods and Formal Verification

1. Overview

Formal methods are a systematic engineering discipline that, grounded in mathematical logic and discrete mathematics, describe the requirements and design of software and hardware systems unambiguously (formal specification) and mathematically prove or refute that the description always satisfies certain properties (formal verification).

Ordinary software quality activities rely on testing and review. However, testing can only show the "presence" of defects for a selected, finite set of inputs; it cannot prove their "absence." Dijkstra's remark that "testing can show the presence of bugs, but never their absence" captures this limitation precisely. Formal methods reduce the behavior of a system to a mathematical model and thus differ fundamentally from testing in that they deal with universal propositions over all possible states and inputs rather than finite cases.

The starting point of formal methods is the elimination of the ambiguity and incompleteness inherent in natural-language specifications. Statements such as "the response must be fast" or "only one accesses at a time" leave much room for interpretation, but writing them in temporal logic or as set-theoretic state predicates fixes their meaning to one. Because the specification itself becomes executable or analyzable, contradictions and omissions can be found early at the requirements stage. Since the cost of fixing a defect grows exponentially the later it is found (tens to hundreds of times more in operations than at the requirements stage), formalization in upstream processes is also significant from a cost standpoint.

A representative lesson is the 1994 floating-point division (FDIV) defect in the Intel Pentium. This error, arising in a blind spot of design verification, cost Intel about 470 million dollars in recall expenses, and the semiconductor industry subsequently adopted theorem-proving-based verification for arithmetic circuits on a broad scale. In software too, formal methods took root mainly in high-assurance fields such as aviation, railways, medical devices, and financial payments, where a single error can lead to loss of life or large-scale damage.

1.1 Background and Necessity

First, regulation of safety-critical systems effectively demands formal methods. EN 50128 for railway signaling, DO-333 (the Formal Methods Supplement to DO-178C) for aviation software, high ASIL grades of the automotive functional safety standard ISO 26262, and Common Criteria EAL6–7 for security evaluation all explicitly recognize or recommend formal specification and verification at the highest assurance levels.

Second, defects in concurrency and distributed systems are hard to reproduce by testing. Race conditions, deadlocks, message reordering, and partial failures surface only under particular schedulings and timings, and such state combinations are hard for humans to enumerate and have low reproducibility. Formal methods exhaustively explore the possible interleavings over a model and automatically present counterexamples that humans could not have imagined.

Third, they correct the illusion of test coverage. High line and branch coverage does not equal correctness, and especially for stateful protocols and algorithms, coverage metrics do not guarantee the absence of defects. Formal verification fills this gap by providing property-centric assurance of "what must always be true."

1.2 The Spectrum of Formalization (Lightweight to Fully Formal)

Formal methods should be understood not as "all or nothing" but as a spectrum of application intensity. Fully formal approaches, which stitch together machine-checked proofs from specification to implementation, are the most costly. At the opposite end, lightweight formal methods model only the core parts of a design and filter out fatal errors early through automated analysis. In practice, the lightweight approach leads industrial adoption because of its strong cost-effectiveness. Amazon, for example, chose a strategy of modeling only core protocols such as consensus and replication in TLA+ to remove deep defects in advance, rather than proving the entire service.

Organizing this spectrum from a cost and assurance perspective yields the following. As application intensity rises, the assurance gained grows, but the required expertise and time grow as well, so organizations must choose an appropriate point according to the risk of the target.

Intensity Representative techniques Assurance level Cost/difficulty
Lightweight Type systems, Alloy, design model checking Early detection of design defects Low
Medium Contract-based, abstract interpretation, BMC Partial assurance such as absence of runtime errors Medium
Fully formal Theorem-proving-based end-to-end verification Full assurance that implementation satisfies the spec Very high

2. Overall Structure and Classification of Formal Methods

flowchart TB
    R["Requirements (natural language)"] --> SPEC["Formal specification<br/>Z / VDM / B / TLA+ / Alloy"]
    SPEC --> PROP["Properties to verify<br/>safety / liveness / invariants"]
    SPEC --> VER{"Formal verification approach"}
    VER --> MC["Model checking<br/>state-space exploration"]
    VER --> TP["Theorem proving<br/>deductive reasoning"]
    VER --> AI["Abstract interpretation<br/>static analysis"]
    MC -->|counterexample| FIX["Fix design/spec"]
    TP -->|proof fails| FIX
    AI -->|alarm| FIX
    MC -->|property holds| OK["Verification complete"]
    TP -->|proof succeeds| OK
    FIX --> SPEC
    OK --> IMPL["Implementation/refinement"]
    IMPL --> CODE["Verified code/circuit"]

Formal methods consist broadly of two axes: "formal specification" and "formal verification." Specification is the activity of writing in mathematical language what a system must do, and verification is the activity of proving that the specification satisfies the properties or that the implementation satisfies the specification. The two axes are not separable; through refinement, an abstract specification is concretized step by step while each step is verified to preserve the higher-level specification.

The properties to be verified are usually divided into three categories. Safety means "something bad never happens" (e.g., two trains never enter the same section simultaneously); liveness means "something good eventually happens" (e.g., a request is eventually answered); and an invariant is a predicate true in every reachable state. Safety and liveness are commonly expressed in temporal logics such as linear temporal logic (LTL) and branching temporal logic (CTL).

2.1 Formal Specification Languages

Formal specification languages differ in character according to the abstraction they aim for. State-based languages model a system as a set of states and state transitions, while algebraic / process-algebra languages describe it around behavior and communication. The table below is a supplementary comparison; the essence of the choice lies in "the property to be verified and the level of automation."

Language Family Strength Representative use
Z, VDM State specs based on set theory and predicate logic Clarity of data/function specs Finance / spec standardization
B / Event-B Refinement-centric, auto-generated proof obligations Spec→code refinement assurance Paris Metro signaling (B)
TLA+ State + temporal logic, model checking (TLC) Concurrency / distributed protocols Distributed system design
Alloy Relational logic, SAT-based analysis Structure/invariant exploration, lightweight Design exploration / security models
SPIN/Promela Process models, LTL verification Communication protocols Protocols / concurrency

The B language family automatically generates a "proof obligation" at each refinement step from specification to implementation, and discharging them guarantees that the implementation preserves the specification. TLA+, by contrast, does not aim at code generation but focuses on filtering out design-level defects through model checking. Thus, even for the same "formal specification," the practical key is that tool choice differs according to the goal (assuring code conformance vs. finding design defects).

2.2 Classification of Formal Verification Techniques

Formal verification is distinguished by the trade-off between degree of automation and completeness. Model checking exhaustively explores a finite-state model fully automatically but is vulnerable to state explosion; theorem proving can handle infinite states and general properties but requires creative human intervention (proof strategies, auxiliary lemmas). Abstract interpretation over-approximates program semantics to automatically prove the absence of runtime errors while accepting false positives.

Abstract interpretation is among the most widely adopted axes in practice. By interpreting a program over abstract domains such as intervals, signs, or nullness instead of concrete variable values, one can compute in finite time an over-approximating set that safely covers all executions. Thanks to this over-approximation, one can automatically prove that "array out-of-bounds, null dereference, and overflow never occur," while the price of over-approximation is false positives that raise alarms on cases that are actually safe. Astrée, used to prove the absence of runtime errors in Airbus avionics software, is a representative example, reportedly analyzing embedded C code of hundreds of thousands of lines without false positives. The important distinction is that abstract interpretation gives "property-centric exhaustive assurance" with almost no human intervention, so it tends to be applied to large-scale code earlier than model checking or theorem proving.

3. Model Checking and Theorem Proving

flowchart LR
    M["System model<br/>finite state transitions"] --> B["Build state space"]
    P["Property<br/>LTL/CTL formula"] --> B
    B --> E["Exhaustive reachable-state search"]
    E --> Q{"Property-violating state?"}
    Q -->|none| T["Proof that property holds"]
    Q -->|exists| X["Generate counterexample path"]
    X --> D["Diagnose design defect"]
    E -.state explosion.-> O["Mitigation techniques"]
    O --> SYM["Symbolic representation (BDD)"]
    O --> SAT["SAT/SMT, BMC"]
    O --> PO["Partial-order reduction"]
    O --> ABS["Abstraction, CEGAR"]

3.1 Model Checking

Model checking exhaustively explores all reachable states of a finite-state system and automatically decides whether a property written in temporal logic holds. When a property is violated, it presents the concrete execution path leading to the violation—that is, a counterexample—so its debugging value is very high. For this achievement, Clarke, Emerson, and Sifakis received the Turing Award in 2007.

The greatest challenge of model checking is state explosion. With n concurrent components, the total state grows as the product of each component's states, increasing exponentially with the number of variables and the degree of concurrency. To mitigate this, one uses symbolic model checking, which represents sets of states symbolically with binary decision diagrams (BDDs) instead of enumerating states explicitly; bounded model checking (BMC), which reduces the existence of a counterexample up to a certain depth to a SAT/SMT problem; partial-order reduction, which removes unnecessary orderings of concurrent events; and CEGAR, which progressively refines abstractions based on counterexamples.

Industrially, model checking is widely applied to verifying communication protocols, cache coherence, hardware control logic, and distributed consensus algorithms. For instance, SPIN detects deadlock and liveness violations of protocols with Promela models and LTL properties, and TLA+'s TLC checker finds subtle invariant violations in distributed consensus and replication designs that surface only when dozens of steps are entangled.

3.2 Theorem Proving (Deductive Verification)

Theorem proving expresses the system and properties as logical formulas and deductively proves the properties by applying axioms and inference rules. Unlike model checking, there is no constraint on the number of states, so it can handle infinite-state, parameterized systems, and general mathematical properties. Interactive theorem provers such as Coq, Isabelle/HOL, Lean, and PVS have humans direct the proof strategy while the machine rigorously checks the validity of each inference step.

The price is the limit of automation. Conceiving the key lemmas, designing the inductive structure, and strengthening invariants still depend on human creativity. However, with advances in Hoare logic and separation logic and their combination with SMT solvers (e.g., Dafny, F*), the repetitive and mechanical proof burden has been greatly reduced. Separation logic is a core theory that modularized memory-safety proofs dealing with pointers and the heap, making verification of large-scale system software feasible.

3.3 Model Checking vs. Theorem Proving — Why the Difference Arises

The difference between the two techniques stems from the approach of "search vs. reasoning." Model checking concretely unfolds the state space to check properties, so automation is easy and counterexamples are concrete, but the space must be finite and of manageable size. Theorem proving generalizes mathematically without unfolding states, so it handles the infinite and large-scale, but constructing proofs takes expert personnel and long time. Therefore, in practice, a layered strategy is reasonable: quickly filter defects with model checking early in design, and ultimately invest theorem proving only in core assets that need full assurance, such as kernels and compilers.

Aspect Model checking Theorem proving
Automation High (fully automatic) Low (interactive)
State scale Finite, explosion-prone Possibly infinite
Output Counterexample path Machine-checked proof
Required skill Relatively low High expertise
Representative tools SPIN, TLC, NuSMV Coq, Isabelle, Lean

4. Industrial Application Cases

The most symbolic case is the seL4 microkernel. It is the first general-purpose OS kernel to machine-prove functional correctness—that is, that the implementation exactly matches the abstract specification—in Isabelle/HOL for about 8,700 lines of C code; the proof ran to about 200,000 lines and the effort to about 20 person-years. seL4 later extended its proofs to memory safety and information-flow security and is used in high-assurance embedded and defense fields.

In the compiler field, CompCert is representative. It is a verified C compiler that proved in Coq that "the semantics of the source program is preserved in the generated machine code," and it earned trust in safety-critical fields such as aviation (Airbus). A supporting point for the effectiveness of formal verification is that while random-testing studies found many defects in other commercial compilers, essentially no miscompilation defects were found in CompCert's verified optimization phases.

In distributed systems, Amazon Web Services' (AWS) use of TLA+ is widely cited. AWS reported that by modeling core protocols of S3, DynamoDB, EBS, and others in TLA+, it removed deep errors before operation—such as a defect reproduced only when 35 steps are entangled—that design review and testing had missed. In particular, they emphasized as the practical benefit of adopting TLA+ that "model checking reaches consensus faster than design discussion and catches defects at the design stage rather than the costly operations stage." In railways, the driverless signaling system of Paris Metro Line 14 (METEOR), formally developed and verified at roughly 110,000 lines in the B language, is a classic success case.

Microsoft's Static Driver Verifier (SDV) is also an industrial success. By verifying with model-checking-based tools (SLAM/SDV) whether Windows device drivers violate kernel API usage conventions (lock acquire/release ordering, callback rules, etc.), it filtered out en masse, before release, the third-party driver defects that had been a major cause of blue screens. These cases show that formal methods are not an academic ideal but an engineering means that actually lowers the design risk of large-scale commercial systems.

5. Advanced: Recent Trends and Adoption Strategy

The recent trend in formal methods is summarized as a shift from "experts only" to "developer-friendly." First, the dramatic performance improvement of SMT solvers (such as Z3) has raised the level of automation in proof and verification. "Verification-oriented programming" languages such as Dafny and F*, which annotate specifications directly in code and have the solver automatically discharge proof obligations, have emerged, so that verification at the level of pre/post-conditions and invariants can be integrated into everyday development even by non-mathematicians.

Second, the fusion of memory-safe languages and formal methods is active. Rust's ownership and borrow model is itself a lightweight formal rule at compile time that eliminates a large class of memory and data-race errors, and tools such as Kani, Prusti, and Verus add model checking and deductive verification to Rust code. Moreover, since blockchain smart contracts are hard to fix after deployment and directly tied to monetary loss, security audits premised on formal verification—such as the Certora and K frameworks—are becoming a de facto standard.

Third, a bidirectional combination with AI is rising. On one hand, there are active attempts to lower the entry barrier to formal verification by having large language models generate draft specifications, proof scripts, and invariant candidates (proof-automation assistance), and on the other hand, research proceeds on formally verifying safety-critical AI control logic itself. However, since LLM outputs cannot be trusted on their own, a structure in which a machine checker guarantees final validity (AI generates, the prover checks) is a core design principle.

6. Considerations and Implications

First, the application strategy must be "selection and concentration." Fully formalizing an entire system is mostly uneconomical, so a layered quality strategy is realistic: invest formal methods only in core algorithms, protocols, and security boundaries with high impact on failure, and run testing in parallel for the rest. Filtering architectural defects with lightweight formal methods (TLA+, Alloy) early in design yields the greatest return on investment.

Second, the core trade-off is assurance level versus cost and capability. Full assurance at the level of theorem proving demands enormous time and expert personnel, so the assurance level must be set according to the organization's maturity, regulatory requirements, and risk. Also, in that "if the specification is wrong, the proof is wrong too," verification presupposes the correctness and completeness of the specification, and specification review itself is an important quality activity. What is verified is only that "the implementation satisfies the specification"; whether "the specification reflects the real requirement" is a separate problem.

Third, combination with related technologies is the key to adoption. A DevSecOps-oriented design is needed that integrates formal specification and verification into the CI pipeline to automate regression verification (e.g., running model checking on commit) and places them complementarily with testing, fuzzing, and runtime verification. Automatically generating test cases or monitors (runtime assertions) from formal models allows verification assets to be reused all the way into operations.

Fourth, from the perspective of outlook and personnel. As SMT and AI assistance lower the entry barrier, formal methods are expected to spread gradually beyond special domains into general software engineering. However, since specification ability, invariant design, and abstraction capability remain advanced engineering competencies, from a professional engineer's perspective one must prepare organization-level education, tool standardization, and a verification-asset management system together to make adoption sustainable.

References

In one line: Formal methods are a high-assurance quality means that deals with the "absence of defects" through mathematical specification and proof; they become effective when model checking (automatic, finite) and theorem proving (general, infinite) are selected and concentrated according to risk and combined with SMT, AI, and CI.