📐 형식 검증 Formal Verification

🧮 쉽게 풀면 — 답 몇 개 맞춰보는 게 아니라 공식을 증명하는 것

수학 시험에 비유해볼게요. 일반 테스트는 몇 문제의 답을 확인해보는 것과 같아요 — 틀린 게 없다면 안심되지만, 모든 숫자를 다 넣어본 건 아니죠. 형식 검증은 공식 자체가 맞는지 증명하는 것과 같아요. 증명됐다면 어떤 숫자를 넣어도 성립해요. 크립토에서 '공식'은 스마트 컨트랙트이고, 형식 검증은 그 컨트랙트의 모든 가능한 입력값을 한꺼번에 따져봐요.

⚙️ 실제로 어떻게 작동하나요?

먼저 개발자가 형식 명세(formal specification)를 작성해요. "풀이 보유한 것보다 많이 내줄 수 없다"처럼, 컨트랙트가 항상 지켜야 할 조건을 정밀하게 정리한 목록이에요. 그러면 자동화 도구가 코드를 실제로 실행하지 않고 수학적으로 검사해서, 이 규칙이 깨질 수 있는지 따져봐요. 코드가 안전하면 도구가 증명을 내놓고, 아니면 규칙을 깨는 정확한 입력값을 돌려줘요.

단계	무슨 일이 일어나나요?
📝 명세 작성	사람이 컨트랙트가 절대 위반하면 안 되는 규칙을 써요
🤖 검사	도구가 몇 가지 테스트 케이스 대신 모든 가능한 입력값을 대상으로 따져봐요
✅ 결과	규칙이 성립한다는 증명, 또는 규칙이 깨지는 반례를 출력해요

🔧 자주 등장하는 도구: Certora Prover, Solidity 내장 SMTChecker, 증명 시스템인 Coq·Isabelle·K framework. Mythril이나 Manticore도 연관된 분석 도구예요.

🔒 크립토에서 왜 중요한가요?

배포된 스마트 컨트랙트는 앱처럼 패치할 수 없는 경우가 많아요 — 대부분 변경 불가예요. 그런데 대규모 자산을 담고 있을 때가 많으니, 버그 하나가 영구적이고 되돌릴 수 없는 손실로 이어질 수 있어요. 형식 검증이 가치 있는 이유가 여기 있어요. 빠른 테스트나 사람의 검토로는 놓칠 수 있는 재진입 공격(reentrancy)이나 정수 오버플로우(integer overflow) 같은 미묘한 버그 유형을 잡아낼 수 있거든요.

🤝 감사(audit)를 대체하지는 않아요

형식 검증과 스마트 컨트랙트 감사는 서로 다른 위험을 커버해요. 그래서 진지한 프로젝트는 둘 다 써요. 형식 검증은 코드가 명세를 지키는지 증명하고, 사람 감사자는 다른 질문을 해요 — 명세와 설계 자체가 합리적인가, 어떤 규칙도 잡아내지 못한 취약점은 없는가? 어느 하나만으로는 빈틈이 생겨요.

🌍 입문자가 어디서 마주치나요?

• 📊 DeFi 감사 리포트 — "formally verified" 또는 "verified by Certora" 같은 표현이 DeFi 보안 리포트에 자주 등장해요
• 🏦 메이커다오(DAI) — DAI의 핵심 엔진이 K framework로 형식 검증됐어요
• 🔁 유니스왑 — AMM 수식(x·y=k)과 v4의 지급능력이 Certora Prover로 형식 검증됐어요 (유니스왑)
• 🛡️ 다른 프로토콜 — Aave 등도 Certora Prover를 활용해요 (벤더 주장이므로 범위 수치는 참고용으로만)

❓ 자주 묻는 질문

'형식 검증 완료'라고 하면 버그가 없고 해킹도 불가능한 건가요?

아니요. 코드가 주어진 규칙을 지킨다는 것만 증명해요. 규칙 자체가 불완전하거나 잘못됐다면 실제 버그가 그대로 남을 수 있습니다. 강력한 근거이지 안전 보장은 아니에요.

형식 검증이 일반 테스트와 다른 점이 뭔가요?

테스트는 몇 가지 예시 입력값만 확인하고, 버그가 '있다'는 사실만 드러낼 수 있어요. 형식 검증은 가능한 모든 입력값을 한 번에 따져보며, 작성된 규칙 범위 안에서 어떤 버그 유형 자체가 존재하지 않음을 증명하는 것이 목표예요.

코드가 형식 검증됐다면 수동 감사(audit)를 건너뛰어도 되나요?

아니요. 둘은 서로 다른 위험을 커버해요. 형식 검증은 코드가 명세를 지키는지 증명하고, 사람 감사자는 그 명세와 설계 자체가 합리적인지 따져봐요. 제대로 된 프로젝트는 둘 다 씁니다.

🔗 관련 용어·코인