프로그램 검증에서 Rocq가 Lean보다 나은 이유

 (joomy.korkutblech.com)
1P by GN⁺ | ★ favorite | 댓글과 토론
  • 수학 형식화에서 Lean의 성장세는 뚜렷하지만, 실행 가능한 프로그램 검증에는 네이티브 공귀납과 다양한 추출 경로, 축적된 검증 생태계를 갖춘 Rocq가 더 잘 맞음
  • Rocq는 CoInductive와 CoFixpoint로 공데이터를 선언하고 guardedness를 검사한 뒤 지연 실행 코드로 추출하지만, Lean에서는 라이브러리 인코딩·이터레이터·Thunk·partial def 중 하나를 선택해야 함
  • Lean의 중첩 귀납 타입 검사기는 Rocq가 허용하는 일부 검증 관계를 거부해, JSON 스키마 사례에서는 하나의 Forall₂ 증명을 여러 관계로 분리하고 별도의 귀납 원리를 마련해야 함
  • Rocq는 OCaml·Haskell·Rust·C++·WebAssembly 등의 프로그램 추출 경로와 Iris·CompCert·Interaction Trees 같은 검증 기반을 제공해 실제 게임의 검증된 로직을 실행 코드로 연결할 수 있음
  • AI 에이전트도 문서와 사례가 있으면 Rocq 코드를 작성할 수 있으며, Lean으로 전환하려면 정의뿐 아니라 추출 파이프라인·라이브러리·규제 및 제도적 이력까지 대체해야 하므로 현재 작업에서는 실익이 부족함

프로그램 검증을 기준으로 한 비교

  • 비교 대상은 수학 형식화가 아니라 프로그램 검증이며, 수학 분야에서는 Lean이 실제 성장 동력을 갖고 있음
  • “더 낫다”는 절대적인 우열이 아니라 현재 수행하는 작업에 Rocq가 더 잘 맞는다는 뜻임
  • AI의 수학 분야 성과와 Lean에 대한 관심이 커지면서 Rocq를 계속 사용하는 이유를 자주 질문받았고, 논지는 LangSec 기조연설의 슬라이드에서 출발함

네이티브 공귀납 타입과 cofixpoint

  • Lean의 coinductive가 제공하는 범위

    • Lean FRO의 Wojciech Różowski와 Joachim Breitner가 개발한 공귀납 술어 지원은 Lean 4.25의 coinductive 명령에 포함됨
    • 이 기능은 bisimulation과 공귀납 증명에는 유용하지만, Type의 실행 가능한 cofixpoint나 추출 가능한 프로그램을 제공하지 않음
    • Rocq의 CoInductive와 CoFixpoint는 실행 가능한 공데이터(codata) 를 Type에 직접 제공함
    • Lean에는 이에 대응하는 커널 선언이 없어 일반 함수·구조체 또는 라이브러리 인코딩을 사용해야 함

  • QPFTypes의 선언 제약

    • Alex Keizer의 QPFTypes는 일반 공데이터를 위한 개념 증명 패키지로, codata 명세에서 destructor·corecursor·bisimulation 원리를 생성함
    • Rocq의 CoInductive와 달리 커널 선언이 아닌 라이브러리 인코딩임
    • 예제는 당시 최신 지원 버전인 Lean 4.25.0 고정 도구 체인을 사용함
    • Rocq에서는 평범한 다음 세 선언이 QPFTypes에서 동작하지 않음
      • 매개변수 없는 공데이터는 구현 버그로 실패함
      • tree와 forest 같은 상호 공귀납 선언은 Lean의 mutual block 제약 때문에 지원되지 않음
      • 단계마다 clock 인덱스가 진행하는 istream 같은 인덱스 공귀납 패밀리는 QPF 자체의 한계로 지원되지 않음
    • 프로토콜·단계·크기·상태 머신에도 인덱스 공귀납 패턴이 쓰이지만, QPFTypes의 단순·비상호·비인덱스 범위를 벗어나면 저수준 MvQPF.Cofix.corec와 bisim API를 직접 사용해야 하거나 구현할 수 없음
    • Rocq 역시 guardedness 검사기를 다루기 어렵지만, 위 사례들은 별도 인코딩 없이 선언할 수 있음
    • Paco와 Damien Pous의 coinduction은 공귀납 술어와 관계 증명을 지원하지만 프로그램용 CoFixpoint를 대체하지는 않음

  • 추출되는 프로그램의 차이

    • Rocq의 네이티브 cofixpoint는 실제 지연 OCaml 값으로 추출됨
    • game tree library의 unfold_cotree는 Lazy.t로 감싼 트리와 재귀적인 지연 생성 함수가 됨
    • 결과물은 사람이 직접 작성할 법한 지연 트리 구조에 가까움
    • QPFTypes에서는 생성과 관찰이 MvQPF.Cofix.corec와 MvQPF.Cofix.dest를 거치며, 추출된 프로그램도 일반화된 Cofix 표현을 유지함
    • BadCoinduction.lean에는 Colist·Cotree, 생성된 인터페이스, 매개변수 없는·상호·인덱스 공데이터의 실패 사례와 재현용 QPFTypes 커밋 및 명령이 들어 있음

