2nd/10_Wiki/Topic_Programming/DevOps_and_Security/Formal-Verification-of-Software.md

id, title, category, status, canonical_id, aliases, duplicate_of, source_trust_level, confidence_score, verification_status, tags, raw_sources, last_reinforced, github_commit, tech_stack

id	title	category	status	canonical_id	aliases	duplicate_of	source_trust_level	confidence_score	verification_status	tags	raw_sources	last_reinforced	github_commit	tech_stack
wiki-2026-0508-formal-verification-of-software	Formal Verification of Software	10_Wiki/Topics	verified	self	Formal Methods Program Verification	none	A	0.9	applied	formal-methods verification correctness		2026-05-10	pending	language framework Coq/Lean/TLA+ 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

---- 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

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

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

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

#[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

#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)

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)
• 응용: 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