logo

[번역] AI가 세상의 소프트웨어를 작성할 때, 누가 검증하는가?

검증이 생성과 같은 속도로 확장되지 않는다면, 상황은 더 나빠질 것이며, 빠르게 나빠질 것입니다.

April 21, 2026

원문: https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-the-worlds-software.html

AI가 세상의 소프트웨어를 작성할 때, 누가 검증하는가?

AI가 세상의 소프트웨어를 다시 작성하고 있습니다

Code Metal은 최근 AI를 사용해 방위 산업 코드를 재작성하기 위해 1억 2,500만 달러를 투자받았습니다. Google과 Microsoft 모두 새로운 코드의 25~30%가 AI로 생성된다고 보고합니다. AWS는 AI를 사용해 Toyota의 4,000만 줄 COBOL 코드를 현대화했습니다. Microsoft의 CTO는 2030년까지 모든 코드의 95%가 AI로 생성될 것이라고 예측합니다. 세상의 소프트웨어를 다시 작성하는 일은 다가오는 미래가 아닙니다. 이미 진행 중입니다.

Anthropic은 최근 병렬 AI 에이전트를 사용하여 2주 만에, 2만 달러 미만의 비용으로 10만 줄짜리 C 컴파일러를 구축했습니다. 이 컴파일러는 Linux를 부팅하고 SQLite, PostgreSQL, Redis, Lua를 컴파일합니다. AI는 이제 놀라운 속도로 대규모 소프트웨어를 생산할 수 있습니다. 하지만 컴파일러의 정확성을 증명할 수 있을까요? 아직은 아닙니다.

아무도 결과에 대한 형식 검증을 수행하고 있지 않습니다.

Andrej Karpathy는 이런 패턴을 다음과 같이 묘사했습니다. "저는 항상 '모두 수락'을 누릅니다. 더 이상 diff를 읽지 않아요." AI 코드가 대부분의 경우 충분히 좋으면, 사람은 꼼꼼한 검토를 멈춥니다. AI가 생성한 코드의 절반 가까이가 기본적인 보안 테스트를 통과하지 못하며, 더 새롭고 더 큰 모델도 이전 모델보다 훨씬 더 안전한 코드를 생성하지 못합니다. 오류는 분명히 존재합니다. 하지만 검토자는 없습니다. Karpathy조차 AI를 신뢰하지 않습니다. 그는 이후 "실제로 중요한 코드"를 위한 신중한 워크플로를 제시했으며, 자신의 중요한 프로젝트를 만들 때는 직접 코드를 작성했습니다.

규모가 커지면 어떤 일이 발생하는지 생각해 보겠습니다. OpenSSL의 단 하나의 버그 Heartbleed는 수백만 사용자의 개인 통신을 노출시켰고, 2년간의 코드 리뷰를 통과했으며, 업계에 수억 달러의 비용을 들여 해결하게 했습니다. 한 명의 사람이 하나의 라이브러리에 도입한 하나의 버그였습니다. AI는 이제 소프트웨어 스택의 모든 계층에 걸쳐 천 배 빠른 속도로 코드를 생성하고 있으며, 우리가 의존하는 방어 수단(코드 리뷰, 테스트, 수동 검사)은 2년간 Heartbleed를 놓친 바로 그 수단들입니다.

Harvard Business Review는 최근 "워크슬롭(workslop)"이라 부르는 현상을 지적했습니다. 이는 AI가 생성한 결과물 중 겉보기에는 완성도 높아 보이지만, 결국 후속 작업에서 수정이 필요한 것들을 말합니다. 그 작업물이 메모라면 단지 짜증나는 정도이지만, 암호화 라이브러리와 같은 중요한 문서라면 치명적인 문제로 이어질 수 있습니다. AI가 소프트웨어 생산 속도를 높인다고 해서 검증 격차는 줄어들기는커녕 오히려 벌어지고 있습니다. 엔지니어들은 자신들이 개발한 시스템의 작동 방식을 제대로 이해하지 못하게 되었습니다. AI에 위임되는 것은 코드 작성만이 아닙니다. 사고까지 위임됩니다.

