Formal Verification — SAT/BDD, SMT, and Symbolic Execution (Foundry Invariants, Halmos) TODO

Algorithms · Day 34 / 100 · B. Compilers, Runtimes & VMs (Day 20-35)

Concept

Formal verification doesn't test a handful of inputs like testing does — it logically determines whether a stated property holds across the entire defined input space. At the foundation are SAT solvers (CDCL-based) that solve propositional-logic satisfiability, and BDDs, which represent Boolean functions in a canonical form relative to a variable ordering; on top of these sit SMT solvers, which layer in theories like bit-vectors, arrays, and arithmetic. Symbolic execution runs a program on symbols instead of concrete values, collecting the path condition at every branch, then hands that condition together with the negation of the property to an SMT solver to search for a counterexample. Practical tools differ in character: Foundry's invariant tests are stateful random fuzzing — finding a counterexample is conclusive, but not finding one is not a proof — while symbolic execution tools like Halmos give a proof, but only within a bounded scope such as a fixed loop-unrolling depth. So you always need to state explicitly "a proof under which assumptions and within which bounds."

Smart contracts are hard to patch after deployment and failure costs mean lost funds, so the state space that unit tests can't cover has to be blocked off property by property. At the same time, misunderstanding the scope of a tool's guarantee buys you the false comfort of thinking "it's verified" when it isn't.

Code & Formula

# 형식 검증 — SAT(브루트포스 충족가능성 판정)와 심볼릭 실행(경로 조건 수집 후 반례 탐색)의 최소 예제.
# 실제로는 CDCL SAT/SMT 솔버를 쓰지만, 작은 변수 공간에서는 완전 탐색으로도 같은 개념을 보여줄 수 있다.

from itertools import product

def sat_solve(clauses, variables):
    """clauses: [[('x',True), ('y',False)], ...] 형태의 CNF. 모든 대입을 완전 탐색해 충족 대입을 찾는다."""
    for values in product([False, True], repeat=len(variables)):
        assignment = dict(zip(variables, values))
        if all(any(assignment[var] == want for var, want in clause) for clause in clauses):
            return assignment
    return None  # UNSAT

# (x OR y) AND (NOT x OR y) AND (x OR NOT y)  ->  x=True, y=True 를 만족해야 한다.
clauses = [[('x', True), ('y', True)], [('x', False), ('y', True)], [('x', True), ('y', False)]]
model = sat_solve(clauses, ['x', 'y'])
print("SAT model:", model)

def vault_withdraw(balance, amount, is_owner):
    """검증 대상 함수: 소유자만, 그리고 잔고 범위 안에서만 출금할 수 있어야 한다는 invariant를 건다."""
    if is_owner and amount <= balance:
        return balance - amount
    return balance  # 조건 불충족이면 상태 불변

def invariant_holds(balance):
    return balance >= 0  # 성질: "잔고는 절대 음수가 될 수 없다"

# 심볼릭 실행: 입력 변수(balance, amount, is_owner)를 구체값 대신 작은 범위 전체로 탐색해
# 경로마다 invariant 위반 여부를 SMT 대신 브루트포스로 판정한다.
counterexample = None
for balance in range(0, 5):
    for amount in range(0, 7):
        for is_owner in (False, True):
            result = vault_withdraw(balance, amount, is_owner)
            if not invariant_holds(result):
                counterexample = (balance, amount, is_owner, result)
                break

print("invariant: withdraw 후 balance >= 0")
print("counterexample found:", counterexample)  # None 이면 이 유한 범위 안에서는 증명된 것
print("proved within explored bounds:", counterexample is None)

docs/code/algorithms/algorithms-34.py

Exercise

Put an invariant like "the sum of all users' balances ≤ the contract's collateral balance" on a simple collateral vault contract, run it through Foundry's invariant tests, then verify the same property symbolically with Halmos, and compare the two results and their run times.

Practical Connection

Verex's Conditional Tokens settlement path is a perfect fit for invariants like "the sum of each condition's outcome-slot balances never exceeds the deposited collateral" and "total redeem amount after resolve = collateral amount" — exactly the kind of conservation property invariants are meant to pin down.

Where it lands in Jayverse

• Verex: write the invariant test this week, not just the property. Add the Foundry invariant "sum of outcome-slot balances ≤ collateral" to the Conditional Tokens path now, then run the same property through Halmos with an explicit bound (market count, loop-unrolling depth) written into the test file itself.
• DeFi: give liquid-staking accounting the same conservation invariant. "Total shares priced ≤ total assets held" is the EtherFi-style equivalent of Verex's collateral check — add it as a Foundry invariant before any devnet deploy of the staking contracts.
• Bridge: state the lock-mint conservation invariant and its bound. "Locked amount on Anvil equals minted amount on Sepolia" is the bridge's version of the same property — write it as a Foundry invariant first, and once the contract is small enough, check it with Halmos under a stated bound.

If you study this on a given day, add a note link and a ✅ to this line in the source curriculum (docs/knowledge/dev-100-curriculum.md) and this spot will lead straight to the note body. You can also write directly on this page — but regenerating overwrites it, so it's safer to keep anything you want to save as markdown under docs/algorithms/.

한국어

형식 검증 TODO

Algorithms · Day 34 / 100 · B. 컴파일러·런타임·VM (Day 20–35)

SAT/BDD·SMT·심볼릭 실행(Foundry invariant·Halmos) (TAOCP 4권 SAT 접목)

개념