Lean에서 선택할 수 있는 대안

  • 스트림과 이터레이터

    • mathlib의 Stream'은 Nat → α 함수임
    • 위치 n의 원소를 계산할 수 있고 corecursor·확장성·bisimulation·공귀납 보조정리를 제공함
    • 그러나 꼬리가 다른 스트림인 지연 생성자는 아니며, 임의의 상호·인덱스 공데이터까지 해결하지는 않음
    • 명시적인 상태와 step 함수를 사용하는 상태 머신도 corecursor 역할을 할 수 있음
    • Lean의 Iter는 요청에 따라 한 단계씩 계산하는 순차 인터페이스임
    • 이터레이터는 값 생성 또는 종료를 보장하는 Productive 증명을 가질 수 있으며, Iter.repeat에는 이미 제공됨
    • 사용자 정의 이터레이터에는 step 인터페이스·불변식·필요한 경우 생산성 증명을 직접 공급해야 함
    • Rocq의 CoFixpoint는 재귀 호출의 guardedness를 검사하고, 상태 머신과 시퀀스 사이의 별도 연결 작업 없이 공귀납 값을 반환함

  • Thunk, partial def, unsafe def

    • Lean의 Thunk는 컴파일된 코드에서 처음 강제할 때 계산하고 결과를 캐시하지만 공귀납을 제공하지 않음
    • 논리에서는 Unit → α로 보이므로 전체 정의를 증명에 사용할 수 있지만 캐시는 보이지 않음
    • 재귀를 허용하거나 재귀가 결국 생성자를 생산하는지 검사하지도 않음
    • Rocq의 추출 코드 역시 런타임 지연성을 사용하지만 먼저 guardedness 검사를 통과함
    • partial def는 재귀 본문을 실행할 수 있으나 논리에는 불투명한 상수만 남음
    • 종료성이나 생산성을 검사하지 않아 자연수 생산자와 즉시 무한 재귀하는 생산자를 모두 허용함
    • unsafe def도 실행할 수 있지만 theorem-safe 선언에서는 참조할 수 없음
    • Batteries의 MLList는 비공개 unsafe 지연 구현, 불투명한 공개 인터페이스, partial def로 작성한 fix·iterate 생산자를 조합함
    • 이런 생산자는 관찰된 Rocq cofixpoint처럼 증명에서 펼칠 수 없음
    • partial_fixpoint는 방정식을 유지하지만 생성자와 thunk를 결합한 재귀는 받아들이지 않음
    • QPFTypes는 corecursor와 bisimulation 원리를 제공해 불투명성을 피하지만, 일반화된 Cofix 표현과 선언 제약을 감수해야 함

