Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

한 줄 핵심

코딩 에이전트의 출력은 테스트·리뷰만으로는 전 입력에 대한 정당성을 보장할 수 없으므로, Lean 같은 형식 검증 도구로 사양은 사람이 정의하고 증명은 기계가 맡는 방식이 가장 강한 안전장치가 된다.

시간별 요약

1. 0:00
   일반적인 점검으로는 에이전트 결과를 다 검증할 수 없는 이유 LM 심사, 테스트, 인간 코드리뷰는 모두 일부 입력만 확인할 뿐 전 입력에 대해 코드가 올바르다고 말해주지 못한다. 형식 검증은 코드가 무엇을 만족해야 하는지 사양을 정하고, 그 사양을 만족한다는 수학적 증명을 통해 모든 입력에 대한 정당성을 제공한다.
2. 1:06
   사양은 사람이, 증명은 기계가 맡는 구조 사양을 먼저 정의한 뒤 인간이 검토하거나 일부 입력으로 시험해 검증하고, 그 다음 AI coding agent가 구현을 작성하면 formal verification tool이 구현이 사양과 일치함을 증명한다. 사양은 상위에 있는 살아 있는 산출물이고, 나머지는 그 아래에서 따라오는 구조다.
3. 2:00
   코드와 증명을 하나의 언어로 다루는 Lean Lean은 프로그래밍 언어이자 proof assistant로, 정의와 증명을 같은 언어로 작성할 수 있어 번역층이 없다. 작은 trusted kernel을 갖고 있어 증명은 내보낸 뒤 독립적으로 다시 검사할 수 있으며, 코드와 theorem이 같은 파일에 함께 존재한다.
4. 3:01
   전술, 정리, 그리고 체스 비유 Lean에서는 tactics로 증명 단계를 진행하고 kernel이 최종 검사를 맡는다. 증명 과정은 체스처럼 목표를 향해 여러 수를 두며 탐색하고, 막히면 되돌아가 다른 가지를 시도하는 트리 탐색에 가깝다.
5. 3:58
   독립적으로 다시 만들 수 있는 작은 커널 잘못된 증명은 kernel에서 즉시 거절되므로, 신뢰해야 할 범위는 매우 작은 핵심부에 한정된다. kernel은 C++, Rust, Lean 등으로 여러 구현을 둘 수 있고, 이를 직접 다시 작성해 검증할 수도 있다.
6. 4:52
   zlib를 Lean으로 옮기고 32,000줄의 증명을 만든 사례 zlib를 Lean으로 옮긴 사례에서는 자연어 사양을 formal spec으로 만들고, AI가 Lean 코드와 보조 lemma를 생성한 뒤 tactics로 각 subgoal을 풀어 최종 theorem을 완성했다. 이 작업은 32,000 lines of proof 규모였고, 마지막 검사는 작은 독립 kernel이 수행했다.
7. 6:44
   Cedar: Lean 의미론, Rust 운영 코드 Cedar는 정책 언어의 사양을 Lean으로 두고 프로덕션 코드는 Rust로 운영하며, 두 구현이 같은 입력에서 같은 출력을 내는지 differential random testing으로 검증한다. nightly에 약 100 million 테스트를 돌리고, 만족할 때까지 버전을 출시하지 않는다.
8. 7:40
   솔버, 전제조건, 그리고 런타임에서 지워지는 코드 solver는 식을 넣으면 satisfiable/unsatisfiable 같은 결과를 돌려주는 계산기처럼 작동하며, Verus는 Z3를 활용한다. requires와 ensure로 표현하는 precondition과 postcondition은 정적 검증되지만 런타임에는 사라져 일종의 ghost code처럼 취급된다.
9. 8:37
   어떤 언어든 같은 핵심으로 끌어오는 방법 Strata는 어떤 프로그래밍 언어든 dialect로 받아 high-level IR을 Strata core라는 low-level IR로 내리는 Lean 기반 도구다. 모든 프로그램을 같은 핵심 언어로 맞춘 뒤 Lean proof, SMT solver, model checker 같은 여러 엔진에 분배해 검증할 수 있다.

실무 인사이트

• 코딩 에이전트의 산출물은 테스트보다 사양 품질이 더 중요하므로, 먼저 사람이 검토 가능한 명세를 만드는 흐름을 표준 프로세스로 두는 것이 효과적이다.
• 전사적 도입보다 오류 비용이 큰 핵심 코드부터 Lean, solver, differential testing을 붙여 검증 강도를 단계적으로 높이는 편이 현실적이다.
• 형식 검증을 도입할 때는 런타임 성능보다 사전 조건·사후 조건, 보조 정리, kernel 신뢰 경계를 먼저 설계해야 운영 적용이 쉬워진다.