코드에 버그가 있어도 Lean4로 증명하는 형식 검증

메타데이터

• 원문 제목: Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS
• URL: https://www.youtube.com/watch?v=lRa9sPaMyy4
• 비디오 ID: lRa9sPaMyy4
• 발행일: 2026-08-29
• 채널: aiDotEngineer
• 발표자: Varun Pant, AWS
• 분류: dev-engineering

📌 핵심 질문 / 이 글이 다루는 핵심 논점

==AI 코딩 에이전트가 만든 코드가 모든 입력에서 올바르다는 사실을 어떻게 보장할 것인가? 형식 검증(Formal Verification)은 명세를 수학적 증명으로 바꾸어 코드가 명세를 만족함을 모든 가능한 입력에 대해 확인한다.==

• 대규모 언어 모델을 코드의 심판으로 쓰는 방식은 확률적이며, 테스트는 일부 입력만 검사하고, 사람의 코드 리뷰는 에이전트의 속도를 따라 확장되지 않는다.
• 형식 검증은 사람이 올바름의 의미인 명세(Specification)를 소유하고, 코딩 에이전트가 구현을 만들며, 검증 도구가 구현과 명세의 일치를 증명하는 역할 분담을 만든다.
• Lean4는 정의와 증명을 같은 언어로 표현하고 작은 신뢰 커널(Small Trusted Kernel)로 결과를 독립 확인하므로, 코드 생성 속도가 빨라지는 시대에 강한 정당성 보증을 제공한다.

코딩 에이전트가 매주 수백~수천 개의 PR을 생성하는 환경에서는 “아마 맞을 것”이라는 판단만으로 충분하지 않다. 올바름을 자연어 또는 Lean 명세로 먼저 정하고, 그 명세를 사람이 검토하거나 일부 입력으로 시험한 뒤, 에이전트가 구현하고 증명 도구가 전체 입력 공간에 대한 일치를 확인하는 파이프라인이 필요하다. Lean, Rust 연동 도구, SMT solver, model checker, AWS의 Strata가 이 파이프라인을 여러 프로그래밍 언어로 확장한다.

1. AI 코딩 시대에 형식 검증이 필요한 이유

코드 생산량이 급증할수록 코드의 품질을 추정하는 방법과 모든 입력에 대한 올바름 보증을 분리해야 한다.

1.1. 기존 품질 확인 방식의 한계

1. AI를 코드 심판으로 쓰는 방식은 확률적이다

   1. 대규모 언어 모델을 이용해 코드의 정답 여부를 판단할 수 있지만, 모델의 판단은 확률적 출력이며 수학적 보증이 아니다.
   2. 모델이 높은 확률로 맞는 답을 내놓더라도 모든 가능한 입력에 대해 코드가 정확하다는 결론으로 이어지지 않는다.

2. 테스트는 입력 공간의 일부만 다룬다

   1. 테스트는 선택한 입력과 시나리오에서 기대 동작을 확인하는 데 유용하지만, 선택하지 않은 입력까지 검사하지는 않는다.
   2. 테스트가 모두 통과해도 검사하지 않은 경계 조건이나 조합에서 버그가 남을 수 있으므로, “모든 입력에서 정확하다”는 명제를 직접 증명하지 못한다.

3. 사람의 리뷰는 에이전트의 생산 속도를 따라가기 어렵다

   1. AI 코딩 에이전트가 매주 수백 개에서 수천 개의 PR을 만들면 인간 리뷰어의 처리량이 병목이 된다.
   2. 코드 생성 속도에 맞춰 리뷰 인원을 계속 늘리는 방식은 확장되지 않으며, 사람의 주의력만으로 전체 입력 공간을 검토할 수도 없다.

1.2. 형식 검증이 추가하는 보증

1. 올바름을 명세로 명시한다

   1. 먼저 “정확하다”는 말이 무엇을 뜻하는지 명세(Specification)로 작성한다.
   2. 명세는 자연어로 시작해 AI가 형식 명세로 자동 변환하게 할 수도 있고, 사람이 Lean에서 직접 형식적으로 작성할 수도 있다.

