---
id: wiki-2026-0508-formal-methods
title: Formal Methods
category: 10_Wiki/Topics
status: verified
canonical_id: self
aliases: [formal verification, TLA+, model checking, theorem proving, Coq, Lean, Alloy, refinement type]
duplicate_of: none
source_trust_level: A
confidence_score: 0.95
verification_status: applied
tags: [formal-methods, verification, tla-plus, model-checking, coq, lean, software-correctness]
raw_sources: []
last_reinforced: 2026-05-10
github_commit: pending
tech_stack:
  language: TLA+ / Lean / Coq / Alloy
---

# Formal Methods

## 매 한 줄
> **"매 mathematical 의 의 의 software 의 correctness 의 prove"**. 매 model checking (TLA+), 매 theorem proving (Coq, Lean), 매 SMT (Z3), 매 refinement type (F*). 매 modern: 매 AWS TLA+ usage, 매 Lean 4 in math, 매 LLM-aided proof.

## 매 핵심

### 매 spectrum
- **Lightweight**: 매 design-by-contract, type system.
- **Model checking**: TLA+, SPIN, Alloy.
- **Theorem proving**: Coq, Lean, Isabelle.
- **SMT solvers**: Z3, CVC5.
- **Verified compiler**: CompCert, CakeML.

### 매 modern usage
- **AWS** S3, DynamoDB use TLA+ for distributed protocols.
- **CompCert**: 매 verified C compiler.
- **seL4**: 매 verified microkernel.
- **CakeML**: 매 verified ML.
- **Cardano**: 매 Plutus formal.
- **Lean 4**: 매 mathlib, Anthropic / OpenAI 의 LLM usage.

### 매 modern AI integration
- **LLM-aided proof** (PALM, GPT-f).
- **AlphaProof / AlphaGeometry** (DeepMind).
- **Tactic prediction** (Coq, Lean).

### 매 응용
1. **Distributed protocol**.
2. **Cryptography**.
3. **Compiler / OS**.
4. **Hardware design**.
5. **Smart contract**.
6. **Mathematics**.

## 💻 패턴

### TLA+ specification
```tla
EXTENDS Naturals, TLC
VARIABLE counter

Init == counter = 0
Next == counter' = counter + 1
Spec == Init /\ [][Next]_counter
Invariant == counter >= 0
```

### TLA+ distributed mutex (Lamport)
```tla
EXTENDS Sequences, Naturals
VARIABLES requests, granted

Request(c) == requests' = Append(requests, c) /\ UNCHANGED granted
Grant ==
    /\ Len(requests) > 0
    /\ granted' = Head(requests)
    /\ requests' = Tail(requests)

MutualExclusion == Cardinality({c \in granted}) <= 1
```

### Lean 4 (theorem)
```lean
theorem add_comm (a b : Nat) : a + b = b + a := by
  induction a with
  | zero => simp
  | succ n ih => rw [Nat.succ_add, ih, Nat.add_succ]
```

### Coq proof
```coq
Theorem plus_comm : forall n m : nat, n + m = m + n.
Proof.
  intros n m.
  induction n as [|n' IHn'].
  - simpl. rewrite <- plus_n_O. reflexivity.
  - simpl. rewrite IHn'. rewrite <- plus_n_Sm. reflexivity.
Qed.
```

### Z3 SMT (Python)
```python
from z3 import *

x, y = Ints('x y')
s = Solver()
s.add(x + y > 5)
s.add(x < 10)
s.add(y < 10)
if s.check() == sat:
    print(s.model())  # 매 e.g., x=6, y=0
```

### Alloy (relational)
```alloy
sig Person {
    spouse: lone Person
}
fact spouse_symmetric { all p, q : Person | p in q.spouse iff q in p.spouse }
fact no_self_marriage { all p : Person | p not in p.spouse }
run {} for 5
```