위협은 우발적 오류를 넘어섭니다. AI가 소프트웨어를 작성할 때, 공격 표면이 바뀝니다. 훈련 데이터를 오염시키거나 모델의 API를 침해할 수 있는 공격자는 AI가 접촉하는 모든 시스템에 미묘한 취약점을 주입할 수 있습니다. 가상의 위험이 아닙니다. 공급망 공격은 이미 사이버 보안에서 가장 치명적인 공격 중 하나이며, AI가 생성한 코드는 이전에 존재하지 않았던 규모의 새로운 공급망을 만들어냅니다. 전통적인 코드 리뷰로는 의도적으로 미묘한 취약점을 안정적으로 탐지할 수 없으며, 단단히 마음먹은 공격자는 테스트 스위트를 연구하여 이를 회피하도록 설계된 버그를 심을 수 있습니다. 형식 명세가 방어 수단입니다. 코드를 생성한 AI에 의존하지 않고, '정확하다'는 것이 무엇을 의미하는지를 독립적으로 정의합니다. 무언가 깨지면, 어떤 가정이 실패했는지 정확히 알 수 있으며, 감사자도 마찬가지입니다.

2022년 Consortium for Information & Software Quality의 연구 결과에 따르면, 소프트웨어 품질 저하는 이미 미국 경제에 연간 2.41조 달러의 비용을 초래하고 있습니다. 이 수치는 AI가 주요 기업에서 새로운 코드의 4분의 1 이상을 작성하기 시작하기 전에 계산된 것입니다. LLVM과 Clang의 창시자인 Chris Lattner는 직설적으로 말했습니다. AI는 좋은 구조든 나쁜 구조든 가리지 않고 증폭시킵니다. AI 의 속도로 만들어진 나쁜 코드는 "이해할 수 없는 악몽"이 됩니다. AI가 세계의 핵심 인프라(금융 시스템, 의료 기기, 국방, 교통)에서 점점 더 많은 비중을 차지하면서, 검증되지 않은 코드는 단순한 품질 문제가 아니라 시스템적 위험이 됩니다.

오늘날 대부분의 핵심 소프트웨어는 잘 작동합니다. 테스트, 코드 리뷰, 그리고 오랜 경험을 통해 유능한 엔지니어들이 유지보수하고 있습니다. 문제는 모든 것이 망가져 있다는 것이 아닙니다. AI가 소프트웨어 생산의 규모와 속도를 우리의 검증 능력보다 빠르게 바꾸고 있다는 것입니다. 사람의 속도에서 작동하는 것이 AI의 속도에서도 살아남지 못할 수 있습니다.

검증이 생성과 같은 속도로 확장되지 않는다면, 상황은 더 나빠질 것이며, 빠르게 나빠질 것입니다.

수학적 증명이 필요한 이유

테스트와 증명은 상호 보완적입니다. 프로퍼티 기반 테스트와 퍼징(fuzzing)을 포함한 테스트는 강력합니다. 버그를 빠르고, 저렴하고, 종종 놀라운 방식으로 잡아냅니다. 하지만 테스트는 확신(confidence)을 줍니다. 증명은 보장(guarantee)을 줍니다. 이 차이는 중요하며, 테스트에서 얻는 신뢰가 실제로 얼마나 높은지 정량화하기 어렵습니다. 소프트웨어에는 정확성의 증명, 즉 컴퓨터가 빈틈없이 자동으로 검사하는 증명이 동반될 수 있습니다. AI가 증명을 저렴하게 만들면, 증명이 더 강력한 선택지가 됩니다. 하나의 증명이 모든 가능한 입력, 모든 엣지 케이스, 모든 인터리빙(interleaving, 실행 순서의 모든 조합)을 커버합니다. 검증된 암호화 라이브러리는 더 나은 엔지니어링이 아닙니다. 수학적 보증입니다.

예를 들어 보겠습니다. AI가 TLS 라이브러리를 다시 작성합니다. 코드는 모든 테스트를 통과합니다. 하지만 명세는 상수 시간 실행을 요구합니다. 어떤 분기도 비밀 키 자료에 의존하면 안 되고, 어떤 메모리 접근 패턴도 정보를 유출하면 안 됩니다. AI의 구현에는 키 비트에 따라 달라지는 미묘한 분기가 포함되어 있습니다. 테스트에도, 코드 리뷰에도 보이지 않는 타이밍 사이드채널입니다. 상수 시간 동작에 대한 형식 증명은 이를 즉시 포착합니다. 증명이 없으면 그 취약점은 프로덕션에 배포됩니다. 이러한 저수준 프로퍼티를 증명하려면 적절한 추상화 수준에서의 검증이 필요하며, 이것이 플랫폼이 타이밍, 메모리 레이아웃, 기타 하드웨어 수준의 관심사에 대한 추론을 위해 특화된 하위 언어를 지원해야 하는 이유입니다.