효과가 있고 종료하지 않는 프로그램

  • Interaction Trees는 효과가 있고 종료하지 않을 수 있는 프로그램을 공귀납 트리로 표현함
    • 같은 트리로 프로그램을 작성·해석·추출하고, 보통 weak bisimulation까지 포함한 방정식을 증명할 수 있음
  • Stream'과 Iter는 시퀀스만 제공하므로 효과에 필요한 분기 continuation을 표현하지 못함
  • Thunk와 partial def로 효과 트리를 실행하면 재귀 생산자가 증명에 불투명해지며, 계산과 증명을 함께 지원하려면 공데이터 라이브러리 인코딩이 필요함
  • MIT PLV의 lean4-itree는 Mathlib의 PFunctor.M final coalgebra로 Interaction Trees를 구현함
  • PolyFun은 handler·재귀 프로시저·실행 추적·strong/weak bisimulation과 monad 및 iteration 법칙 증명을 추가함
    • Lean에서 트리를 계산하고 증명할 수 있지만 여전히 라이브러리로 인코딩된 M-type임
    • 네이티브 공데이터 선언이 없으며 직접적인 지연 프로그램 대신 일반 표현이 유지됨
  • HITrees도 이 제약을 우회하지 않음
    • Lean에 네이티브 공귀납 타입이 없어 ITrees의 공귀납 Delay-monad 접근을 사용하지 않음
    • 트리는 귀납적이며 비종료는 고차 재귀 효과가 됨
    • 재귀 계산은 관찰하고 펼칠 수 있는 무한 트리가 아니라 handler가 효과를 해석할 때 의미를 얻음
    • monadic interpretation으로 실행하고 상태 머신 해석으로 증명할 수 있지만, HITree의 방정식 이론은 일반적인 재귀 펼침 방정식을 제공하지 않음
  • Rocq는 공데이터 선언, guarded producer, 관찰 기반 추론, 직접적인 지연 코드 추출을 하나의 흐름으로 지원함

중첩 귀납 타입과 술어

  • JSON 스키마 검증 사례

    • Lean은 여러 중첩 귀납 정의를 허용하지만 Rocq가 받아들이는 일부 정의를 거부함
    • 이 차이는 A Rose Tree Is Blooming에 사용됐으며, 더 작은 JSON 스키마 사례로 재현할 수 있음
    • JSON과 스키마 자체는 두 언어 모두 문제없이 정의할 수 있음
    • 객체 스키마 검증에서는 필드 이름이 일치하고 각 JSON 값이 대응하는 하위 스키마에 유효한지를 쌍별로 확인해야 함
    • Rocq는 이름 동일성과 재귀 검증을 하나의 Forall2 유도에 저장할 수 있음
    • Rocq 9.0은 재귀 출현 주변의 tuple-pattern lambda를 strict positivity 위반으로 거부하지만, 패턴 대신 projection을 사용하면 컴파일됨
    • Lean 4.32.1은 같은 객체 생성자에서 재귀 출현이 Forall₂와 And를 모두 통과하면 내부 And를 잘못된 중첩 귀납 데이터 타입으로 거부함
    • Forall₂ ParRed, And·Exists를 통한 직접 재귀, Forall₂ (fun sf jf => Valid sf.2 jf.2) 같은 인접 형태는 허용함
    • 관계 매개변수가 생성자 지역 변수 env를 캡처하는 Forall₂ (Eval env)는 Forall₂ 단계에서 실패함

  • 우회 방식과 증명 비용

    • Lean에서는 객체 검증을 두 개의 Forall₂ 유도로 나눌 수 있음
      • 하나는 필드 이름의 동일성을 보존함
      • 다른 하나는 대응 값의 재귀 검증을 보존함
    • 별도 인덱스나 길이 증명 없이 리스트 구조를 유지하고 head 제거도 구조적으로 증명할 수 있지만, 두 유도를 모두 분해해야 함
    • 관계를 분리하면 각 이름 동일성과 재귀 검증이 한 쌍으로 묶인 단일 증명 객체를 잃음
    • 상호 ValidFields 관계로 결합을 복원할 수 있으나 Lean의 induction 전술은 상호 귀납 타입을 지원하지 않고 생성된 recursor도 관계마다 motive를 요구함
    • 사용자 정의 귀납 정리를 만들면 이 설정을 감출 수 있음
    • Rocq는 표준 Forall2 표현을 유지하며, 상호 정의가 필요하면 Scheme으로 결합 원리를 생성할 수 있음
    • Lean도 인덱스 기반 인코딩 없이 같은 명제를 표현할 수 있지만 선언을 재배치하고 더 많은 증명 장치를 만들어야 함
    • 전체 비교 파일은 Rocq 9.0.0용 NestedPain.v와 Lean 4.32.1용 NestedPain.lean에 있으며, Lean의 예상 실패는 #guard_msgs로 컴파일 시 검사됨

  • 중첩 인자에 대한 강한 귀납 원리

    • Term이 list Term을 포함하는 경우처럼 중첩 데이터의 원소별 가정이 필요한 증명에서는 두 시스템 모두 더 강한 recursor가 필요했음
    • Rocq 9.2는 nesting type에 All 술어와 정리를 등록하면 중첩 인자의 귀납 가정을 생성함
    • 표준 라이브러리는 이를 기본 등록하지 않으므로 Term 선언 전에 Scheme All for list. 한 줄을 추가해야 함
    • 생성된 Term_ind와 Term_rect는 app 사례에서 list_all Term P l 가정을 얻고 본문은 list_all_forall을 호출함
    • Scheme All for Forall2.를 추가하면 ParRed_ind도 Forall2 ParRed args args' 전제에 대한 귀납 가정을 제공함
    • 등록하지 않으면 기존의 약한 원리와 함께 [register-all] 경고가 나옴
    • Lean에서는 여전히 강한 recursor를 직접 마련해야 함