2. 명세에서 구현과 증명을 파생한다

   1. 명세가 확정되면 AI 코딩 에이전트가 그 명세를 만족하는 코드를 구현한다.
   2. 형식 검증 도구는 구현이 명세와 일치한다는 사실을 증명한다.
   3. 증명이 통과하면 가능한 모든 입력에 대해 명세가 말하는 속성이 성립한다.

3. 사람과 기계의 책임을 분리한다

   1. 사람은 upstream에 있는 명세를 소유하고, 명세가 의도와 정확히 일치하는지 검토한다.
   2. 기계는 명세에서 코드를 작성하고 증명 과정을 탐색한다.
   3. 명세는 한 번 쓰고 버리는 문서가 아니라 구현자와 계속 상호작용하는 살아 있는 산출물(Living Artifact)이며, downstream의 코드와 증명 전체가 이 산출물에 의존한다.

1.3. 명세를 먼저 검증해야 하는 이유

1. 잘못된 명세는 완벽하게 증명된 잘못된 프로그램을 만든다

   1. 형식 검증 도구가 증명하는 대상은 사람이 작성하거나 AI가 자동 형식화한 명세다.
   2. 명세 자체가 요구사항을 잘못 표현하면, 구현이 그 명세를 완벽히 만족해도 실제로 원하는 동작과는 달라진다.

2. 초기 검증과 지속적인 검토가 필요하다

   1. 사람의 리뷰로 자연어 명세와 형식 명세가 같은 의미인지 확인할 수 있다.
   2. 일부 입력을 직접 시험해 형식 명세가 의도한 성질을 실제 사례에서도 표현하는지 확인할 수 있다.
   3. 명세가 upstream에 있으므로 이 단계의 오류가 코드·보조 정리·최종 증명 전체로 전파되기 전에 잡아야 한다.

2. Lean4의 구조: 코드와 증명을 하나의 언어로 다루기

Lean은 프로그래밍 언어이면서 proof assistant이며, 코드 정의와 그 성질의 증명을 같은 표현 체계 안에서 연결한다.

2.1. 하나의 언어로 정의와 증명을 작성한다

1. 번역 계층을 없앤다

   1. Lean에서는 프로그램 정의와 증명을 같은 언어로 작성한다.
   2. 코드 표현을 별도의 증명 언어로 번역하는 중간 계층이 없으므로, 구현과 증명이 서로 다른 형식으로 어긋날 위험을 줄인다.

2. 언어 자체를 확장할 수 있다

   1. Lean은 Lean으로 구현되어 있어 새로운 기능과 도구를 언어 안에서 확장하기 쉽다.
   2. 핵심 신뢰 기반은 작게 유지되며, 작은 trusted kernel이 증명 결과를 최종적으로 확인한다.

3. 증명을 독립적으로 재검사할 수 있다

   1. 증명 결과를 내보내 다른 구현이 독립적으로 확인할 수 있다.
   2. 오픈 소스 생태계에는 C++, Rust, Lean으로 작성된 여러 커널을 만들 수 있으며, 누구나 직접 독립 커널을 구현할 수 있다.
   3. Arena Lang 같은 프로젝트에서 커널을 추가하거나 실험할 수 있어, 하나의 검증 구현을 맹목적으로 신뢰하지 않아도 된다.

2.2. 리스트 뒤집기 예제로 보는 정리 증명

1. 코드와 정리를 같은 파일에 둔다

   1. Lean 파일 위쪽에는 리스트를 뒤집는 함수가 정의된다.
   2. 리스트 [1, 2, 3]을 뒤집으면 [3, 2, 1]이 된다는 계산 동작이 코드로 표현된다.

2. 모든 입력을 포괄하는 성질을 정리로 적는다

   1. 파일 중간에는 reverse (A ++ B) = reverse B ++ reverse A라는 성질을 말하는 정리(Theorem)가 놓인다.
   2. 여기서 A와 B는 특정 리스트가 아니라 임의의 리스트이므로, 정리는 가능한 모든 입력에 대해 성립해야 한다.
   3. 개별 예시 [1,2,3]만 계산하는 것과 달리, 이 정리는 리스트 두 개의 연결(concatenation)을 어떻게 뒤집어야 하는지 일반 법칙으로 보증한다.