Claude C 컴파일러는 반대편을 보여줍니다. 정확성이 아닌 테스트 통과에 최적화되어 있습니다. 테스트 스위트를 만족시키기 위해 값을 하드코딩합니다. 일반화되지 않습니다. 프로퍼티 기반 테스트는 이 특정 사례를 포착할 가능성이 높지만, 일반적인 문제는 남아 있습니다. 고정된 테스트 전략이 있으면, 충분히 적대적인 시스템은 그에 과적합할 수 있습니다. 증명은 조작할 수 없습니다. 구성적으로(by construction) 모든 입력을 커버합니다.

수동으로 코드를 작성할 때의 마찰은 신중한 설계를 유도했습니다. AI는 이러한 마찰, 심지어 유익한 마찰까지도 제거합니다. 해답은 AI의 속도를 늦추는 것이 아닙니다. 오히려 인간의 마찰을 수학적 마찰로 대체하는 것입니다. AI가 빠르게 움직이되, 자신의 작업을 증명하게 하는 것입니다. 새로운 마찰은 생산적입니다. 명세와 모델을 작성하고, "정확하다"는 것이 정확히 무엇을 의미하는지 정의하고, 생성하기 전에 설계하는 것입니다.

장애물은 항상 비용이었습니다. 수작업으로 증명을 작성하는 것은 광범위하게 적용하기에 너무 비쌌습니다. AI가 경제성을 바꾸고 있습니다. 증명이 대규모로도 충분히 실용적인 선택지가 되어가고 있습니다.

발전을 가속하다

대부분의 사람은 검증을 비용으로 생각합니다. 즉, 개발에 대한 세금으로 여기며, 안전이 매우 중요한 시스템에서만 정당화된다고 봅니다. 하지만 이러한 관점은 시대에 뒤떨어졌습니다. AI가 검증된 소프트웨어를 검증되지 않은 소프트웨어만큼 쉽게 생성할 수 있을 때, 검증은 더 이상 비용이 아니라 개발을 촉진하는 촉매제가 됩니다.

가치는 검증 행위 자체에 있지 않습니다. 검증된 결과물이 열어주는 가능성에 있습니다. 새로운 하드웨어를 위해 ML 커널을 제공하는 회사를 생각해 보겠습니다. 오늘날에는 테스트와 검증에 수개월이 소요됩니다. AI가 커널을 작성하고 한 번에 정확성을 증명하면, 그 기간은 수 시간으로 단축됩니다. 현재 1년 걸리는 것이 수 주 만에 납품되는, 증명 가능하게 정확한 하드웨어 설계는 산업 전체의 경제성을 바꿉니다.

검증, 테스트, 명세가 항상 병목이었습니다. 구현이 아닙니다. 좋은 엔지니어는 무엇을 만들어야 하는지 압니다. 단지 정확성을 증명할 여유가 없을 뿐입니다. 그 비용이 거의 0에 가까워지면, 정확성이 중요한 모든 분야가 가속됩니다. 항공우주, 자동차, 의료기기 인증은 현재 수년간의 검증 노력이 필요합니다. 클라우드 제공자도 보안 핵심 서비스와 암호화 구현 검증에 비슷한 노력을 투자합니다. 검증된 코드 생성은 이 기간을 수 주로 단축할 수 있습니다. 단 하나의 버그가 수억 달러의 비용을 초래할 수 있는 하드웨어 검증도 동일한 혜택을 받습니다.

이러한 가속에는 명세, 즉 소프트웨어가 무엇을 해야 하는지에 대한 정밀하게 기술하는 문서가 필요합니다. AI가 구현을 맡으면서, 명세 작성이 핵심 엔지니어링 분야가 됩니다. 명세를 작성하면 시스템이 무엇을 해야 하는지, 어떤 불변량을 유지해야 하는지, 무엇이 잘못될 수 있는지에 대한 명확한 사고가 강제됩니다. 진정한 엔지니어링 작업은 항상 바로 이 명세 작성 과정에서 이루어졌습니다. 과거에는 구현 과정이 더 큰 비중을 차지했을 뿐입니다.

