Loading...
시리즈: 형식 검증 시리즈 · 3부 중 1부 대상 독자: 완전 초심자. 수학, 프로그래밍, 암호학 배경지식이 필요하지 않습니다. 이 글을 읽고 얻게 될 것: 소프트웨어가 정확하다는 것을 증명한다는 의미, 그것이 테스트와 근본적으로 다른 이유, 기계 검증 증명이 무엇인지, 그리고 그러한 증명이 약속할 수 있는 범위의 정확하고 정직한 한계에 대한 명확한 이해.
대부분의 소프트웨어는 테스트되었기 때문에 신뢰받습니다. 많은 입력으로 실행해 보고, 제대로 작동하는지 관찰합니다. 형식 검증은 더 대담한 질문을 던집니다. 아무도 시도할 생각을 하지 못한 입력까지 포함하여, 모든 가능한 입력에 대해 시스템이 해야 할 일을 수행한다는 것을 수학적 확실성으로 증명할 수 있을까요? 이 글은 그 개념을 기초부터 쌓아 올립니다. 먼저 직관을 다루고, 필요한 순간까지 기호는 사용하지 않습니다.
다음은 실화이며, 이 시리즈가 존재하는 이유입니다.
2022년, 프라이버시에 중점을 둔 암호화폐 Zcash는 금액을 숨긴 채 거래할 수 있도록 Orchard라는 새 쉴디드 풀을 출시했습니다. 4년 동안 완벽하게 작동했고 전문 감사를 반복해서 통과했습니다. 그러다 2026년 5월, 한 보안 연구자가 AI 도구의 도움을 받아 기반 수학을 주의 깊게 추론하던 중 시스템 수학의 단 하나의 제약이 부족한 지점을 발견했습니다. 그 단 하나의 빈틈은 공격자가 무제한의 위조 화폐를 만들 수 있게 했을 수 있으며, 금액이 숨겨져 있었기 때문에 누구도 그 일이 일어나는 것을 보지 못했을 것입니다. 결함은 그 모든 기간 내내 존재했습니다.
테스트가 이 결함을 잡아낸 것은 아니었습니다. 모든 테스트는 4년 동안 통과했습니다. 누군가가 수학을 추론하여 찾아낸 것입니다. 그리고 팀은 이를 고쳤을 때 단순히 패치하고 넘어가지 않았습니다. 대체 시스템에 해당 종류의 결함이 전혀 포함될 수 없음을 보이는, 2,700개가 넘는 개별 정리에 걸친 기계 검증 수학적 증명을 작성했습니다.
이것이 형식 검증이며, 이것이 형식 검증이 주는 것입니다. “많은 경우를 시도했고 작동했다”가 아니라 “모든 경우에 성립함을 증명했다”입니다. 한 번 놓친 경우가 재앙적 결과를 낳는 시스템(화폐, 항공기, 의료기기, 암호학)에서는 이 차이가 모든 것을 바꿉니다.
테스트의 사각지대는 수십 년 전 컴퓨터 과학자 에츠허르 데이크스트라가 이름 붙였으며, 지금도 여전히 사실입니다.
테스트는 버그의 존재는 보여줄 수 있지만, 그 부재는 결코 보여줄 수 없습니다.
테스트가 통과했다면, 그 시스템이 그 입력에서 작동한다는 사실을 알게 된 것입니다. 시도하지 않은 입력에 대해서는 아무것도 알지 못하며, 위험한 버그는 거의 항상 아무도 시도하지 않은 경우에 있습니다.
문이 천 개 있는 건물을 책임지고 있으며, 밤마다 모든 문이 잠겼음을 보장해야 한다고 상상해 봅시다.
차이는 현실을 표본 추출하는 것과 설계의 속성을 증명하는 것 사이에 있습니다. 테스트는 표본을 추출합니다. 형식 검증은 증명합니다. 이것이 전체 개념이며, 나머지는 이를 엄밀하게 수행하기 위한 장치입니다.
아무리 고도화된 형식 검증이라도 정확히 세 가지 요소로 구성됩니다. 이들을 명확히 이해하면 나머지는 세부 사항입니다.
| 기둥 | 쉬운 의미 | 건물 비유 |
|---|---|---|
| 명세 | “정확하다”는 것이 무엇을 의미하는지에 대한 정밀한 설명 | “밤에는 모든 문이 잠겨야 한다” |
| 시스템 | 실제로 검사하는 대상(프로그램, 회로, 프로토콜) | 건물과 잠금 메커니즘 |
| 증명 | 시스템이 항상 명세를 충족한다는 엄밀한 논증 | “잠금”을 누르면 모든 문이 잠긴다는 논리적 입증 |
그리고 네 번째, 더 조용한 요소가 전체를 신뢰할 수 있게 만듭니다.
들어본 적 있을 증명 보조기로는 Lean, Rocq(이전의 Coq), Isabelle이 있습니다. 이들은 사실상 대단히 엄격한 논리 검사 엔진입니다. 첫 이야기의 Zcash 증명은 Lean으로 작성되었습니다. 특히 현대 AI 모델은 사람이 안내하는 가운데 이러한 증명을 작성하는 데 점점 더 많이 사용되고 있으며, 한때 수년이 걸리던 작업을 수 주로 줄였습니다. 기계는 여전히 모든 단계를 검사하므로, 속도가 빨라져도 확실성에는 대가가 없습니다.
“증명”이라는 말은 어렵게 느껴질 수 있으므로, 구체적이고 확인 가능한 예시로 이해해 봅시다. 암호학이 아니라 학교 산수만 사용합니다.
주장: 모든 정수 n에 대해, 합 0 + 1 + 2 + ... + n은 n(n+1)/2과 같습니다.
이것을 테스트할 수는 있습니다. n = 5이면 0+1+2+3+4+5 = 15이고, 5 × 6 / 2 = 15입니다. ✓ 일치합니다. n = 10도 시도해 봅시다. 합은 55이고 공식은 10 × 11 / 2 = 55을 줍니다. ✓ (이들은 계산 및 확인되었으며, 실제로 직접 검사하면 이 주장은 0부터 999까지의 모든 n에 대해 성립합니다.)
하지만 값들을 천 개 테스트해도 “모든 정수”에 도달할 수는 없습니다. 정수는 무한히 많습니다. 증명은 귀납법이라는 기법을 사용해 유한한 논증으로 그 무한한 간극을 메웁니다.
n = 0일 때 합은 단지 0이고, 공식은 0 × 1 / 2 = 0을 줍니다. 일치합니다. ✓k에 대해 공식이 성립한다고 가정합시다. 이제 다음 수인 k+1을 더합니다. k+1까지의 합은 (sum up to k) + (k+1) = k(k+1)/2 + (k+1)입니다. 한 줄의 대수적 정리를 통해 이를 (k+1)(k+2)/2로 바꿀 수 있으며, 이는 k 대신 k+1을 넣은 공식과 정확히 같습니다. ✓처음(0)에서 성립하고 각 단계가 이를 다음 수로 이어 주므로, 하나의 유한한 논증으로 모든 정수에 대해, 영원히 성립합니다. 이것이 증명입니다. 증명 보조기는 정확히 이런 추론을 수행하지만, “한 줄의 대수”를 포함한 모든 단계가 실제로 앞선 내용으로부터 따라 나오는지 기계적으로 검증합니다.
반드시 이해할 만한 도약: 증명은 “무한히 많은 경우”를 유한하고 검증 가능한 논증으로 바꿉니다. 이것이 테스트가 구조적으로 갖지 못하는 초능력입니다.
형식 검증이 강력한 이유 중 하나는 애초에 버그가 어디서 발생하는지에 대한 명확한 통찰을 제공하기 때문입니다. 규칙을 검사하는 시스템의 모든 결함은 세 곳 중 하나로 거슬러 올라갑니다.
| 버그의 원천 | 의미 | 증명으로 없앨 수 있을까? |
|---|---|---|
| 명세 | 수학 또는 규칙 자체가 잘못됨(누락된 조건, 잘못된 정의) | 그렇다, 바로 이것이 형식 검증의 핵심 영역입니다 |
| 구현 | 코드가 올바른 명세를 충실히 수행하지 못함 | 부분적으로 가능하며, 이런 실패는 흔히 탐지 가능한 증거를 남깁니다 |
| 깨진 가정 | 전체 시스템이 의존하는 어떤 것이 거짓으로 드러남 | 아니다. 가정은 더 줄일 수 없는 토대입니다 |
이 분류법은 보기보다 더 중요하며, 2부와 3부는 여기에 달려 있습니다. 영원히 숨을 수 있는 가장 깊고 위험한 버그는 대개 명세에 존재합니다. 즉, 시스템이 해야 할 일을 설명하는 수학적 기술에 있습니다. 그리고 명세야말로 기계 검증 증명이 모든 경우를 한 번에 직접 검사할 수 있는 대상입니다. 이것이 진지한 형식 검증 노력이 먼저 이곳을 겨냥하는 이유입니다.
형식 검증은 강력하지만, 그 약속은 정확합니다. 이를 오해하면 사람들을 잘못된 방향으로 이끌 수 있습니다. 따라서 신중하게 말해야 합니다.
증명은 명시된 가정 아래에서 시스템이 명세를 충족함을 보장합니다. 그 이상은 아닙니다.
네 가지 결과가 따르며, 각각 중요합니다.
이러한 정밀함은 형식 검증을 약화시키는 것이 아니라 강점입니다. 무엇을 얻게 되는지 정확히 알려 줍니다. 3부에서 보겠지만, 범위와 가정을 명확히 밝히는 Zcash 팀(“우리는 이름이 명시된 가정하에 공급 건전성을 증명했으며, 프라이버시는 증명하지 않았다”)은 그러한 정직함의 모범입니다.
읽기 쉽게 하기 위해 단순화했습니다. 실제 명세는 영어 문장이 아니라 정확한 형식 언어로 작성됩니다. 서로 다른 문제에 적합한 형식 검증 방식(대화형 정리 증명, 모델 검사, SMT 기반 방법)도 여러 가지입니다. 또한 AI의 도움을 받더라도 이러한 증명을 작성하는 일은 여전히 숙련과 노력이 필요한 작업입니다. 증명 보조기가 내부적으로 논리를 표현하는 방식도 생략했습니다. 그러나 이러한 사실은 핵심을 바꾸지 않습니다. 즉, 명시된 가정하에 명세, 시스템, 그리고 이 둘이 일치함을 기계로 검증한 증명이 있다는 것입니다. 필요해질 때 세부 사항으로 돌아오겠습니다.
| 용어 | 쉬운 의미 |
|---|---|
| Formal verification | 모든 경우에 시스템이 명세를 충족함을 수학적으로 증명하는 것 |
| Specification | “올바른 동작”의 의미에 대한 정밀한 설명 |
| System | 검사 대상인 실제 프로그램, 회로 또는 프로토콜 |
| Proof | 모든 경우에 대해 주장을 확립하는 유한한 논리 단계의 연쇄 |
| Proof assistant / theorem prover | 증명의 모든 단계를 검사하는 소프트웨어(Lean, Rocq, Isabelle) |
| Machine-checked | 사람이 읽어서만 확인한 것이 아니라 컴퓨터가 단계별로 검증함 |
| Induction | 증명 기법. 처음에 참이고 각 단계가 이를 다음 단계로 이어 줌 |
| Assumption | 증명이 의존하는 조건. 거짓이면 보장이 성립하지 않을 수 있음 |
형식 검증이 테스트를 대체하나요? 아니요. 둘은 서로 보완합니다. 테스트는 실무적 문제와 잘못된 가정을 저렴하게 찾아내고, 검증은 테스트가 결코 표본으로 뽑지 못할 수도 있는 버그 전체 부류를 배제합니다.
그렇게 강력하다면 왜 모든 것을 형식 검증하지 않나요? 비용이 많이 들고 전문 기술이 필요하기 때문입니다. 다만 AI 지원이 그 비용을 낮추고 있습니다. 드문 버그가 재앙적 결과를 낳을 시스템에 사용되며, სწორედ 그런 곳에서 그 비용은 가치가 있습니다.
형식 검증된 시스템도 실패할 수 있나요? 그렇습니다. 명세가 잘못되었거나, 정의가 잘못 서술되었거나, 가정이 성립하지 않았거나, 실패가 명세된 범위 밖에 있다면 가능합니다. 증명은 자신이 다룬다고 주장하는 범위만 포괄합니다.
기계 검증 증명이 사람의 증명보다 더 신뢰할 수 있나요? 크고 복잡한 증명에서는 일반적으로 그렇습니다. 기계는 미묘한 빈틈을 놓치거나 대충 넘어가는 설명을 받아들이지 않습니다. 다만 기계도 자신에게 주어진 명세와 정의는 신뢰합니다.
AI가 증명 작성에 도움을 준다면 왜 신뢰할 수 있나요? 증명 보조기가 모든 단계를 기계적으로 검사하기 때문입니다. AI는 단계를 제안하고 기계는 이를 검증합니다. 잘못된 단계는 단순히 거부되므로, AI는 보장을 약화시키지 않으면서 작업 속도를 높입니다.
은행 소프트웨어가 “계좌 잔액이 절대 음수가 되지 않는다”는 것을 증명했습니다. 1년 후에도 여전히 돈이 사라지고 있습니다. 어떻게 둘 다 동시에 참일 수 있을까요? (답은 아래에 있습니다.)
증명은 정확히 한 가지 속성만 보장했습니다. 잔액이 절대 음수가 되지 않는다는 것입니다. 예를 들어 자금을 잘못된 계좌(그래도 음수는 아닌 계좌)로 옮기는 버그나, 명세에 전혀 포함되지 않은 시스템 부분의 결함처럼, 그 속성이 전혀 다루지 않은 방식으로 돈이 사라질 수 있습니다. 검증은 약속한 일을 정확히 수행했을 뿐, 그 이상은 아닙니다. 이것이 6절의 주의사항이 실제로 작동하는 모습입니다. 증명은 명세를 다루지, 상상 가능한 모든 “정확함”의 개념을 다루지는 않습니다.
2부 · Orchard 버그: 이제 실제 2026년 이야기를 자세히 살펴봅니다. 프라이버시 시스템은 암호학적 증명을 통해 금액을 숨겼고, 수학에서 제약이 부족한 한 줄 때문에 그 증명이 거짓말을 하도록 만들 수 있었습니다. 이로 인해 무제한의 보이지 않는 위조가 가능했습니다. “제약이 부족한 회로”가 정확히 무엇인지, 이 종류의 버그가 왜 영원히 숨을 수 있는지, 그리고 왜 이런 일이 한 번 이상 일어났는지 알아보겠습니다.
ZecHub을 위한 Formal Verification 시리즈의 일부입니다.