3. 전술과 커널이 서로 다른 역할을 맡는다

   1. Tactic은 정리를 증명하기 위해 필요한 작업을 자동으로 수행하는 절차다.
   2. Tactic이 만든 증명 과정을 작은 커널이 검사하며, 커널은 전술의 결과를 믿는 것이 아니라 결과가 실제 정리를 증명하는지 확인한다.

2.3. 체스판 비유로 이해하는 증명 탐색

1. 정리는 체크메이트 목표와 같다

   1. 체스에서 목표는 상대를 체크메이트하는 것이고, 플레이어는 나이트와 비숍을 움직이며 목표에 접근한다.
   2. Lean에서는 정리의 증명이 체크메이트 목표에 해당하고, tactic이 체스판 위에서 선택하는 수에 해당한다.

2. 증명은 탐색 트리를 따라 진행된다

   1. 하나의 목표에 여러 tactic을 차례로 적용하면서 증명 상태를 바꾼다.
   2. 어떤 가지에서는 목표를 증명할 수 없으므로 뒤로 돌아가(backtrack) 다른 tactic 또는 다른 가지를 시도한다.
   3. 여러 갈래의 탐색 끝에 정리를 완성하는 목표 상태를 찾으면, 독립 커널이 최종 결과를 확인한다.

3. 커널이 잘못된 수를 잡아낸다

   1. 증명 상단에 잘못된 증명을 제시하면 커널이 즉시 거부한다.
   2. 따라서 사용자가 신뢰해야 하는 핵심 구성 요소는 복잡한 tactic 탐색기 전체가 아니라 작고 독립적으로 점검 가능한 커널이다.

3. Lean으로 전체 코드를 형식화하는 사례

자연어 요구사항을 형식 명세로 바꾸고, AI가 Lean 코드를 작성한 뒤, 보조 정리들을 거쳐 최종 정리를 커널로 확인하는 흐름이 실제 라이브러리에 적용된다.

3.1. C 압축 라이브러리 zlib를 Lean으로 옮기기

1. 오픈 소스 변환 작업

   1. 오픈 소스 프로젝트 Andreo.AI는 C로 작성된 압축 라이브러리 zlib를 Lean으로 변환했다.
   2. 변환에는 약 일주일이 걸렸으며, 단순한 번역이 아니라 명세와 증명이 함께 있는 Lean 구현을 구축하는 작업이었다.

2. 자연어 요구사항에서 형식 명세로 이동한다

   1. 자연어 요구사항은 “압축(compress)의 결과를 압축 해제(decompress)하면 원래 데이터가 돌아와야 한다”는 내용이다.
   2. AI가 이 요구사항을 형식 명세로 생성한다.
   3. 형식 명세를 만든 뒤에는 그 명세가 정말 원하는 압축의 의미를 표현하는지 검토하는 일이 핵심이다.

3. AI가 코드와 보조 정리를 만든다

   1. 명세가 확인되면 AI가 Lean으로 코드를 작성한다.
   2. 증명 과정에서 최종 명제를 직접 해결하기 어려운 부분은 여러 helper lemma이라는 하위 목표(subgoal)로 분해된다.
   3. 각 하위 목표는 tactic으로 증명되고, 완성된 보조 정리들이 최종 정리로 조립된다.

4. 작은 커널이 대규모 증명을 확인한다

   1. 32,000줄의 증명으로 이루어진 꽤 큰 사례라도, 최종 결과는 작은 독립 커널이 검사한다.
   2. AI가 문제를 분해하고 tactic으로 각각의 목표를 풀었다는 사실만으로 끝나지 않고, 커널이 조립된 최종 정리가 명세를 실제로 따르는지 확인한다.

3.2. 구현 언어와 명세 언어를 분리하는 Cedar

1. Rust 생산 코드와 Lean 명세를 결합한다

   1. Cedar는 오픈 소스 authorization policy language다.
   2. AWS Verified Permissions와 AWS의 접근 제어 시스템에서 사용되며, Cedar의 기능 명세는 Lean으로 작성되고 production code는 Rust로 실행된다.