명세를 작성하는 것이 항상 쉬운 것은 아니지만, 최적화된 구현을 작성하는 것보다는 쉽습니다. 그리고 강력한 지름길이 있습니다. 분명히 정확하지만 비효율적인 프로그램이 그 자체로 명세 역할을 할 수 있습니다. 사용자와 AI가 함께 단순한 모델을 작성하고, AI가 효율적인 버전을 작성한 뒤, 둘이 동치임을 증명합니다. 어려운 부분이 구현에서 설계로 옮겨가는 것입니다. 이것이 바로 우리가 원하는 종류의 어려움입니다.

핵심 시스템에만 국한되지 않습니다. 버그가 비싼 모든 비자명한 엔지니어링 프로젝트(대부분이 그렇듯)는 정확성이 저렴해질 때 가속됩니다.

검증 플랫폼에 필요한 것

AI 시대를 위한 검증 플랫폼에는 무엇이 필요할까요?

작고 신뢰할 수 있는 커널. 모든 증명의 모든 단계를 기계적으로 검사하는, 불과 수천 줄의 코드입니다. 나머지 모든 것(AI, 자동화, 사람의 지도)은 신뢰 경계 밖에 있습니다. 서로 다른 언어(Lean, Rust)로 구현된 독립적인 재구현들이 교차 검증 역할을 합니다. 복잡한 AI나 솔버를 신뢰할 필요가 없습니다. 완전히 감사할 수 있을 만큼 작은 커널로 증명을 독립적으로 검증하면 됩니다. 검증 계층은 코드를 생성하는 AI와 분리되어야 합니다. AI가 핵심 소프트웨어를 작성하는 세상에서, 검증자는 마지막 방어선입니다. 같은 벤더가 AI와 검증을 모두 제공한다면 이해충돌이 발생합니다. 독립적 검증은 철학적 선호가 아닙니다. 보안 아키텍처 요구사항입니다. 플랫폼은 오픈소스여야 하며 단일 벤더가 통제해서는 안 됩니다.

이 플랫폼은 프로그래밍 언어이면서 동시에 정리 증명기 역할을 모두 수행해야 하며, 코드와 증명을 하나의 시스템에 통합하여 변환 과정에서의 간극이 없어야 합니다. AI에게 구조화되고 점진적인 피드백을 제공하는 풍부하고 확장 가능한 택틱(tactic) 프레임워크가 필요합니다. 현재 목표가 무엇인지, 사용 가능한 가설이 무엇인지, 각 단계 이후 무엇이 바뀌었는지를 알려주는 것입니다. AI가 증명 탐색을 제어해야 하며, 블랙박스에 위임해서는 안 됩니다.

대안으로 제시된, 중간 상태 없이 성공 또는 실패라는 이진적인 결과만 반환하는 푸시버튼 솔버(push-button solver)는 AI에게 학습할 자료를 제공하지 않고 탐색 방향을 제시할 방법도 없습니다. 더 심각한 문제는 휴리스틱 솔버에 의존하는 증명은 솔버가 업데이트되거나 개발자가 명세 작성 방식을 약간만 변경해도 깨지는 경우가 많다는 것입니다. 변경이 논리적으로 동치인 경우에도 그렇습니다. 재현 불가능한 기반 위에 신뢰할 수 있는 AI 파이프라인을 구축할 수 없습니다. (이에 대해 최근 Stanford 강연에서 자세히 논의했습니다.)

이를 위해서는 구축할 수 있는 가장 큰 형식화된 지식 라이브러리가 필요합니다. 소프트웨어를 검증하는 것은 수학입니다. 추상대수학에서 정리를 증명하는 것과 동일한 추론이 암호화 라이브러리가 명세를 올바르게 구현하는지 증명합니다. 수학자와 엔지니어 모두를 위한 플랫폼은 타협이 아닙니다. 엄밀한 추론이 소수에 적용되든 프로토콜 정확성에 적용되든 하나의 분야라는 인식입니다.