형식 검증은 테스트처럼 몇 개 입력을 시험하는 대신, 명시한 성질이 정의된 입력 공간 전체에서 성립하는지를 논리적으로 판정한다. 바닥에는 명제 논리의 충족 가능성을 푸는 SAT 솔버(CDCL 기반)와 불리언 함수를 변수 순서에 대해 정규형으로 표현하는 BDD가 있고, 그 위에 비트벡터·배열·산술 같은 이론을 얹어 판정하는 SMT 솔버가 있다. 심볼릭 실행은 프로그램을 구체적 값 대신 심볼로 실행하며 분기마다 경로 조건을 모으고, 그 조건과 성질의 부정을 SMT에 던져 반례를 찾는다. 실무 도구는 성격이 다른데, Foundry의 invariant 테스트는 상태를 가진 랜덤 퍼징이라 반례를 찾으면 확실하지만 못 찾았다고 증명이 되진 않고, Halmos 같은 심볼릭 실행 도구는 루프 전개 깊이 등으로 제한된 범위 안에서 증명을 준다. 따라서 "어떤 가정과 어떤 경계 안에서의 증명인가"를 항상 함께 명시해야 한다.

스마트 컨트랙트는 배포 후 수정이 어렵고 실패 비용이 자금 손실이라, 단위 테스트가 커버하지 못하는 상태 공간을 성질 단위로 막아야 한다. 동시에 도구가 주는 보장의 범위를 오해하면 "검증했다"는 잘못된 안심을 사게 된다.

코드 · 수식

# 형식 검증 — SAT(브루트포스 충족가능성 판정)와 심볼릭 실행(경로 조건 수집 후 반례 탐색)의 최소 예제.
# 실제로는 CDCL SAT/SMT 솔버를 쓰지만, 작은 변수 공간에서는 완전 탐색으로도 같은 개념을 보여줄 수 있다.

from itertools import product

def sat_solve(clauses, variables):
    """clauses: [[('x',True), ('y',False)], ...] 형태의 CNF. 모든 대입을 완전 탐색해 충족 대입을 찾는다."""
    for values in product([False, True], repeat=len(variables)):
        assignment = dict(zip(variables, values))
        if all(any(assignment[var] == want for var, want in clause) for clause in clauses):
            return assignment
    return None  # UNSAT

# (x OR y) AND (NOT x OR y) AND (x OR NOT y)  ->  x=True, y=True 를 만족해야 한다.
clauses = [[('x', True), ('y', True)], [('x', False), ('y', True)], [('x', True), ('y', False)]]
model = sat_solve(clauses, ['x', 'y'])
print("SAT model:", model)

def vault_withdraw(balance, amount, is_owner):
    """검증 대상 함수: 소유자만, 그리고 잔고 범위 안에서만 출금할 수 있어야 한다는 invariant를 건다."""
    if is_owner and amount <= balance:
        return balance - amount
    return balance  # 조건 불충족이면 상태 불변

def invariant_holds(balance):
    return balance >= 0  # 성질: "잔고는 절대 음수가 될 수 없다"

# 심볼릭 실행: 입력 변수(balance, amount, is_owner)를 구체값 대신 작은 범위 전체로 탐색해
# 경로마다 invariant 위반 여부를 SMT 대신 브루트포스로 판정한다.
counterexample = None
for balance in range(0, 5):
    for amount in range(0, 7):
        for is_owner in (False, True):
            result = vault_withdraw(balance, amount, is_owner)
            if not invariant_holds(result):
                counterexample = (balance, amount, is_owner, result)
                break

print("invariant: withdraw 후 balance >= 0")
print("counterexample found:", counterexample)  # None 이면 이 유한 범위 안에서는 증명된 것
print("proved within explored bounds:", counterexample is None)

docs/code/algorithms/algorithms-34.py

연습

간단한 담보 볼트 컨트랙트에 "모든 사용자 잔고 합 ≤ 컨트랙트 담보 잔액" 같은 invariant를 걸고 Foundry invariant 테스트로 돌린 뒤, 같은 성질을 Halmos로 심볼릭 검증해 두 결과와 실행 시간을 비교하라.

실무 · Verex 연결

Verex의 Conditional Tokens 정산 경로는 "각 조건의 outcome 슬롯 잔고 합이 예치된 담보를 넘지 않는다", "resolve 이후 redeem 총액 = 담보액" 같은 보존 성질을 invariant로 못 박기에 딱 맞는 대상이다.

Jayverse에서의 위치

• Verex: 속성뿐 아니라 인바리언트 테스트를 이번 주에 작성한다. "각 조건의 결과 슬롯 잔액 합 ≤ 담보"라는 Foundry 인바리언트를 Conditional Tokens 경로에 지금 추가하고, 같은 속성을 Halmos로도 돌리되 테스트 파일 안에 명시적 경계(마켓 수, 루프 언롤링 깊이)를 적어둔다.
• DeFi: 유동성 스테이킹 회계에도 같은 보존 인바리언트를 적용한다. "가격이 매겨진 총 지분 ≤ 보유 총자산"이 EtherFi식 스테이킹에서 Verex 담보 체크에 대응하는 값이다. devnet에 스테이킹 컨트랙트를 배포하기 전에 Foundry 인바리언트로 추가한다.
• Bridge: lock-mint 보존 인바리언트와 그 경계를 명시한다. "Anvil에서 잠긴 양 = Sepolia에서 발행된 양"이 브릿지 버전의 같은 속성이다. 먼저 Foundry 인바리언트로 적고, 컨트랙트가 충분히 작아지면 명시된 경계 아래 Halmos로도 확인한다.

공부한 날 원본 커리큘럼(docs/knowledge/dev-100-curriculum.md)의 이 줄에 노트 링크와 ✅ 를 붙이면, 이 자리는 노트 본문으로 바로 이어집니다. 노트 없이 이 페이지에 바로 적어도 됩니다 — 다만 다시 생성하면 덮어쓰이므로, 남길 글은 docs/algorithms/ 의 마크다운으로 쓰는 편이 안전합니다.