2. 정책 의미를 일반 법칙으로 표현한다

   1. 예를 들어 어떤 요청이 forbid 정책을 만족한다면 그 요청은 언제나 거부되어야 한다.
   2. 특정 사례의 출력만 확인하는 것이 아니라, 모든 관련 입력에서 forbid가 항상 deny로 이어지는 정책 의미를 명세로 고정한다.

3. 차분 무작위 테스트로 두 구현을 대조한다

   1. 같은 입력을 Rust production code와 Lean functional specification에 각각 넣는다.
   2. 두 구현이 동일한 입력에서 동일한 결과를 내는지 differential random testing으로 확인한다.
   3. 매일 밤 약 1억 건의 차분 무작위 테스트를 실행하며, 이 조건이 충족되지 않으면 어떤 버전도 출시하지 않는다.

4. Rust 코드의 연역적 검증과 solver

Lean의 tactic 탐색이 체스판에서 수를 찾는 과정이라면, solver는 수식에 대한 답을 계산하는 강력한 계산기다.

4.1. Solver의 역할과 Z3

1. 수식의 만족 가능성을 계산한다

   1. Solver에 수식(formula)을 입력하면 결과로 satisfiable 또는 unsatisfiable을 반환한다.
   2. 모든 증명 단계를 사람이 직접 탐색하는 Lean tactic과 달리, 특정 종류의 논리 문제를 빠르게 계산하는 엔진이다.

2. Z3를 검증 엔진으로 사용한다

   1. Verus는 오픈 소스 도구이며, 강력한 solver인 Z3를 사용한다.
   2. Rust 코드에 명세를 주석처럼 추가하면서 생산 코드와 검증 조건을 가까운 위치에 둘 수 있다.

4.2. Verus의 사전 조건과 사후 조건

1. requires로 이전 조건을 선언한다

   1. requires는 함수가 실행되기 전에 무엇이 참이어야 하는지를 나타내는 precondition이다.
   2. 입력 범위, 자료구조의 불변식, 호출자가 보장해야 하는 조건을 이 위치에 명시할 수 있다.

2. ensures로 이후 결과를 선언한다

   1. ensures는 함수가 실행된 뒤 무엇이 참이어야 하는지를 나타내는 postcondition이다.
   2. verifier는 사전 조건이 주어졌을 때 코드의 실행이 사후 조건을 만족하는지를 정적으로 검사한다.

3. 검증 코드는 실행 시 사라진다

   1. 이 검사는 정적(static) 검증이며 runtime에 강제되는 일반 비즈니스 로직이 아니다.
   2. requires와 ensures 같은 검증용 주석은 ghost code와 비슷하게 취급되어 실행 바이너리에서는 제거된다.

4.3. Rust를 Lean으로 기능적으로 번역하는 Eneus

1. 중간 표현에서 번역한다

   1. Eneus는 Rust의 mid-level intermediate representation을 사용한다.
   2. Rust 프로그램을 Lean에서 다룰 수 있는 functional representation으로 번역한다.

2. 번역 뒤에 동일한 증명 환경을 적용한다

   1. 번역이 끝나면 Lean의 동일한 theorem prover와 체스판에 해당하는 증명 환경을 사용한다.
   2. Rust로 배포되는 프로그램의 동작을 Lean 명세·정리와 연결해 연역적으로 검증할 수 있다.

5. 모든 프로그래밍 언어로 확장하는 AWS Strata

특정 언어에 종속된 변환기를 넘어, 여러 언어를 공통 중간 표현으로 낮추고 여러 검증 엔진에 분배하는 확장 계층이 필요하다.

5.1. 언어별 dialect와 컴파일러 구조

1. 임의의 언어를 위한 dialect를 만든다

   1. AWS는 Strata라는 오픈 소스 도구를 개발 중이며, 작업이 진행 중인 상태다.
   2. 사용자는 자신이 원하는 프로그래밍 언어에 맞는 dialect를 만들 수 있다.

2. 고수준 IR을 Strata core로 낮춘다

   1. 구조는 컴파일러와 유사하다. 각 언어의 high-level intermediate representation을 공통 low-level intermediate representation으로 lowering한다.
   2. 공통 하위 표현인 Strata core는 Lean으로 작성된다.

5.2. 공통 표현에서 여러 엔진으로 분배한다