그리고 뛰어난 확장성이 필수적입니다. 사용자와 AI는 시스템 내부 구조에 접근하는 확장을 작성할 수 있어야 합니다. 커스텀 도구, 자동화, 도메인 특화 추론 엔진을 구축할 수 있어야 합니다. 이러한 움직임은 이미 현실화되고 있습니다. AI 에이전트가 플랫폼 위에서 자체 증명 전략을 구축하고 있습니다. 플랫폼이 사용자에게 적응하는 것이지, 그 반대가 아닙니다.

AI 커뮤니티는 이미 방향을 정했습니다. AlphaProof(Google DeepMind), Aristotle(Harmonic), SEED Prover(ByteDance), Axiom, Aleph(Logical Intelligence), 그리고 Mistral AI 모두 Lean 위에서 구축합니다. 국제 수학 올림피아드에서 메달 수준의 성과를 달성한 모든 주요 AI 추론 시스템이 Lean을 사용했습니다. 경쟁 플랫폼을 사용한 곳은 하나도 없습니다. 미래는 오늘날의 초기 애플리케이션보다 훨씬 거대합니다.

Lean은 역대 최대 규모의 일관된 형식화된 수학 체계인 Mathlib을 기반으로 합니다. 20만 개 이상의 형식화된 정리와 750명의 기여자가 있습니다. 다섯 명의 필즈상 수상자가 Lean과 교류하고 있습니다. 동일한 플랫폼이 정리를 형식화하는 수학자와 프로덕션 시스템을 검증하는 엔지니어 모두를 위해 작동합니다. ACM SIGPLAN은 2025 프로그래밍 언어 소프트웨어 상으로 이 융합을 인정했습니다. "Lean은 AI 기반 수학적 추론 시스템의 사실상 표준이 되었습니다."

이미 기업 팀이 프로덕션에서 Lean을 사용하고 있습니다. AWS는 Cedar 인가 정책 엔진을 검증했고, Microsoft는 SymCrypt 암호화 라이브러리를 검증하는 데 Lean을 사용하고 있습니다. 8,000개 이상의 GitHub 저장소에 Lean 코드가 있습니다. 20만 명 이상의 사용자가 프로그래밍 환경을 설치했습니다. 매일 700명 이상이 Lean Zulip 채널에서 활동합니다. 전 세계 연구 그룹이 생태계에 기여합니다. Chris Lattner가 관찰한 대로, 수동 재작성과 변환 작업은 AI 네이티브 작업이 되고 있습니다. AI가 세계의 코드베이스를 다시 작성할 것입니다. 어떤 플랫폼에서 하느냐가 매우 중요합니다.

Lean은 이미 Haskell 및 OCaml과 비견되는 성능을 보여줍니다. 더 높은 성능이 필수적인 경우, Lean 모델을 Lean 내에 임베딩된 효율적인 명령형 코드로 변환할 수 있으며, 깔끔한 의미론과 C의 정의되지 않은 동작 없이 가능합니다. 우리는 성능이 중요한 코드에 대한 남은 격차를 좁히기 위해 적극적으로 작업하고 있습니다. 진정한 비교는 Lean 대 C가 아닙니다. 검증된 코드 대 검증되지 않은 코드입니다.

Lean은 12년 이상의 지속적인 개발의 결과입니다. 신뢰할 수 있는 커널, 컴파일러, 언어 서버, IDE, 증명 자동화에 이르기까지 모든 계층을 처음부터 설계하고 구축했습니다. 팀은 20명입니다. 커뮤니티가 독립적으로 Lean을 선택했습니다. 수학자, AI 연구자, 기업 엔지니어 모두가 동일한 플랫폼 위에서 구축하고 있습니다.

다가올 미래의 전조

Lean FRO의 선임 연구 소프트웨어 엔지니어 Kim Morrison은 최근 우리의 기대를 훨씬 뛰어넘는 실험을 진행했습니다. AI 에이전트가 수많은 시스템에 내장된 널리 사용되는 C 압축 라이브러리인 zlib을 최소한의 인간 지도로 Lean으로 변환했습니다. 특별한 도구는 만들지 않았습니다. 정리 증명을 위한 특별한 훈련 없이 범용 AI인 Claude를 그대로 사용했습니다. 워크플로는 네 단계로 구성되었습니다. 첫째, AI가 핵심인 DEFLATE 알고리즘을 포함하여 zlib 압축 형식의 깔끔하고 읽기 쉬운 Lean 구현을 만들었습니다. 둘째, Lean 버전이 라이브러리의 기존 테스트 스위트를 통과하여 동작 동치성을 확인했습니다. 셋째, 핵심 프로퍼티가 테스트가 아닌 수학 정리로 진술되고 증명되었습니다. 핵심 정리는 다음과 같습니다.

theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8)
    (hsize : data.size < 1024 * 1024 * 1024) :
    ZlibDecode.decompressSingle (ZlibEncode.compress data level) = .ok data

이것은 압축된 버퍼를 해제하면 전체 zlib 형식에서 모든 압축 수준에 걸쳐 항상 원본 데이터를 반환한다는 기계 검증된 증명입니다. 크기 전제 조건(hsize)은 증명 엔지니어링의 산물입니다. AI가 증명을 구성하면서 사용할 수 있는 연료(fuel, 재귀 깊이 제한)의 상한을 설정합니다. 사람 엔지니어라면 이를 제거했을 것입니다. 지도 없이 작업한 AI는 증명을 완료하기에 충분한 한계를 선택했습니다. AI 역량과 플랫폼 도구가 모두 개선되면 이러한 산물은 사라질 것입니다. 원시 DEFLATE 및 gzip 프레이밍 라운드트립도 증명되었습니다. 넷째, 최적화된 버전이 개발 중이며 검증된 모델과의 동치성이 증명되고 있습니다. 이 작업은 진행 중입니다.

전체 증명은 최소한의 인간 지도와 특별한 도구 없이 구성되었습니다. 이 결과는 AI가 오늘날 프로덕션 소프트웨어를 검증된 형태로 변환할 수 있음을 보여줍니다. 아직 가능하리라고 예상되지 않았던 일입니다.

zlib은 깔끔한 RFC 명세를 가진 순차 알고리즘으로, 데이터베이스 엔진이나 분산 시스템보다 단순합니다. 이 결과와 검증된 소프트웨어 스택 사이의 격차는 실재합니다. 하지만 최근까지 프로덕션 소프트웨어에 대한 AI 생성 증명을 보여준 사람은 없었습니다. 궤적이 시작점보다 중요합니다. 결정적으로, zlib 증명은 정리 증명을 위한 특별한 훈련 없이 범용 AI가 생성했습니다. 커스텀 모델이 필요하지 않았습니다. 이는 검증된 소프트웨어의 장벽이 더 이상 AI 역량이 아님을 의미합니다. 장벽은 이제 플랫폼이 얼마나 잘 갖춰져 있느냐입니다. 범용 AI가 개선되면서 병목은 전적으로 검증 플랫폼으로 이동합니다. AI에게 얼마나 풍부한 피드백을 제공하는지, 자동화가 얼마나 강력한지, 구축할 수 있는 사전 지식 라이브러리가 얼마나 큰지가 관건입니다.

zlib 워크플로는 테스트가 구조적으로 할 수 없는 것도 드러냅니다. 테스트와 코드가 같은 잘못된 가정을 공유하면, 테스트는 아무것도 찾지 못합니다. 증명하는 행위는 모든 가정을 명시적으로 만들도록 강제합니다. 설계자가 프로퍼티를 진술하고, AI가 이를 정밀한 형식 문장으로 변환한 뒤, 증명을 구성하거나 명세가 수정되어야 함을 발견합니다. 잘못된 가정은 충족될 수 없는 증명 의무로 드러납니다. 명세는 증명을 시도하는 과정에서 더 날카로워집니다.

이 접근법은 순차 알고리즘을 넘어 가장 어려운 버그가 존재하는 분산 시스템으로 확장됩니다. NUS의 Ilya Sergey 그룹은 모델 검사와 완전한 형식 증명을 결합하는 Lean 기반 분산 프로토콜 검증기 Veil을 구축했습니다. 프로퍼티가 성립하지 않을 때, Veil은 모델 검사기처럼 실패를 보여주는 구체적인 반례, 즉 실제 실행 추적을 생성합니다. 성립할 때는 특정 한계까지의 반례 부재가 아닌 완전한 형식 증명을 생성합니다. Veil은 무작위 합의 프로토콜인 Rabia를 포함한 프로토콜을 검증하여 임의의 노드 수에 대한 합의와 유효성을 증명했습니다. 검증 과정에서 팀은 두 개의 별도 도구에서 감지되지 않았던 Rabia의 이전 형식 검증에서의 불일치를 발견했습니다. 더 단순한 프로토콜의 경우, Claude Code가 필요한 보조 불변량 대부분을 수 분 내에 추론할 수 있습니다.

