---
id: wiki-2026-0508-formal-verification-of-software
title: Formal Verification of Software
category: 10_Wiki/Topics
status: verified
canonical_id: self
aliases: [Formal Methods, Program Verification]
duplicate_of: none
source_trust_level: A
confidence_score: 0.9
verification_status: applied
tags: [formal-methods, verification, correctness]
raw_sources: []
last_reinforced: 2026-05-10
github_commit: pending
tech_stack:
  language: Coq/Lean/TLA+
  framework: Dafny/F*
---

# Formal Verification of Software

## 매 한 줄
> **"매 prove correctness, 매 test correctness 의 X"**. Formal verification 의 mathematical proof 의 program 의 specification 에 대한 conformance — 매 testing 의 fundamental superset. 2026 의 industrial use 의 expanding (AWS s2n-tls, sel4, CompCert, Cardano, Dafny in MS, Lean 4 의 mathlib).

## 매 핵심

### 매 Spectrum of rigor
1. **Type systems**: lightweight, daily (TypeScript, Rust borrow checker).
2. **Property-based testing**: empirical, partial (QuickCheck).
3. **Model checking**: finite-state exhaustive (TLA+, SPIN).
4. **Deductive verification**: machine-checked proofs (Coq, Lean, Dafny, F*).
5. **Refinement**: high-level spec → low-level impl preserves properties (Event-B).

### 매 Tools (2026 leaders)
- **TLA+**: distributed system specs (used by AWS, Azure for protocols).
- **Coq / Lean 4**: dependent types, proof assistant.
- **Dafny**: verification-aware imperative language (MS).
- **F***: ML-style with refinement types (HACL* crypto, EverParse).
- **Kani / Creusot**: Rust verification.
- **CBMC**: bounded model checker for C.

### 매 What gets verified
- Algorithmic correctness (sorting, hashing).
- Protocol safety (no deadlock, agreement).
- Memory safety (no UAF, overflow).
- Cryptographic implementations (HACL* used in Linux, Firefox).
- Compiler correctness (CompCert).
- OS kernel (seL4 — full functional correctness).

### 매 응용
1. Safety-critical (avionics DO-178C Level A, automotive ISO 26262).
2. Crypto libraries (HACL*, Project Everest).
3. Distributed protocols (Paxos, Raft TLA+).
4. Smart contracts (Cardano Plutus, MoveProver).
5. Compilers / kernels (CompCert, seL4).

## 💻 패턴

### TLA+ — distributed mutex spec
```tla
---- MODULE Mutex ----
EXTENDS Naturals
VARIABLES queue, holder

Init == queue = <<>> /\ holder = NULL

Request(p) == queue' = Append(queue, p) /\ UNCHANGED holder

Acquire == /\ queue # <<>>
           /\ holder = NULL
           /\ holder' = Head(queue)
           /\ queue' = Tail(queue)

MutualExclusion == \A p, q \in Procs : holder = p /\ holder = q => p = q

THEOREM Spec => []MutualExclusion
====
```

### Dafny — verified binary search
```dafny
method BinarySearch(a: array<int>, key: int) returns (idx: int)
  requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  ensures 0 <= idx ==> idx < a.Length && a[idx] == key
  ensures idx < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{
  var lo, hi := 0, a.Length;
  while lo < hi
    invariant 0 <= lo <= hi <= a.Length
    invariant forall i :: 0 <= i < lo ==> a[i] < key
    invariant forall i :: hi <= i < a.Length ==> a[i] > key
  {
    var mid := (lo + hi) / 2;
    if a[mid] < key      { lo := mid + 1; }
    else if a[mid] > key { hi := mid; }
    else                 { return mid; }
  }
  return -1;
}
```

### Lean 4 — proof of a simple lemma
```lean
theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero => rfl
  | succ k ih => simp [Nat.succ_add, ih]
```

### F* refinement types
```fsharp
val divide : x:int -> y:int{y <> 0} -> int
let divide x y = x / y

// Compiler proves y <> 0 at every call site — divide-by-zero impossible
```

### Kani — Rust harness
```rust
#[kani::proof]
fn check_sum_no_overflow() {
    let a: u32 = kani::any();
    let b: u32 = kani::any();
    kani::assume(a < 1000 && b < 1000);
    let sum = a + b;
    assert!(sum == a + b);  // proven for ALL inputs in range
}
```

### CBMC — bounded check on C
```c
#include <assert.h>
int main() {
  int x = nondet_int();
  __CPROVER_assume(x >= 0 && x < 100);
  int y = x * x;
  assert(y >= 0);
  return 0;
}
// cbmc file.c → reports counterexample if assertion fails
```

### Property + spec hybrid (Hypothesis)
```python
from hypothesis import given, strategies as st

@given(st.lists(st.integers()))
def test_sort_preserves_length(xs):
    assert len(sorted(xs)) == len(xs)

@given(st.lists(st.integers()))
def test_sort_is_ordered(xs):
    s = sorted(xs)
    assert all(s[i] <= s[i+1] for i in range(len(s)-1))
```

## 매 결정 기준
| 상황 | Approach |
|---|---|
| Web app daily | Strong types + property tests |
| Distributed protocol | TLA+ model |
| Crypto primitive | F* / HACL* |
| Smart contract | MoveProver / Plutus |
| OS / hypervisor | Coq / seL4-style |
| Rust kernel code | Kani / Creusot |

**기본값**: types everywhere + property-based for parsers + TLA+ for distributed designs + reach for proof assistants only when life/billions on the line.

## 🔗 Graph
- 부모: [[Computer_Science_and_Theory]]
- 변형: [[Type-safe Error Handling  Exhaustiveness Checking]] · [[TypeScript 타입 시스템 (TypeScript Type System)|Type Systems]]
- 응용: [[Practical-Cryptography]] · [[SAST]]
- Adjacent: [[Quality-Control]] · [[Test_Automation]]

## 🤖 LLM 활용
**언제**: draft TLA+ specs from prose descriptions, suggest invariants, explain failing proofs.
**언제 X**: never trust LLM-generated proof without checker (Lean/Coq) verifying.

## ❌ 안티패턴
- **Spec ≠ implementation**: verify spec, ship different code.
- **Unverified assumptions**: proofs depend on `axiom` blocks that hide bugs.
- **Verify everything**: cost > benefit for typical CRUD.
- **No model**: claim "formally verified" with handwaved diagram.

## 🧪 검증 / 중복
- Verified (Lamport TLA+ book, Pierce SF, AWS Builders Library 2024 formal methods).
- 신뢰도 A.

## 🕓 Changelog
| 날짜 | 변경 |
|---|---|
| 2026-05-08 | Phase 1 |
| 2026-05-10 | Manual cleanup — spectrum + tool examples |