[Lobsters 요약] Rust 코드의 기계 검증 가능한 증명을 위한 AI 기반 파이프라인 경험 보고
3
설명
Runtime Verification 팀은 프로덕션 Rust 암호화 코드를 Lean 4의 기계 검증 가능한 증명으로 변환하는 파이프라인을 개발했습니다.
이 파이프라인은 Rust 코드 추출 도구, 형식 암호화 사양 라이브러리, 그리고 AI 기반 증명 보조 도구를 통합합니다.
2026년 5월에 발표된 이 보고서는 Plonky3 및 RISC Zero 프로젝트의 암호화 기본 요소에 대한 파이프라인 적용 경험을 공유합니다.
### 배경 설명
소프트웨어의 신뢰성은 특히 암호화 코드에서 매우 중요합니다. 제로 지식 가상 머신(zkVM)과 같은 시스템에서 작은 버그 하나가 전체 증명의 무결성을 손상시킬 수 있습니다. 코드 검토, 퍼징, 속성 기반 테스트는 버그를 탐지하는 데 유용하지만, 모든 가능한 입력과 의미론적 오류를 포괄하는 데는 한계가 있습니다. 형식 검증은 모든 입력에 대해 기계 검증 가능한 증명을 제공하지만, 사양 설계의 복잡성과 높은 비용이 주요 장애물이었습니다. 과거 seL4 및 CompCert과 같은 시스템의 완전한 형식 검증은 수년간의 노력을 필요로 했습니다. 최근에는 Rust의 안전한 부분 집합을 Lean 4와 같은 증명 보조 도구로 변환하는 Aeneas 및 Hax와 같은 도구의 발전, 그리고 Aristotle 및 Aleph와 같은 AI 기반 증명 보조 도구의 등장으로 형식 검증의 진입 장벽이 낮아지고 있습니다. 또한, Mathlib4 및 ArkLib, CompPoly와 같은 특수화된 라이브러리는 복잡한 수학적 사양을 형식화하는 데 필요한 기반을 제공합니다. 이러한 세 가지 주요 발전의 조합은 산업 규모의 형식 검증 비용을 크게 절감할 수 있는 잠재력을 가지고 있습니다.
### 파이프라인 아키텍처
이 파이프라인은 네 단계로 구성됩니다. 첫 번째 단계는 Charon 및 Aeneas 또는 Hax와 같은 도구를 사용하여 Rust 코드를 Lean 4로 변환하는 것입니다. 이 과정에서 Rust의 루프는 재귀 함수로, 산술 연산은 오류 경로를 명시적으로 노출하는 모나드로 표현됩니다. 두 번째 단계는 ArkLib 또는 CompPoly와 같은 라이브러리에서 가져오거나 수동으로 작성된 사양을 정의하는 것입니다. 세 번째 단계에서는 수동 또는 AI 보조를 통해 증명을 생성합니다. Aeneas의 경우 progress 및 scalar_tac과 같은 전용 전술이 사용되며, 일반적인 Lean 4 전술(omega, nlinarith, ring, simp, decide)도 활용됩니다. Aristotle 및 Aleph와 같은 AI 증명 보조 도구는 개별 보조 정리나 전체 정리를 증명하는 데 사용될 수 있습니다. 마지막 네 번째 단계는 Lean 커널이 모든 증명을 재확인하여 신뢰 경계를 설정하는 것입니다. AI가 생성한 증명이라도 Lean 커널에서 타입 검사를 통과해야만 유효한 것으로 간주됩니다.
### 실행 예제: compute_log_arity_for_round
Plonky3의 FRI(Fast Reed-Solomon Interactive Oracle Proof of Proximity) 프로토콜에서 사용되는 `compute_log_arity_for_round` 함수를 실행 예제로 사용했습니다. 이 함수는 FRI 라운드에서 폴딩의 공격성을 결정하며, 최대 허용 아리티, 최종 높이까지의 거리, 다음 입력 커밋먼트까지의 거리를 고려합니다. Hax 도구를 사용하여 이 Rust 함수를 Lean 4로 추출했으며, 두 개의 검증된 빼기 연산과 옵션 매치, 그리고 두 개의 "min" 선택을 포함하는 구조를 가집니다. 이 함수에 대해 두 가지 정리를 공식화했습니다: 결과가 최대 허용 아리티를 초과하지 않아야 한다는 정리(`arity_respects_max_bound`)와 최종 높이까지의 거리를 초과하지 않아야 한다는 정리(`arity_respects_target_distance`). 이 두 정리는 원래 "sorry" 상태였으나, 2026년 2월에 Aleph AI 증명 보조 도구에 의해 자동으로 증명되었습니다. 특히 `arity_respects_max_bound` 증명은 두 개의 재사용 가능한 헬퍼 보조 정리를 식별하고 증명한 후 이를 조합하는 방식으로 진행되었습니다. `arity_respects_target_distance` 증명은 더 복잡했으며, 검증된 빼기 연산을 포함하여 `h_gt` 가정을 사용하여 일반적인 자연수 빼기와 동일하게 작동함을 입증해야 했습니다.
### AI 기반 증명 자동화: 경험적 관찰
Aristotle 및 Aleph와 같은 AI 증명 보조 도구를 사용한 경험을 바탕으로, 특정 유형의 증명 요구 사항을 AI가 효과적으로 처리할 수 있음을 관찰했습니다. AI가 잘 처리한 범주에는 제어 흐름 및 구조적 보조 정리(모나드 역전, 조건부 경계, 열거형 분기), 온화한 부수 조건이 있는 선형 산술, 그리고 추출된 코드 주변의 단순한 보일러플레이트(모나드 바인드 펼치기, 조건부 분배, 검증된 산술 가드 정규화)가 포함됩니다. 반면, 상당한 수동 증명이나 완전한 수동 구성이 필요한 범주도 있었습니다. 여기에는 Mathlib4 보조 정리를 신중하게 선택해야 하는 도메인별 대수적 항등식, Aeneas 추출 재귀 함수에 대한 루프 불변량 발견, 그리고 공리 선택 자체가 설계 결정인 외부 인터페이스 공리화가 포함됩니다. 현재 AI 증명 보조 도구는 이러한 작업에서 생산성 향상 도구 역할을 하지만, 사양 설계, 불변량 발견, 수학적 추상화 선택과 같은 근본적인 검증 노력의 형태를 바꾸지는 않았습니다.
### 엔지니어링 과제 및 해결책
이 파이프라인을 개발하고 적용하는 과정에서 몇 가지 엔지니어링 과제에 직면했습니다. 첫째, Lean 4 버전 충돌이 발생했습니다. Aeneas, Hax, ArkLib, CompPoly, Mathlib4가 독립적인 Lean 4 릴리스 트랙에서 발전함에 따라, 각 도구가 다른 Lean 도구 체인에 고정되어 단일 프로젝트에서 여러 소스의 도구를 가져올 수 없는 문제가 있었습니다. 이 문제는 관련 저장소에 보고되었고, 유지 관리 팀 간의 조정을 통해 라이브러리가 공통 Lean 4 버전(Hax 기반 작업의 경우 4.26.0, Aeneas 기반 작업의 경우 4.28.0)으로 정렬되면서 해결되었습니다. 둘째, Aeneas 및 Hax의 추출 제한이 있었습니다. 예를 들어, BitVec.toNat_pow와 같은 이름 충돌은 Aeneas의 비트 벡터 보조 정리와 Batteries/Mathlib4 간의 충돌을 야기하여 AeneasVerif/aeneas#832에서 패치되었습니다. 또한, 모듈식 산술 내의 더 넓은 정수 유형으로의 캐스트는 복잡한 증명 엔지니어링을 요구했으며, 일반 함수는 구체적인 단형(monomorphised) 유형이 필요했습니다. 이러한 문제를 해결하기 위해 세 가지 주요 전략을 사용했습니다. 첫째, 가능한 경우 상위 저장소를 수정했습니다. 둘째, Aeneas가 처리할 수 없는 패턴(병렬 반복자, 깊은 제네릭, 외부 크레이트 호출)을 사용하는 경우, 생산 코드와 의미론적으로 동등하지만 깨끗하게 추출되는 독립적인 비제네릭 Rust 크레이트로 수학적 핵심을 재작성했습니다. 셋째, 안전하지 않은 코드의 경우, 안전한 코어는 Aeneas 또는 Hax로 증명하고, 안전하지 않은 부분에는 cargo-anneal과 같은 보완 도구를 사용하는 계층화된 접근 방식을 사용했습니다.
### 가치와 인사이트
이 연구는 프로덕션 Rust 코드에서 Lean 4의 기계 검증 가능한 증명으로 이어지는 완전한 신경-기호 파이프라인을 제시합니다. Ethereum Foundation의 zkEVM Verification Project 하에서 Plonky3 및 RISC Zero의 암호화 기본 요소에 이 파이프라인을 성공적으로 적용했습니다. 특히, AI 증명 보조 도구(Aristotle 및 Aleph)가 특정 유형의 증명 요구 사항을 효과적으로 처리할 수 있음을 경험적으로 보여주었으며, 이는 형식 검증의 생산성을 크게 향상시킬 수 있습니다. 또한, Lean 4 도구 체인 버전 충돌 및 Rust 코드 추출의 한계와 같은 엔지니어링 과제와 이를 해결하기 위한 실용적인 전략을 문서화했습니다. 이 작업은 형식 검증의 채택 장벽을 낮추고 이 파이프라인에서 AI의 보다 효과적인 사용을 촉진하는 데 기여할 것으로 기대됩니다. 결과적으로, 커널 검증 증명과 재현 가능한 아티팩트를 갖춘 Rust의 형식 검증을 위한 작동하는 파이프라인을 제공합니다.
### 기술·메타
- 언어: Rust, Lean 4
- 도구: Charon, Aeneas, Hax, Aristotle (Harmonic AI), Aleph (Logical Intelligence), Mathlib4, ArkLib, CompPoly, Plonky3, RISC Zero
- 라이선스: CC BY 4.0
- arXiv ID: 2605.30106v2
### 향후 전망
이 연구는 향후 두 가지 주요 방향으로 발전할 가능성이 있습니다. 첫째, Beneficial AI Foundation의 Signal Shot 프로그램에 참여하여 Signal 메시징 스택의 종단 간 기계 검증 가능한 검증을 Lean 4에서 수행할 계획입니다. Signal 코드베이스는 이 파이프라인의 자연스러운 다음 대상이 될 것입니다. 둘째, AI 증명 보조 도구를 검증 CI/CD 루프에 더욱 긴밀하게 통합할 예정입니다. 현재는 풀 리퀘스트별로 호출되지만, 향후에는 새로 도입된 "sorry" 상태에 대해 자동으로 실행하고, 인간 검토자가 코드를 보기 전에 어떤 요구 사항이 이미 해결되었는지 확인할 수 있도록 할 것입니다. 이러한 발전은 AI 증명 보조 도구의 성숙도에 따라 검증 노력의 근본적인 형태를 변화시킬 것으로 예상됩니다.
📝 원문 및 참고
- Source: Lobsters
- 토론(Lobsters): [lobste.rs](https://lobste.rs/s/g2bzt2/rust_lean_verification_pipeline_with_ai)
- 원문: [링크 열기](https://arxiv.org/html/2605.30106)
---
출처: Lobsters · [원문 링크](https://arxiv.org/html/2605.30106)
신고 · 불법·유해·아동 안전(CSAE) 관련 콘텐츠
댓글 0
아직 댓글이 없습니다. 첫 댓글을 남겨 보세요.