1. 프로그램을 하나의 검증 언어로 모은다

   1. 여러 언어의 프로그램이 Strata core라는 같은 언어로 표현되면, 서로 다른 원천 언어를 같은 기반에서 분석할 수 있다.
   2. 언어마다 별도의 검증 파이프라인을 처음부터 만들 필요가 줄어든다.

2. 목적에 맞는 검증 엔진을 선택한다

   1. 정리와 tactic을 이용하는 Lean proof engine으로 증명할 수 있다.
   2. 수식의 만족 가능성을 계산하는 SMT solver로 보조할 수 있다.
   3. 프로그램의 상태 공간을 탐색하는 model checker로 검증할 수도 있다.

3. 형식 검증의 적용 범위를 넓힌다

   1. Strata의 목표는 특정 언어의 코드만 확인하는 것이 아니라, 각 언어를 공통 표현으로 연결해 Lean 증명·SMT solver·model checker를 함께 활용하는 것이다.
   2. 작업이 완료되면 AI 코딩 에이전트가 생성한 다양한 언어의 코드에도 명세와 증명을 연결할 수 있다.

6. 엔지니어가 바로 시작하는 방법

형식 검증은 미래의 연구 주제에 머물지 않으며, 브라우저에서 Lean을 실행하고 가장 중요한 코드부터 명세화하는 방식으로 시작할 수 있다.

6.1. 핵심 코드부터 선택한다

1. 실패 비용이 큰 코드를 고른다

   1. 전체 코드베이스를 한 번에 형식화하기보다, 보안·권한·데이터 변환처럼 오류 비용이 큰 핵심 로직을 먼저 선택한다.
   2. 어떤 동작을 보장해야 하는지 명확히 말할 수 있는 작은 단위부터 시작하면 명세와 증명의 경계를 관리하기 쉽다.

2. 올바름의 의미를 먼저 쓴다

   1. 자연어로 요구사항을 적고 AI에게 형식화를 맡기거나 Lean으로 직접 명세를 작성한다.
   2. 자동 형식화 결과를 사람이 검토하고, 일부 입력을 시험해 명세가 의도한 동작을 표현하는지 확인한다.

6.2. 에이전트와 검증 도구를 연결한다

1. 구현은 명세에서 생성한다

   1. 명세가 확정되면 코딩 에이전트가 구현을 작성하게 한다.
   2. 구현 과정에서 필요한 helper lemma과 하위 목표는 증명 탐색 과정의 일부로 다룬다.

2. 도구가 전체 입력을 증명하게 한다

   1. Lean kernel, Verus/Z3, Eneus, Strata 같은 도구 중 코드와 요구사항에 맞는 엔진을 사용한다.
   2. 통과한 증명은 테스트한 일부 입력을 넘어, 명세가 정의한 모든 가능한 입력에 대한 보증을 제공한다.

주요 발언 모음

“AI 에이전트가 그 어느 때보다 많은 코드를 생성하고 있다.”

“어떻게 이것이 정확하다는 것을 알 수 있는가?”

“형식 검증은 모든 입력에 대해 코드가 올바르다는 수학적 증명을 제공할 수 있다.”

“사람은 명세를 소유하고, 기계는 코드와 증명을 소유한다.”

“명세는 upstream에 있다. 나머지 모든 것은 그 명세의 downstream이다.”

“Lean은 정의와 증명을 위한 같은 언어이며, 번역 계층이 없다.”

“체크메이트를 얻으면 작고 독립적인 커널이 그것을 확인한다.”

“이제 소프트웨어와 시스템이 ‘아마도 올바른(probably correct)’ 수준이 아니라 ‘증명된 올바름(provably correct)’을 갖기를 바란다.”

핵심 데이터 & 수치

• 코드 생산량: AI 코딩 에이전트와 빌더가 매주 수백 개에서 수천 개의 PR을 만들 수 있다.
• zlib 변환 기간: C 압축 라이브러리 zlib를 Lean으로 옮기는 작업은 약 일주일에 걸쳐 진행됐다.
• zlib 증명 규모: 최종 사례에는 32,000줄의 proof가 포함됐다.
• Cedar 테스트 규모: Rust production code와 Lean 명세를 비교하는 differential random test를 매일 밤 약 1억 건 실행한다.
• 출시 조건: Cedar는 차분 무작위 테스트 조건이 충족되지 않으면 어떤 버전도 출시하지 않는다.
• 신뢰 기반: 복잡한 tactic과 검증 도구의 결과는 작은 trusted kernel이 최종적으로 검사한다.

