Formal verification is the use of mathematical models and logical reasoning to establish that a hardware or software system satisfies a precisely stated specification. In computer science, it can address particular properties, such as safe memory access, or broader claims about functional behavior. Its conclusions concern every behavior covered by the model and assumptions, rather than only selected executions. Verification may establish a claim through a machine-checked formal proof or an exhaustive algorithmic analysis; it does not establish correctness independently of the specification. (cs.cmu.edu)
Specifications and models
Verification requires a formal description of what the system does and what it should do. A model may represent program execution, a circuit’s state changes, or interactions among components. Its precision depends on the chosen abstraction: a high-level protocol model can omit implementation details, whereas a code-level model must account for relevant features of the programming language, including memory operations and arithmetic behavior. Tools for low-level software verification explicitly model such features as bit vectors and floating-point arithmetic. (cs.cmu.edu)
Properties can describe individual states or complete executions. A safety property excludes an undesirable event, such as an out-of-bounds array access. A progress requirement concerns whether an event eventually occurs. Temporal logic provides operators expressing notions such as “always,” “eventually,” and “until,” making it useful for specifying the behavior of concurrent systems. Verification concerns the stated properties, which need not constitute a complete specification of every system feature. (cprover.org)
An essential distinction is between proving a model correct and establishing that the model faithfully represents the deployed system. Hardware behavior, initialization, external libraries, and environmental constraints may remain assumptions. A proof about modeled information channels, for example, does not automatically cover timing channels absent from that model. (sel4.systems)
Deductive program verification
Deductive verification establishes program properties using a logical system. Hoare logic expresses a basic correctness judgment as a triple:
[ {P}\ C\ {Q}. ]
Here, (P) is a precondition, (C) is a command, and (Q) is a postcondition. Under the partial-correctness interpretation, if execution begins in a state satisfying (P) and terminates, its final state satisfies (Q). Total correctness additionally requires termination. Thus, proving a postcondition alone does not necessarily show that a program returns a result. (cs.cornell.edu)
Rules for assignments, sequencing, conditionals, and loops reduce larger claims to smaller obligations. A loop invariant describes a property maintained across iterations. The proof establishes that it holds before the loop, is preserved by the body, and implies the required result when the loop exits. Termination can be established separately using a quantity that decreases according to a well-founded ordering. (cs.cornell.edu)
A proof assistant supports the construction and checking of these arguments. Human users provide definitions and intermediate claims, while automation can discharge some obligations. The guarantee depends on the soundness of the reasoning system and the correctness of its proof-checking machinery. Proof assistants with small trusted kernels aim to limit the amount of software that must be trusted directly. (sel4.systems)
Model checking and bounded analysis
Model checking determines whether a system model satisfies a property, commonly by analyzing a state-transition structure. For finite-state systems, algorithms can examine all relevant reachable states without requiring a manually constructed deductive proof. When a property fails, a checker can often produce a counterexample showing an execution that violates it. Such traces make model checking useful both for establishing properties and for diagnosing design errors. (cs.cmu.edu)
Bounded model checking examines executions up to a specified bound. One approach encodes the transition steps and a possible property violation as a Boolean satisfiability problem. A satisfying assignment represents a counterexample within the bound. An unsatisfiable result excludes violations in the encoded search space, but does not alone exclude longer executions. (cprover.org)
For programs with loops, proving that the chosen unwinding bound covers every relevant iteration can strengthen bounded analysis into an exhaustive result for the modeled program. CBMC uses unwinding assertions for this purpose. Without adequate coverage, a successful bounded check remains a restricted guarantee rather than an unrestricted correctness proof. (github.com)
Applications and examples
Formal verification applies to hardware designs and software components. Hardware model checking can examine circuit behavior, while software tools check properties such as pointer safety, arithmetic exceptions, and user-specified assertions. The scope ranges from a single function to selected components of an operating system. (cs.cmu.edu)
The seL4 microkernel illustrates verification through multiple abstraction levels. Its proof stack relates implementations to higher-level specifications and includes functional correctness and security properties. Coverage depends on the architecture and configuration: not every property is established for every variant. Its documented assumptions identify remaining dependencies, including hardware behavior and certain low-level code. (sel4.systems)
CompCert illustrates verified compilation. Its machine-checked correctness argument relates the observable behavior of supported C programs to the assembly code produced by compilation. This establishes a property of translation, not the application’s intended functionality. A separate argument is needed to show that the source program satisfies its requirements; the compiler guarantee also has conditions concerning undefined behavior and the surrounding toolchain. (arxiv.org)
Limits and assurance
Verification faces computational and modeling constraints. State spaces can grow rapidly, and software introduces difficulties through dynamic allocation, concurrency, external calls, and complex language features. Abstraction reduces the problem size, but the relationship between an abstract model and the implementation must itself be justified. (cs.cmu.edu)
The trusted computing base comprises components relied upon without being fully covered by the proof. These may include proof checkers, unverified toolchain stages, hardware models, or initialization code. Testing and manual validation remain relevant at these boundaries: a mathematical argument cannot establish that physical hardware behaves exactly as assumed. The assurance claim must therefore identify the verified artifact, the properties proved, the configurations covered, and the assumptions connecting the formal result to execution. (arxiv.org)