Files

T

Antigravity Agent f8b21af4be Wiki cleanup: error-doc removal, dedup merge, link normalization

10_Wiki/Topics 대규모 정리:
- 오류 캡처/미완성 stub 문서 227개 제거
- 교차폴더 중복 43클러스터 병합 (63파일 → redirect)
- 링크명 정규화: 깨진 링크 수정·redirect 직결·개념 매핑 ~2,400건
- 카테고리 MOC 6개 신규 생성
- Graph 섹션 미해결 related-keyword 링크 10,058건 제거

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

2026-05-20 23:52:15 +09:00

5.9 KiB

Raw Blame History

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

title

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

Type systems: lightweight, daily (TypeScript, Rust borrow checker).
Property-based testing: empirical, partial (QuickCheck).
Model checking: finite-state exhaustive (TLA+, SPIN).
Deductive verification: machine-checked proofs (Coq, Lean, Dafny, F*).
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).

매 응용

Safety-critical (avionics DO-178C Level A, automotive ISO 26262).
Crypto libraries (HACL*, Project Everest).
Distributed protocols (Paxos, Raft TLA+).
Smart contracts (Cardano Plutus, MoveProver).
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

5.9 KiB Raw Blame History