더 큰 그림이 궤적을 확인해 줍니다. Lean을 사용하는 AI 시스템이 수십 년간 인간의 노력으로도 풀리지 않던 미해결 수학 문제를 해결했습니다. 한 수학자가 AI 에이전트와 함께 3주 만에 완전한 소수 정리를 형식화했습니다. 25,000줄의 Lean, 1,000개 이상의 정리입니다. 이전 형식화에는 1년 이상과 수십 명의 기여자가 필요했습니다. 필즈상 수상자 Maryna Viazovska의 E8 격자가 8차원에서 최적의 구 패킹이라는 증명이 Lean으로 형식 검증되었으며, AI 에이전트가 마지막 단계를 완료했습니다. Google DeepMind의 AlphaEvolve는 새로운 수학적 구성을 발견했고, AlphaProof는 Lean으로 증명을 형식화했습니다. 발견에서 검증된 증명까지 완전한 AI 파이프라인입니다.

생산성 격차가 벌어지고 있습니다. 최고의 도구를 가진 팀이 더 앞서 나가는 반면 다른 팀은 정체합니다. 검증 능력은 결정적인 경쟁 우위가 될 것입니다.

검증된 스택

이것이 향하는 곳은 명확합니다. 계층별로, 핵심 소프트웨어 스택이 수학적 증명이 내장된 형태로 재구성될 것입니다. 문제는 이것이 일어나느냐가 아니라 언제 일어나느냐입니다.

이미 시작되고 있습니다. 생태계가 성장하고 있습니다. 스타트업이 증명 데이터로 AI를 훈련하고, 검증 도구를 구축하고, 인재를 키우고 있습니다. 1단계는 Lean을 사용하여 기존 코드를 검증하는 것입니다. 2단계는 재구성입니다. 처음부터 증명이 내장된 형태로 Lean에서 스택을 구축하는 것입니다. 두 단계 모두 같은 플랫폼에서 이루어집니다. 둘 다 플랫폼을 강화합니다.

대상은 현대 소프트웨어 스택의 기반입니다. 다른 모든 것이 신뢰하는 암호화. 모든 소프트웨어의 구성 요소인 핵심 라이브러리(데이터 구조, 알고리즘, 압축). 지구상의 모든 기기에 내장된 SQLite와 같은 스토리지 엔진. 모든 메시지가 통과하는 파서와 프로토콜 구현(JSON, HTTP, DNS, 인증서 검증). 그리고 다른 모든 것을 빌드하는 컴파일러와 런타임.

모든 스마트폰, 모든 브라우저, 모든 주요 운영 체제에 내장된 SQLite를 생각해 보겠습니다. 검증된 SQLite는 쓰기 중 충돌이 데이터베이스를 손상시킬 수 없고, 동시 읽기가 부분적 트랜잭션을 절대 볼 수 없다는 증명을 제공합니다. Jepsen이나 상태 기반 프로퍼티 기반 테스트 같은 도구가 실제로 이런 버그를 많이 찾지만, 신뢰를 제공하지 보증을 제공하지는 않습니다. 수학적 증명은 모든 충돌 지점과 모든 인터리빙을 커버합니다.

검증된 각 구성 요소는 영구적인 공공재입니다. 독점 소프트웨어와 달리, 검증된 오픈소스 라이브러리는 품질이 저하되거나 보증이 조용히 철회되거나 단일 회사의 사업 결정에 좌우되지 않습니다. 증명은 공개됩니다. 누구나 감사하고, 그 위에 구축하고, 보증을 유지하면서 구현을 교체할 수 있습니다. 가장 깊은 의미에서의 인프라입니다. 모두의 기준선을 높여줍니다. 이 스택 위에 구축하면 증명을 상속받습니다. 각 계층은 독립적입니다. 플랫폼과 방법론이 먼저이며, 이후 작업은 자연스럽게 병렬화됩니다.

