> For the complete documentation index, see [llms.txt](https://isubasinghe.gitbook.io/isithas-wiki/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://isubasinghe.gitbook.io/isithas-wiki/computer_science/formal-verification.md).

# formal verification

## Basic idea

Mathematically proving that a program (or hardware design) satisfies a specification, rather than testing it on sample inputs. Approaches range from automated SMT-based checking (Z3, Dafny) to interactive proof assistants and dedicated logics for state, heap, and concurrency.

## Key facts

* **SMT** (Satisfiability Modulo Theories): SAT extended with theories of integers, reals, arrays, bitvectors — Z3, CVC5.
* **Solver architecture**: DPLL(T), congruence closure, theory combination, quantifier instantiation, and interpolation.
* **Separation logic**: extension of Hoare logic with $P \* Q$ for disjoint heaps; enables the frame rule and local reasoning.
* **Weak memory models**: x86-TSO, ARMv8, C11 — reasoning about reorderings under relaxed consistency.
* **Memory fences**: language- and ISA-level constraints on ordering and visibility.
* **Dafny / Viper**: program verifiers that discharge proof obligations to SMT solvers.
* **Refinement**: proves that concrete steps and traces implement an abstract specification.
* **Distributed verification**: safety invariants, liveness, fairness, and protocol refinement.
* **Program logics**: Hoare triples, weakest preconditions, loop invariants, and well-founded variants.
* **Abstract interpretation**: sound fixed-point approximation over abstract domains.
* **Temporal logic**: safety, liveness, fairness, and branching- or linear-time behavior.
* **Model checking**: exhaustive or symbolic state exploration with counterexample traces.