결론 및 시사점

1. AI가 코드를 빠르게 생성할수록 코드 생성 자체보다 “올바름”을 정의하는 명세가 더 중요한 upstream 자산이 된다.
2. 명세를 사람이 검토하고 소유하면 AI의 확률적 생성 능력을 기계적으로 확인할 수 있는 구현·증명 파이프라인으로 바꿀 수 있다.
3. Lean은 코드와 증명을 같은 언어에 놓고 작은 커널로 결과를 확인해 형식 검증의 신뢰 경계를 작게 유지한다.
4. Rust를 사용하는 Cedar, Verus, Eneus는 형식 명세와 생산 코드가 반드시 같은 언어일 필요는 없으며, 차분 테스트나 기능적 번역으로 연결할 수 있음을 보여준다.
5. Strata는 여러 프로그래밍 언어를 Lean 기반의 공통 IR로 낮추고 proof engine, SMT solver, model checker를 선택적으로 연결하는 확장 방향을 제시한다.
6. 형식 검증은 모든 코드를 한 번에 증명하라는 요구가 아니라, 실패 비용이 큰 핵심 코드의 계약과 불변식을 먼저 증명하는 실무적 워크플로로 시작할 수 있다.

핵심 요약 (20줄)

AI 코딩 에이전트가 만드는 코드의 양이 폭증하면서 모든 입력에 대한 올바름을 보장하는 방법이 필요해졌다. 언어 모델의 코드 평가는 확률적이므로 수학적 정확성 보증을 대신할 수 없다. 테스트는 선택한 입력만 검사하므로 검사하지 않은 경계 조건의 버그를 배제하지 못한다. 인간 코드 리뷰는 에이전트가 매주 생산하는 수백~수천 개의 PR을 처리할 만큼 확장되지 않는다. 형식 검증은 명세를 만족하는 코드라는 사실을 모든 가능한 입력에 대해 수학적으로 증명한다. 사람은 코드가 올바르다는 뜻을 명세로 정하고 그 명세의 의미를 검토해야 한다. AI 코딩 에이전트는 검증된 명세에서 구현을 생성하고 증명 과정에 필요한 하위 목표를 만든다. Lean4는 프로그램 정의와 증명을 같은 언어로 표현해 별도 번역 계층에서 생기는 불일치를 줄인다. Lean의 작은 trusted kernel은 tactic이 만든 복잡한 증명 결과를 독립적으로 재검사한다. Lean의 증명 탐색은 체스에서 여러 수를 시도하고 막힌 가지에서 되돌아가는 과정과 닮았다. zlib의 Lean 변환 사례는 자연어 요구사항을 형식 명세와 수만 줄 규모의 증명으로 확장할 수 있음을 보여준다. Cedar는 Lean으로 작성한 authorization 명세와 Rust production code를 함께 사용한다. Cedar는 매일 밤 약 1억 건의 differential random test를 통과해야 새 버전을 출시한다. Verus는 Rust 코드에 requires와 ensures를 선언하고 Z3 solver로 사전 조건과 사후 조건을 정적으로 확인한다. Verus의 검증용 조건은 runtime에 실행되지 않고 ghost code처럼 제거된다. Eneus는 Rust의 mid-level intermediate representation을 Lean의 기능적 표현으로 번역한다. AWS의 Strata는 임의의 언어를 dialect로 연결해 Lean으로 작성된 공통 Strata core로 낮추려는 도구다. Strata core에서 Lean proof engine과 SMT solver와 model checker를 목적에 따라 선택할 수 있다. 실무자는 오류 비용이 큰 핵심 코드부터 올바름의 의미를 명세하고 일부 입력으로 명세를 검토하면 된다. 검증된 명세와 작은 신뢰 커널을 결합하면 소프트웨어를 “아마도 올바른” 상태에서 “증명된 올바름” 상태로 끌어올릴 수 있다.