• 수학 형식화에서 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 형식 의미론임

번역 기반의 경량 검증

프로그램 합성과 파싱

• 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가 더 적합함

댓글과 토론