Formal Verification — SAT/BDD, SMT, and Symbolic Execution (Foundry Invariants, Halmos) TODO
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.
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/.