검증된 컴포넌트가 저렴해지면, 확신을 가지고 조합할 수 있습니다. 오늘날 대부분의 버그는 통합에서 발생합니다. 컴포넌트 간의 경계, 정확히 일치하지 않는 가정들입니다. 통합 테스트가 존재하는 이유는 바로 컴포넌트 테스트가 조합되지 않기 때문입니다. 두 컴포넌트의 유닛 테스트가 통과해도 함께 작동하는지에 대해서는 아무것도 알 수 없습니다. 검증된 인터페이스는 근본적으로 다릅니다. 각 컴포넌트가 공유된 명세에 대한 증명을 제공하면, 구성의 정확성이 구조적으로 보장됩니다. 각 조각을 독립적으로 검증하고 전체가 건전하다는 것을 알 수 있습니다. 이점은 초선형적(superlinear)으로, 즉 시스템이 커질수록 가속적으로 확장됩니다. 시스템이 클수록 테스트된 것과 검증된 것 사이의 격차가 벌어집니다.

이것이 만드는 세상

목표는 검증된 소프트웨어 스택입니다. 오픈소스이고, 자유롭게 사용할 수 있으며, 수학적으로 정확성이 보장된 것입니다. 핵심 시스템을 구축하는 개발자들이 오늘날 오픈소스 라이브러리를 선택하듯 검증된 컴포넌트를 선택합니다. 다만 테스트가 아닌 증명을 제공합니다. 단일 팀이 혼자 이것을 구축하지 않으며, 단일 플랫폼이 영원히 올바른 것이라는 보장도 없습니다. 중요한 것은 검증된 소프트웨어가 표준이 되는 것입니다. Lean보다 더 나은 것이 나타난다면, 그래도 미션은 성공한 것입니다. 전체 커뮤니티를 위한 열린 도전입니다.

엔지니어의 역할은 변하지만 축소되지는 않습니다. 엔지니어는 명세와 모델을 작성하는 데 더 많은 시간을 쏟고, 더 높은 수준의 추상화에서 시스템을 설계하며, 시스템이 무엇을 해야 하는지, 어떤 불변량을 유지해야 하는지, 어떤 실패를 감수해야 하는지를 정밀하게 정의합니다. 작업은 덜 창의적이 되는 것이 아니라 더 창의적이 됩니다. 생성하기 전에 설계하고, 만들기 전에 생각하는 것입니다. 생산성은 더 많은 코드를 생성하는 데서 오는 것이 아니라 첫 시도에서 증명 가능하게 정확한 코드를 생성하는 데서 옵니다.

명세는 순수하게 기술적이지 않은 질문도 제기합니다. "정확하다"는 것이 무엇을 의미하는지 누가 결정하는가? 의료 기기, 투표 시스템, AI 안전 모니터를 위한 명세는 논리뿐만 아니라 가치를 인코딩합니다. 명세를 형식화하고 공개적으로 만드는 것이 이런 질문을 해결하지는 않지만, 숨겨진 코드로는 절대 할 수 없는 방식으로 명시적이고 감사 가능하게 만듭니다. AI 자체가 접근성 격차를 메울 수 있습니다. 검증된 코드를 생성하는 시스템이 명세를 평이한 언어로 설명하여, 형식 보증을 작성하는 전문가를 넘어서 접근 가능하게 만들 수 있습니다.

AI 산업은 이 결과에 전략적 이해관계를 갖습니다. 증명 가능하게 정확한 코드를 생성하는 AI는 단지 그럴듯한 코드를 생성하는 AI와 질적으로 다릅니다. 검증은 AI 코드 생성을 생산성 도구에서 신뢰 인프라로 변환합니다.

AI는 세상의 소프트웨어 상당 부분을 작성하게 될 것입니다. 아직 예상할 수 없는 방식으로 수학, 과학, 공학을 발전시킬 것입니다. 문제는 누군가가 그 결과의 정확성을 증명할 수 있느냐는 것입니다.

Lean은 오픈소스이며 lean-lang.org에서 자유롭게 사용할 수 있습니다. Lean을 배우려면 문서부터 시작하세요. 커뮤니티에 참여하려면 Lean Zulip을 방문하세요. Lean Focused Research Organization이 플랫폼을 구축하고 유지합니다. 이 작업을 지원하고 싶다면 contact@lean-fro.org로 연락해 주세요.