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

> Clean Markdown view of GeekNews topic #31955. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=31955](https://news.hada.io/topic?id=31955)
- GeekNews Markdown: [https://news.hada.io/topic/31955.md](https://news.hada.io/topic/31955.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2026-07-30T00:05:17+09:00
- Updated: 2026-07-30T00:05:17+09:00
- Original source: [joomy.korkutblech.com](https://joomy.korkutblech.com/posts/2026-07-28-why-rocq-is-better.html)
- Points: 1
- Comments: 0

## Topic Body

- 수학 형식화에서 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가 개발한 [공귀납 술어 지원](https://www.youtube.com/watch?v=vEt07N_v-Yo)은 [Lean 4.25](https://lean-lang.org/doc/reference/latest/releases/v4.25.0/)의 `coinductive` 명령에 포함됨
  - 이 기능은 bisimulation과 공귀납 증명에는 유용하지만, `Type`의 실행 가능한 cofixpoint나 추출 가능한 프로그램을 제공하지 않음
  - Rocq의 `CoInductive`와 `CoFixpoint`는 실행 가능한 **공데이터(codata)** 를 `Type`에 직접 제공함
  - Lean에는 이에 대응하는 커널 선언이 없어 일반 함수·구조체 또는 라이브러리 인코딩을 사용해야 함
- ## QPFTypes의 선언 제약
  - Alex Keizer의 [QPFTypes](https://github.com/alexkeizer/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](https://github.com/snu-sf/paco)와 Damien Pous의 [coinduction](https://github.com/damien-pous/coinduction)은 공귀납 술어와 관계 증명을 지원하지만 프로그램용 `CoFixpoint`를 대체하지는 않음
- ## 추출되는 프로그램의 차이
  - Rocq의 네이티브 cofixpoint는 실제 **지연 OCaml 값**으로 추출됨
  - [game tree library](https://github.com/bloomberg/game-trees)의 `unfold_cotree`는 `Lazy.t`로 감싼 트리와 재귀적인 지연 생성 함수가 됨
  - 결과물은 사람이 직접 작성할 법한 지연 트리 구조에 가까움
  - QPFTypes에서는 생성과 관찰이 `MvQPF.Cofix.corec`와 `MvQPF.Cofix.dest`를 거치며, 추출된 프로그램도 일반화된 `Cofix` 표현을 유지함
  - [BadCoinduction.lean](https://joomy.korkutblech.com/assets/why-rocq-is-better/BadCoinduction.lean)에는 `Colist`·`Cotree`, 생성된 인터페이스, 매개변수 없는·상호·인덱스 공데이터의 실패 사례와 재현용 QPFTypes 커밋 및 명령이 들어 있음

### Lean에서 선택할 수 있는 대안
- ## 스트림과 이터레이터
  - mathlib의 [`Stream'`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Stream/Defs.html)은 `Nat → α` 함수임
  - 위치 `n`의 원소를 계산할 수 있고 corecursor·확장성·bisimulation·공귀납 보조정리를 제공함
  - 그러나 꼬리가 다른 스트림인 지연 생성자는 아니며, 임의의 상호·인덱스 공데이터까지 해결하지는 않음
  - 명시적인 상태와 step 함수를 사용하는 상태 머신도 corecursor 역할을 할 수 있음
  - Lean의 [`Iter`](https://lean-lang.org/doc/reference/latest/Iterators/)는 요청에 따라 한 단계씩 계산하는 순차 인터페이스임
  - 이터레이터는 값 생성 또는 종료를 보장하는 [`Productive`](https://lean-lang.org/doc/reference/latest/Iterators/Iterator-Definitions/#finite-and-productive-iterators) 증명을 가질 수 있으며, `Iter.repeat`에는 이미 제공됨
  - 사용자 정의 이터레이터에는 step 인터페이스·불변식·필요한 경우 생산성 증명을 직접 공급해야 함
  - Rocq의 `CoFixpoint`는 재귀 호출의 guardedness를 검사하고, 상태 머신과 시퀀스 사이의 별도 연결 작업 없이 공귀납 값을 반환함
- ## `Thunk`, `partial def`, `unsafe def`
  - Lean의 [`Thunk`](https://lean-lang.org/doc/reference/latest/Basic-Types/Lazy-Computations/)는 컴파일된 코드에서 처음 강제할 때 계산하고 결과를 캐시하지만 **공귀납을 제공하지 않음**
  - 논리에서는 `Unit → α`로 보이므로 전체 정의를 증명에 사용할 수 있지만 캐시는 보이지 않음
  - 재귀를 허용하거나 재귀가 결국 생성자를 생산하는지 검사하지도 않음
  - Rocq의 추출 코드 역시 런타임 지연성을 사용하지만 먼저 guardedness 검사를 통과함
  - [`partial def`](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#partial-functions)는 재귀 본문을 실행할 수 있으나 논리에는 불투명한 상수만 남음
  - 종료성이나 생산성을 검사하지 않아 자연수 생산자와 즉시 무한 재귀하는 생산자를 모두 허용함
  - `unsafe def`도 실행할 수 있지만 theorem-safe 선언에서는 참조할 수 없음
  - Batteries의 [`MLList`](https://github.com/leanprover-community/batteries/blob/main/Batteries/Data/MLList/Basic.lean)는 비공개 unsafe 지연 구현, 불투명한 공개 인터페이스, `partial def`로 작성한 `fix`·`iterate` 생산자를 조합함
  - 이런 생산자는 관찰된 Rocq cofixpoint처럼 증명에서 펼칠 수 없음
  - [`partial_fixpoint`](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/#partial-fixpoints)는 방정식을 유지하지만 생성자와 thunk를 결합한 재귀는 받아들이지 않음
  - QPFTypes는 corecursor와 bisimulation 원리를 제공해 불투명성을 피하지만, 일반화된 `Cofix` 표현과 선언 제약을 감수해야 함

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

### 중첩 귀납 타입과 술어
- ## JSON 스키마 검증 사례
  - Lean은 여러 중첩 귀납 정의를 허용하지만 Rocq가 받아들이는 일부 정의를 거부함
  - 이 차이는 [*A Rose Tree Is Blooming*](https://joomy.korkutblech.com/papers/game-trees-cpp26.pdf)에 사용됐으며, 더 작은 JSON 스키마 사례로 재현할 수 있음
  - JSON과 스키마 자체는 두 언어 모두 문제없이 정의할 수 있음
  - 객체 스키마 검증에서는 필드 이름이 일치하고 각 JSON 값이 대응하는 하위 스키마에 유효한지를 쌍별로 확인해야 함
  - Rocq는 이름 동일성과 재귀 검증을 하나의 [`Forall2`](https://rocq-prover.org/doc/V9.0.0/stdlib/Stdlib.Lists.List.html#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](https://joomy.korkutblech.com/assets/why-rocq-is-better/NestedPain.v)와 Lean 4.32.1용 [NestedPain.lean](https://joomy.korkutblech.com/assets/why-rocq-is-better/NestedPain.lean)에 있으며, Lean의 예상 실패는 `#guard_msgs`로 컴파일 시 검사됨
- ## 중첩 인자에 대한 강한 귀납 원리
  - `Term`이 `list Term`을 포함하는 경우처럼 중첩 데이터의 원소별 가정이 필요한 증명에서는 두 시스템 모두 더 강한 recursor가 필요했음
  - [Rocq 9.2](https://rocq-prover.org/doc/V9.2.0/refman/changes.html#nested)는 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`](https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-than-rust/)은 순수 Rust `miniz_oxide`보다 빠르게 압축할 수도 있어 성능이 인상적임
- 그러나 Lean은 여러 대체 추출 백엔드를 제공하지 않으며, 현재 컴파일 파이프라인에는 **종단 간 정확성 증명**이 없음
  - Kiran Gopinathan이 발견한 [런타임 버그](https://kirancodes.me/posts/log-who-watches-the-watchers.html) 같은 드문 문제가 발생할 수 있음
  - 생성 코드는 런타임에 특화돼 있고 사람이 읽도록 설계되지 않음
- Rocq는 신뢰 기반과 가독성 사이에서 서로 다른 절충을 제공하는 여러 경로를 갖춤
  - [OCaml·Haskell·Scheme](https://rocq-prover.org/doc/master/refman/addendum/extraction.html)
  - [Malfunction으로 가는 검증된 추출 파이프라인](https://github.com/MetaRocq/rocq-verified-extraction)
  - [Rust](https://github.com/AU-COBRA/coq-rust-extraction)
  - [Elm](https://github.com/AU-COBRA/coq-elm-extraction)
  - [CertiRocq](https://github.com/CertiRocq/certirocq)를 통한 Clight와 WebAssembly이며 일부는 개발 중임
  - 가독성 높은 생성 코드를 목표로 하는 [Crane](https://github.com/bloomberg/crane)의 C++ 추출

### 검증된 로직을 실행하는 게임
- Rocq에서 실행 프로그램과 같은 소스 코드의 속성을 기계 검증한 뒤, Crane으로 로직과 이벤트 루프를 C++로 추출하고 [rocq-crane-sdl2](https://github.com/joom/rocq-crane-sdl2)로 SDL2에 연결함
- ## Rocqman
  - [Rocqman](https://joomy.korkutblech.com/rocqman/)은 프레임 루프가 사용하는 게임 상태 전이를 증명함
    - 점수는 감소하지 않음
    - 생명과 남은 수집물은 증가하지 않음
    - 종료 상태는 `tick`의 고정점임
    - 일시정지와 종료 화면 전이를 검사함
- ## Rocqsweeper
  - [Rocqsweeper](https://joomy.korkutblech.com/rocqsweeper/)는 Minesweeper 규칙과 입력 계층을 증명함
    - 첫 클릭이 안전함
    - 깃발 표시는 지뢰와 인접 데이터를 보존함
    - flood fill은 지뢰를 보존하고 숨겨진 안전 칸을 늘리지 않음
    - 커서는 경계를 벗어나지 않음
    - 마우스 이벤트가 예상한 셀로 해석됨
- ## Reversirocq
  - [Reversirocq](https://joomy.korkutblech.com/reversirocq/)는 Charles C. Norton이 추가한 [Reversi 규칙](https://github.com/bloomberg/game-trees/pull/7)과 같은 game tree library의 공귀납 alpha-beta AI를 사용함
  - 정리는 합법적 수 열거와 게임 결과를 다루며, 검색되는 유한 prefix에서 alpha-beta와 minimax를 연결함
- ## 검증 경계
  - 증명 경계는 **Rocq 소스**에서 끝나며 SDL·Crane·생성된 C++·네이티브 런타임은 포함하지 않음
  - 경계 안에서는 실행 프로그램과 분리된 모델이 아니라 실제 실행 로직의 속성을 증명함

### Rocq 프로그램 검증 생태계
- ## 프로그램 표현 추상화
  - [Interaction Trees](https://github.com/DeepSpec/InteractionTrees): 외부 이벤트의 공귀납 트리로 효과가 있고 종료하지 않을 수 있는 프로그램을 표현하며, 비순수 코드에 표시적 의미론과 방정식 추론을 제공함
  - [Choice Trees](https://github.com/vellvm/ctrees): 내부 비결정적 선택을 추가해 동시성 등 비결정적 시스템을 모델링함
- ## 프로그램 검증 프레임워크
  - [Iris](https://iris-project.org/): 상태와 동시성 프로그램을 위한 고차 concurrent separation logic 프레임워크임
  - [Iris-Lean](https://github.com/leanprover-community/iris-lean)도 빠르게 발전하며 많은 기능을 지원하지만 Rocq Iris만큼 폭넓게 사용되지는 않았음
  - [CFML](https://github.com/charguer/cfml): OCaml 소스를 Rocq로 가져와 characteristic formula를 생성하고 고차 separation logic 명세용 전술을 제공함
  - [Perennial](https://github.com/mit-pdos/perennial): 동시성·충돌 안전 저장소·분산 시스템을 검증하는 Iris 기반 프레임워크이며, [Goose](https://github.com/goose-lang/goose)로 Go 부분집합의 실행 프로그램과 연결함
  - [VST](https://vst.cs.princeton.edu/): CompCert 의미론을 기반으로 C 프로그램의 함수적 정확성을 증명하는 Verified Software Toolchain임
  - [BRiCk](https://github.com/bedrocksystems/BRiCk): 실제 C++ 프로그램을 위한 프로그램 논리와 도구 체인임
- ## Rocq 백엔드 또는 구성 요소를 갖춘 도구
  - [Frama-C](https://frama-c.com/): C 분석·연역 검증 플랫폼으로 증명 의무를 Rocq에 넘길 수 있음
  - [Why3](https://www.why3.org/): 자체 언어의 목표를 여러 증명기로 보내고 Rocq용 대화형 증명 의무를 내보낼 수 있음
  - [Cerberus](https://www.cl.cam.ac.uk/~pes20/cerberus/): 실용적인 대규모 C 부분집합의 실행 가능 형식 의미론이며 CHERI C 메모리 모델에 Rocq 구현이 있음
- ## 실제 언어의 의미론과 검증된 컴파일러
  - [CompCert](https://compcert.org/): 형식 검증된 최적화 C 컴파일러임
  - [Vellvm](https://vellvm.github.io/vellvm/): LLVM IR의 Rocq 명세와 추상 의미론, 이를 정제하는 것으로 증명된 실행 인터프리터를 제공함
  - [Vélus](https://velus.inria.fr/): Lustre에서 CompCert의 Clight로 가는 검증된 컴파일러임
  - [WasmCert](https://github.com/WasmCert/WasmCert-Coq): WebAssembly의 기계화된 형식 의미론임
  - [JSCert](https://github.com/jscert/jscert): ECMAScript 5 명세를 추적하는 JavaScript 형식 의미론임
- ## 번역 기반의 경량 검증
  - [hs-to-coq](https://github.com/plclub/hs-to-coq): Haskell 소스를 Rocq로 번역함
  - [rocq-of-ocaml](https://github.com/formal-land/rocq-of-ocaml): OCaml 소스를 Rocq로 번역함
  - [rocq-of-python](https://github.com/formal-land/rocq-of-python): Python 소스를 Rocq로 번역함
  - [rocq-of-rust](https://github.com/formal-land/rocq-of-rust): Rust 소스를 Rocq로 번역함
  - [Aeneas](https://github.com/AeneasVerif/aeneas): borrow check를 통과한 Rust를 검증용 순수 함수 모델로 바꾸며 Lean도 대상으로 지원함
- ## 프로그램 합성과 파싱
  - [Fiat Crypto](https://github.com/mit-plv/fiat-crypto): 브라우저와 TLS 라이브러리에 쓰일 수 있는 고성능 암호 산술을 correct-by-construction 방식으로 유도함
  - [Rupicola](https://github.com/mit-plv/rupicola): 저수준 함수형 Gallina 프로그램을 명령형 [Bedrock2](https://github.com/mit-plv/bedrock2) 프로그램으로 바꾸는 관계형 컴파일 도구임
  - [Narcissus](https://github.com/mit-plv/fiat): 바이너리 형식의 correct-by-construction encoder와 decoder를 유도함
  - [Verbatim](https://github.com/egolf-cs/Verbatim): 정규식 기반의 검증된 lexer임
  - [CoStar](https://github.com/slasser/CoStar): ALL(\*) 알고리듬 기반의 검증된 parser임
- ## 유지보수 상태
  - 일부 프로젝트는 활발히 유지보수되지 않지만, 에이전트에 맡겨 다시 빌드하고 실행할 수 있었음
  - 필요한 요소 하나를 Lean으로 단기간에 포팅할 수 있더라도, 전체 생태계가 축적한 기능과 사용 이력까지 자동으로 옮겨지지는 않음

### 규제와 인증 이력
- 규제 수용에 대한 직접적인 인증 경험은 없으며, 특히 유럽의 작업자에게 더 중요할 수 있는 요소임
- 프랑스 ANSSI는 Common Criteria 평가에서 Rocq를 사용하기 위한 [기준](https://cyber.gouv.fr/sites/default/files/document/anssi-requirements-on-the-use-of-coq-in-the-context-of-common-criteria-evaluations-v1.1-en.pdf)을 공개함
- CompCert는 AbsInt가 Airbus의 지침을 받아 수행한 작업을 통해 2026년 ATR 42/72 항공기의 `MFC_NG` 컴퓨터용으로 [성공적으로 qualification](https://compcert.org/)됐다고 밝힘
- Lean 포트가 같은 환경에서 어떤 요건을 충족해야 하는지는 알 수 없으며, 깔끔하게 포팅해도 기존의 **인증 이력**을 자동으로 상속하지 않음

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

## Comments



_No public comments on this page._