What are Formal Methods
A technical framework for pursuing software and hardware correctness through mathematical rigor
Overview of Formal Methods
Formal Methods are a collection of techniques for describing system specifications and verifying their correctness based on mathematical notation, logic, and proofs. Rather than relying on human intuition or review to answer questions like 'Is the specification correct?' or 'Does the implementation satisfy the specification?', they provide answers backed by mathematical rigor.
Formal methods are broadly classified into three areas. Each approaches system correctness from a different angle, but all share a common mathematical foundation.
Three Areas of Formal Methods
Model Checking
A methodology that represents system behavior as finite-state models and automatically verifies the absence of undesirable states (deadlocks, livelocks, safety violations, etc.) by exhaustively exploring all possible states.
Since tools mechanically explore the state space without requiring humans to devise test cases, oversights cannot occur in principle. However, the 'state explosion' problem of enormous state counts means direct application to large-scale systems requires careful approaches.
Representative tools: SPIN, NuSMV, UPPAAL, TLC (TLA+ model checker)
Application examples: Communication protocol verification, deadlock detection in concurrent systems, hardware design verification
Theorem Proving
A methodology that formalizes system properties as mathematical theorems and proves their validity using logical inference rules. While model checking is limited to finite states, theorem proving can be applied to systems with infinite state spaces.
Proofs are either developed interactively by humans or explored by automated provers. Full automation is generally difficult, but once a proof is complete, it provides the strongest possible correctness guarantee.
Representative tools: Coq, Isabelle/HOL, Lean, PVS, ACL2
Application examples: Proof of compiler correctness (CompCert), OS kernel verification (seL4), cryptographic protocol safety proofs
Formal Specification
A methodology that uses mathematical notation (predicate logic, set theory, algebra, etc.) to rigorously describe what a system 'should do.' It eliminates the ambiguity unavoidable in natural language specifications, enabling all stakeholders to share a common understanding.
Formal specifications also serve as inputs for model checking and theorem proving, making formal specification the foundation for other formal methods. Additionally, test cases can be automatically generated from specifications, and the stepwise refinement process from specification to implementation can be formally managed.
Representative languages: VDM-SL, Z notation, B-Method, TLA+, Alloy
Application examples: Railway signaling systems (B-Method), distributed system design (TLA+/AWS), smart cards (VDM)
Relationship Between the Three Areas
These three areas are not independent but complement each other. Ideally, formal specification rigorously defines 'what the system should do,' model checking exhaustively verifies 'no undesirable states exist,' and theorem proving mathematically guarantees 'properties always hold.'
In practice, these are combined according to system characteristics and risk. More rigorous methods are applied in safety-critical domains (aviation, railway, medical devices), while even just eliminating ambiguity through formal specification can provide significant benefits for business applications.
Track Record of Formal Methods
Formal methods are not limited to academic theory; they have produced real results in industrial sectors requiring high reliability.
Railway: The Paris Metro Line 14 automated driving system was developed using B-Method and has achieved zero major signal failures since operation began. Safety is guaranteed through gradual refinement of specifications to code and proofs.
Aerospace: Formal verification is employed in Airbus flight control software. NASA also uses theorem provers such as PVS to verify mission-critical systems.
Semiconductor: Following the Intel Pentium FDIV bug (1994), model checking and theorem proving have been widely adopted for verification of floating-point arithmetic in processors. Formal verification is now a standard quality assurance method throughout the semiconductor industry.
Cloud Infrastructure: Amazon Web Services uses TLA+ to verify distributed system designs for DynamoDB, S3, EBS, and other services. The combination of TLA+ specification and the TLC model checker has revealed subtle design bugs.
OS Kernel: The seL4 microkernel is the world's first general-purpose OS kernel whose C implementation has been mechanically proven to correctly satisfy its specification using theorem proving with Isabelle/HOL.
Barriers to Adoption and the Future
Despite the widely recognized effectiveness of formal methods, their adoption in general software development has been limited. The main barriers include the cost of acquiring mathematical expertise, the effort required for specification writing, and the maturity of tool chains.
In recent years, the development of Large Language Models (LLMs) is changing these barriers. The potential to bring formal methods to a wider development audience is being researched through AI-assisted specification writing, interactive specification refinement, and automated verification.
IID Systems Research
IID Systems focuses particularly on formal specification and is researching new development methodologies combining it with AI agents. For details, please see the 'Formal Specification' page and the 'Research Projects' page.