### F* (refinement type)
```fstar
val abs : x:int -> y:int{y >= 0 /\ (y = x \/ y = -x)}
let abs x = if x < 0 then -x else x
```

### Refinement (Liquid Haskell)
```haskell
{-@ type Pos = {v:Int | v > 0} @-}
{-@ divBy :: Int -> Pos -> Int @-}
divBy :: Int -> Int -> Int
divBy x y = x `div` y
```

### Property-based test (QuickCheck)
```haskell
import Test.QuickCheck

prop_reverse :: [Int] -> Bool
prop_reverse xs = reverse (reverse xs) == xs

main = quickCheck prop_reverse
```

### LLM-aided proof (Lean Tactic Prediction)
```python
def predict_tactic(state, llm):
    prompt = f"""You are a Lean 4 expert. Given this proof state:
{state}

Suggest the next tactic. Output Lean syntax only."""
    return llm.generate(prompt)
```

### Verified C compiler (CompCert use)
```bash
ccomp -O hello.c -o hello
# 매 produces same semantic 의 unverified gcc -O0
```

### Spec → impl (Dafny)
```dafny
method Max(a: int, b: int) returns (m: int)
  ensures m >= a && m >= b
  ensures m == a || m == b
{
  if a >= b { m := a; } else { m := b; }
}
```

### TLC model checker
```bash
tlc -workers auto -fp 64 Spec.tla
# 매 invariant violation 의 trace 의 print
```

### Hoare logic (manual)
```
{P}  S  {Q}
{x = 0}  x := x + 1  {x = 1}
```

### LLM proof verifier (sketch)
```python
def llm_proof_then_verify(claim, llm):
    proof_attempt = llm.generate(f'Prove in Lean 4: {claim}')
    # 매 Lean check
    result = run_lean(proof_attempt)
    if result.error:
        return llm.refine_proof(proof_attempt, result.error)
    return proof_attempt
```

### Proof assistant frontend (VSCode)
```yaml
# 매 lean-tactic
extensions:
  - leanprover.lean4
  - jroesch.lean
shortcuts:
  - "Ctrl+Shift+Enter": run tactic
```

## 매 결정 기준
| 상황 | Tool |
|---|---|
| Distributed protocol | TLA+ |
| Crypto algorithm | Coq / EasyCrypt |
| Compiler | CompCert / CakeML |
| Math research | Lean 4 / Isabelle |
| Quick property check | QuickCheck / Hypothesis |
| Specific bug | Z3 / model check |
| Smart contract | Plutus / Vyper formal |
| Critical embedded | Frama-C / SPARK |

**기본값**: 매 distributed = TLA+ + 매 lightweight = property-based + 매 critical = full formal proof + 매 LLM-aided 의 modern.

## 🔗 Graph
- 변형: [[Model-Checking]] · [[Theorem-Proving]] · [[Refinement-Type]]
- 응용: [[Coq]] · [[Lean]]
- Adjacent: [[CompCert]] · [[Property-Based-Testing]] · [[TypeScript 타입 시스템 (TypeScript Type System)|Type-System]]

## 🤖 LLM 활용
**언제**: 매 critical / safety. 매 distributed protocol. 매 math research.
**언제 X**: 매 prototype / app code.

## ❌ 안티패턴
- **Formal everything**: 매 cost > benefit.
- **Spec ≠ impl**: 매 verify wrong.
- **Trust model checker for liveness**: 매 fairness need.
- **Skip property test**: 매 cheap form 의 lose.
- **LLM proof 의 trust**: 매 verify with assistant.

## 🧪 검증 / 중복
- Verified (Lamport TLA+, Pierce TAPL, AWS papers, Lean docs).
- 신뢰도 A.

## 🕓 Changelog
| 날짜 | 변경 |
|---|---|
| 2026-04-20 | Auto-reinforced |
| 2026-05-08 | Phase 1 |
| 2026-05-10 | Manual cleanup — methods + 매 TLA / Lean / Coq / Z3 / Dafny / Alloy code |