프로그램 추출 선택지

  • Lean 표준 도구 체인은 자체 런타임을 통해 컴파일하며, Lean 라이브러리를 만들고 런타임 설계가 맞는 경우 장점이 있음
  • Kim Morrison의 검증된 lean-zip은 순수 Rust miniz_oxide보다 빠르게 압축할 수도 있어 성능이 인상적임
  • 그러나 Lean은 여러 대체 추출 백엔드를 제공하지 않으며, 현재 컴파일 파이프라인에는 종단 간 정확성 증명이 없음
    • Kiran Gopinathan이 발견한 런타임 버그 같은 드문 문제가 발생할 수 있음
    • 생성 코드는 런타임에 특화돼 있고 사람이 읽도록 설계되지 않음
  • Rocq는 신뢰 기반과 가독성 사이에서 서로 다른 절충을 제공하는 여러 경로를 갖춤

검증된 로직을 실행하는 게임

  • Rocq에서 실행 프로그램과 같은 소스 코드의 속성을 기계 검증한 뒤, Crane으로 로직과 이벤트 루프를 C++로 추출하고 rocq-crane-sdl2로 SDL2에 연결함

  • Rocqman

    • Rocqman은 프레임 루프가 사용하는 게임 상태 전이를 증명함
      • 점수는 감소하지 않음
      • 생명과 남은 수집물은 증가하지 않음
      • 종료 상태는 tick의 고정점임
      • 일시정지와 종료 화면 전이를 검사함

  • Rocqsweeper

    • Rocqsweeper는 Minesweeper 규칙과 입력 계층을 증명함
      • 첫 클릭이 안전함
      • 깃발 표시는 지뢰와 인접 데이터를 보존함
      • flood fill은 지뢰를 보존하고 숨겨진 안전 칸을 늘리지 않음
      • 커서는 경계를 벗어나지 않음
      • 마우스 이벤트가 예상한 셀로 해석됨

  • Reversirocq

    • Reversirocq는 Charles C. Norton이 추가한 Reversi 규칙과 같은 game tree library의 공귀납 alpha-beta AI를 사용함
    • 정리는 합법적 수 열거와 게임 결과를 다루며, 검색되는 유한 prefix에서 alpha-beta와 minimax를 연결함

  • 검증 경계

    • 증명 경계는 Rocq 소스에서 끝나며 SDL·Crane·생성된 C++·네이티브 런타임은 포함하지 않음
    • 경계 안에서는 실행 프로그램과 분리된 모델이 아니라 실제 실행 로직의 속성을 증명함

Rocq 프로그램 검증 생태계

  • 프로그램 표현 추상화

    • Interaction Trees: 외부 이벤트의 공귀납 트리로 효과가 있고 종료하지 않을 수 있는 프로그램을 표현하며, 비순수 코드에 표시적 의미론과 방정식 추론을 제공함
    • Choice Trees: 내부 비결정적 선택을 추가해 동시성 등 비결정적 시스템을 모델링함

  • 프로그램 검증 프레임워크

    • Iris: 상태와 동시성 프로그램을 위한 고차 concurrent separation logic 프레임워크임
    • Iris-Lean도 빠르게 발전하며 많은 기능을 지원하지만 Rocq Iris만큼 폭넓게 사용되지는 않았음
    • CFML: OCaml 소스를 Rocq로 가져와 characteristic formula를 생성하고 고차 separation logic 명세용 전술을 제공함
    • Perennial: 동시성·충돌 안전 저장소·분산 시스템을 검증하는 Iris 기반 프레임워크이며, Goose로 Go 부분집합의 실행 프로그램과 연결함
    • VST: CompCert 의미론을 기반으로 C 프로그램의 함수적 정확성을 증명하는 Verified Software Toolchain임
    • BRiCk: 실제 C++ 프로그램을 위한 프로그램 논리와 도구 체인임

  • Rocq 백엔드 또는 구성 요소를 갖춘 도구

    • Frama-C: C 분석·연역 검증 플랫폼으로 증명 의무를 Rocq에 넘길 수 있음
    • Why3: 자체 언어의 목표를 여러 증명기로 보내고 Rocq용 대화형 증명 의무를 내보낼 수 있음
    • Cerberus: 실용적인 대규모 C 부분집합의 실행 가능 형식 의미론이며 CHERI C 메모리 모델에 Rocq 구현이 있음

  • 실제 언어의 의미론과 검증된 컴파일러

    • CompCert: 형식 검증된 최적화 C 컴파일러임
    • Vellvm: LLVM IR의 Rocq 명세와 추상 의미론, 이를 정제하는 것으로 증명된 실행 인터프리터를 제공함
    • Vélus: Lustre에서 CompCert의 Clight로 가는 검증된 컴파일러임
    • WasmCert: WebAssembly의 기계화된 형식 의미론임
    • JSCert: ECMAScript 5 명세를 추적하는 JavaScript 형식 의미론임

  • 번역 기반의 경량 검증

    • hs-to-coq: Haskell 소스를 Rocq로 번역함
    • rocq-of-ocaml: OCaml 소스를 Rocq로 번역함
    • rocq-of-python: Python 소스를 Rocq로 번역함
    • rocq-of-rust: Rust 소스를 Rocq로 번역함
    • Aeneas: borrow check를 통과한 Rust를 검증용 순수 함수 모델로 바꾸며 Lean도 대상으로 지원함

  • 프로그램 합성과 파싱

    • Fiat Crypto: 브라우저와 TLS 라이브러리에 쓰일 수 있는 고성능 암호 산술을 correct-by-construction 방식으로 유도함
    • Rupicola: 저수준 함수형 Gallina 프로그램을 명령형 Bedrock2 프로그램으로 바꾸는 관계형 컴파일 도구임
    • Narcissus: 바이너리 형식의 correct-by-construction encoder와 decoder를 유도함
    • Verbatim: 정규식 기반의 검증된 lexer임
    • CoStar: ALL(*) 알고리듬 기반의 검증된 parser임

  • 유지보수 상태

    • 일부 프로젝트는 활발히 유지보수되지 않지만, 에이전트에 맡겨 다시 빌드하고 실행할 수 있었음
    • 필요한 요소 하나를 Lean으로 단기간에 포팅할 수 있더라도, 전체 생태계가 축적한 기능과 사용 이력까지 자동으로 옮겨지지는 않음

규제와 인증 이력

  • 규제 수용에 대한 직접적인 인증 경험은 없으며, 특히 유럽의 작업자에게 더 중요할 수 있는 요소임
  • 프랑스 ANSSI는 Common Criteria 평가에서 Rocq를 사용하기 위한 기준을 공개함
  • CompCert는 AbsInt가 Airbus의 지침을 받아 수행한 작업을 통해 2026년 ATR 42/72 항공기의 MFC_NG 컴퓨터용으로 성공적으로 qualification됐다고 밝힘
  • Lean 포트가 같은 환경에서 어떤 요건을 충족해야 하는지는 알 수 없으며, 깔끔하게 포팅해도 기존의 인증 이력을 자동으로 상속하지 않음

AI 에이전트와 전환 비용

  • AI 에이전트가 Lean만 잘 작성한다는 전제와 달리 Rocq 코드도 충분히 작성할 수 있음
  • Rocq는 1980년대 후반부터 존재해 코드와 문서가 많이 축적돼 있음
  • 현재 모델은 문서와 예제를 제공하면 익숙하지 않은 언어에도 잘 적응하므로, 인기 언어만 안다는 이유는 proof assistant를 바꿀 장기적인 근거가 되지 못함
  • Lean에서도 mvcgen과 Velvet 같은 진지한 프로그램 검증 작업이 진행 중임
  • 현재 작업을 Lean으로 옮기려면 정의를 재구성하고 추출 파이프라인·라이브러리·제도적 이력을 교체해야 하므로, 지금은 Rocq가 더 적합함

함께 보면 좋은 글 β