Especially now, with AI’s well-publicized success in mathematics, I get asked why I still use Rocq instead of giving in to the hype and switching to Lean. Most of this post started life as a provocatively titled slide in a recent LangSec keynote: “Why Rocq is better than Lean for program verification.”

I am not trying to start a flame war here. If you are a more mature person than I am, feel free to mentally replace “better” with “a better fit for my work today” everywhere below. One more caveat before I start: this post is about program verification, not formalizing mathematics, where I will happily admit Lean has real momentum.

Language-level issues

Coinductive types and cofixpoints

Wojciech Różowski and Joachim Breitner of Lean FRO developed support for coinductive predicates in Lean. Their feature made it into Lean 4.25 as the coinductive command (implementation). It is useful for bisimulations and other coinductive proofs, but it does not provide executable cofixpoints or programs that can be extracted.

I also want codata in Type that I can actually run. Rocq gives me that directly with CoInductive and CoFixpoint. Lean has no corresponding declarations in Type; its alternatives use ordinary functions and structures or library encodings.

The closest Lean experiment I found to a Rocq-style codata declaration is Alex Keizer’s QPFTypes, a proof-of-concept package for generic codata. Its codata command turns a specification into a library encoding and generates destructor, corecursor, and bisimulation principles. Unlike Rocq’s CoInductive, it is not a kernel declaration. The examples use QPFTypes’ pinned Lean 4.25.0 toolchain (latest supported at the time of the post).

Declaring codata

I do not mean this as a dunk on QPFTypes: it says “proof of concept” right there in the readme. But the rough edges show up quickly in examples that are completely ordinary in Rocq. For instance, Rocq accepts this parameterless coinductive type directly:

CoInductive co_unit : Type :=
| co_unit_loop : co_unit.
codata CoUnit where
  | loop : CoUnit

/--
error: Due to a bug, codatatype without any parameters don't quite
work yet. Please try adding parameters to your type
-/

This one can be written off as an implementation bug but the next two are structural. Mutually coinductive declarations are routine in Rocq but not supported by QPFTypes:

CoInductive tree (a : Type) : Type :=
| node : a -> forest a -> tree a
with forest (a : Type) : Type :=
| fnil : forest a
| fcons : tree a -> forest a -> forest a.
mutual
  codata Tree α where
    | node : α → Forest α → Tree α

  codata Forest α where
    | fnil : Forest α
    | fcons : Tree α → Forest α → Forest α
end

/--
error: invalid mutual block: either all elements of the block must be
inductive/structure declarations, or they must all be definitions/
theorems/abbrevs
-/

Indexed coinductive families are also part of Rocq’s ordinary coinductive fragment but outside the QPF encoding. In this example, the index is a clock that advances at each step; the same pattern occurs with protocols, phases, sizes, and state machines:

CoInductive istream (a : Type) : nat -> Type :=
| icons : forall n, a -> istream a (S n) -> istream a n.
codata IStream α : Nat → Type where
  | icons : α → IStream α (n + 1) → IStream α n

/--
error: Unexpected type; type will be automatically inferred. Note that
inductive families are not supported due to inherent limitations of QPFs
-/

Under the hood, QPFTypes generates Cofix machinery. The codata command hides most of it for simple, non-mutual, non-indexed cases, but once I leave that fragment I am either calling the low-level MvQPF.Cofix.corec and bisim API myself or I am out of luck. In Rocq, the examples above are just declarations.

Rocq’s direct support is not painless; anyone who has argued with its guardedness checker knows that. On the proof side, Rocq users also have mature tools such as Paco and Damien Pous’s coinduction library. They help with coinductive predicates and relations, but they do not replace CoFixpoint for programs.

Extracting cofixpoints

A native Rocq cofixpoint extracts to an actual lazy OCaml value. For example, in the game tree library I worked on, the Rocq unfold_cotree function extracts to:

type 'a cotree = 'a __cotree Lazy.t
and 'a __cotree =
| Conode of 'a * 'a cotree colist

(* other definitions ... *)

(** val unfold_cotree : ('a1 -> 'a1 colist) -> 'a1 -> 'a1 cotree **)

let rec unfold_cotree next init =
  lazy (Conode (init, (comap (unfold_cotree next) (next init))))

With QPFTypes, construction and observation instead go through the generic MvQPF.Cofix.corec and MvQPF.Cofix.dest operations. The program keeps the generic Cofix representation rather than becoming the direct lazy tree above. That is fine as mathematics, but it is not the program I would write by hand.

If you want to poke at QPFTypes yourself, BadCoinduction.lean contains the full experiment behind this section: working Colist and Cotree definitions, examples of the generated interface, and checked failures for parameterless, mutual, and indexed codata. Its header records the exact QPFTypes commit and command needed to rerun the test.

Current Lean alternatives

At this point, a Lean programmer may be shouting at the screen: nobody reaches for QPFTypes just to write a stream. Fair enough. QPFTypes is here because it comes closest to a Rocq-style codata declaration. Day-to-day Lean uses several other tricks.

For streams, mathlib’s Stream' is the obvious answer. It is just Nat → α: ask for position n and get an element back. It runs, and mathlib supplies corecursors along with extensionality, bisimulation, and coinduction lemmas, so it is pleasant to prove things about. But it is not a lazy constructor whose tail is another stream. It solves streams, not arbitrary mutual or indexed codata.

Another option is an explicit state machine: keep some state, write a step function, and use it as a corecursor. Lean’s current Iter interface packages this pattern for sequences and computes one step at a time, on demand. An iterator may carry a Productive proof that it will eventually yield a value or finish; Iter.repeat already has one. With a custom iterator, I have to supply the step interface, its invariants, and perhaps that productivity proof. This works, but now I am doing the plumbing between a state machine and the sequence myself. A Rocq CoFixpoint checks its recursive calls for guardedness and gives me the coinductive value directly.

Thunk buys laziness, but not coinduction. Compiled Lean delays a thunk until it is forced and then caches the result. The logic sees a Unit → α, which means total definitions involving thunks remain available to proofs, although the caching is invisible. A thunk neither permits recursion nor checks that recursion eventually produces a constructor. An extracted Rocq cofixpoint uses similar runtime laziness only after its recursion has passed the guardedness checker.

partial def is the blunt instrument. The compiler runs the recursive body, but the logic gets only an opaque constant. Lean checks neither termination nor productivity here; it accepts both a thunked producer of the natural numbers and a producer that immediately calls itself forever. An unsafe def also runs, but theorem-safe declarations cannot mention it at all. Batteries’ MLList shows the usual arrangement: a private unsafe lazy implementation, an opaque public interface, and producers such as fix and iterate written as partial defs. Those producers cannot be unfolded in proofs the way an observed Rocq cofixpoint can. Lean also has partial_fixpoint, which retains equations, but it does not accept this kind of constructor-and-thunk recursion.

QPFTypes avoids that opacity: it gives me a corecursor and bisimulation principles. But then I am back to its generic Cofix representation and the declaration restrictions I tested above.

Why am I worrying about anything beyond streams? Interaction trees. The interaction trees library in Rocq represents effectful, possibly nonterminating programs as coinductive trees. I can write programs with them, interpret and extract those programs, and prove equations about the same trees, usually up to weak bisimulation. Stream' and Iter only give me sequences, not the branching continuations needed for effects. I could run a hand-written effect tree with Thunk and partial def, but then the recursive producer would be opaque to proofs. Getting all of that in Lean requires a library encoding of codata.

MIT PLV’s lean4-itree does this for interaction trees using Mathlib’s PFunctor.M final coalgebra. The newer PolyFun adds handlers, recursive procedures, traces, strong and weak bisimulation, and proofs of the monad and iteration laws. I can compute with these trees and prove things about them in Lean. They are still library-encoded M-types, though. Lean has no native codata declaration here, and computation keeps the generic representation rather than producing the direct lazy program Rocq extracts.

HITrees are not a way around this problem. The authors consider the coinductive Delay-monad approach used by ITrees, but Lean’s lack of native coinductive types rules it out. Their trees are inductive instead, and nontermination becomes a higher-order recursion effect. A recursive computation is no longer an infinite tree that I can observe and unfold; its recursion gets a meaning only when a handler interprets the effect. The monadic interpretation can run it, and proofs can go through the state-machine interpretation, but the HITree equational theory does not provide the usual recursion-unfolding equation. It works. It also moves nontermination out of the tree and into the interpreter, which I find more awkward than writing a guarded Rocq cofixpoint.

With Lean, I have to give up one of these things or rebuild it on top of generic machinery. Rocq lets me declare codata, write a guarded producer, reason about it by observation, and extract direct lazy code. That is what I want from coinduction.

Nested inductive types and predicates

Meven Lennon-Bertrand pointed this out to me, and I expanded the example below. Lean accepts many nested inductive definitions, but its checker rejects some definitions accepted by Rocq. I ran into this while writing my proof pearl A Rose Tree Is Blooming, which relies on this part of Rocq and would have been considerably uglier to write in Lean. The rose tree example is too large for this post, so here is the same issue with JSON schemas.

Suppose you have a JSON schema language and want to prove the usual things about validation: field names line up, dropping a field from the schema is safe, and validating a prefix works. Routine stuff if you are building a verified system. Defining JSON and schemas is no trouble in either language:

Inductive json : Type :=
| jnull : json
| jstr  : string -> json
| jnum  : nat -> json
| jarr  : list json -> json
| jobj  : list (string * json) -> json.

Inductive schema : Type :=
| sany : schema
| sstr : schema
| snum : schema
| sarr : schema -> schema
| sobj : list (string * schema) -> schema.
inductive JSON where
  | null : JSON
  | str  : String → JSON
  | num  : Nat → JSON
  | arr  : List JSON → JSON
  | obj  : List (String × JSON) → JSON

inductive Schema where
  | any  : Schema
  | strS : Schema
  | numS : Schema
  | arrS : Schema → Schema
  | objS : List (String × Schema) → Schema

The interesting part is the validation relation. An object schema like { "name": string, "age": number } should validate an object { "name": "Alice", "age": 30 } by checking, pairwise, that the field names match and that each value validates against the corresponding sub-schema. Rocq can store all of that in one Forall2 derivation:

Inductive valid : schema -> json -> Prop :=
  | valid_any : forall j, valid sany j
  | valid_str : forall s, valid sstr (jstr s)
  | valid_num : forall n, valid snum (jnum n)
  | valid_arr : forall elem_schema elems,
      Forall (fun j => valid elem_schema j) elems ->
      valid (sarr elem_schema) (jarr elems)
  | valid_obj : forall schema_fields json_fields,
      Forall2
        (fun (sf : string * schema) (jf : string * json) =>
          fst sf = fst jf /\ valid (snd sf) (snd jf))
        schema_fields json_fields ->
      valid (sobj schema_fields) (jobj json_fields).

The projections are deliberate. Rocq 9.0 rejects an equivalent tuple-pattern lambda around the recursive occurrence as non-strictly positive; its syntactic checker does not see through that pattern match. The projection-based declaration above compiles.

Lean 4.32.1 rejects the corresponding object constructor:

inductive ValidCombined : Schema → JSON → Prop where
  | obj :
      Forall₂
        (fun (sf : String × Schema) (jf : String × JSON) =>
          sf.1 = jf.1 ∧ ValidCombined sf.2 jf.2)
        schemaFields jsonFields →
      ValidCombined (.objS schemaFields) (.obj jsonFields)
error: (kernel) invalid nested inductive datatype 'And',
nested inductive datatypes parameters cannot contain local variables.

Lean accepts several nearby forms: Forall₂ ParRed, direct recursion through And and Exists, and Forall₂ (fun sf jf => Valid sf.2 jf.2). In the rejected declaration, the recursive occurrence passes through both Forall₂ and And, and the kernel reports the inner And. A different case, Forall₂ (Eval env), fails at Forall₂ because its relation parameter captures the constructor-local env.

Lean can retain the list structure by splitting the combined relation into two Forall₂ derivations:

inductive Valid : Schema → JSON → Prop where
  | obj :
      Forall₂
        (fun (sf : String × Schema) (jf : String × JSON) =>
          sf.1 = jf.1)
        schemaFields jsonFields →
      Forall₂
        (fun (sf : String × Schema) (jf : String × JSON) =>
          Valid sf.2 jf.2)
        schemaFields jsonFields →
      Valid (.objS schemaFields) (.obj jsonFields)

No indices or separate length proof are needed. Dropping the head remains structural, although Lean must destruct both derivations:

Lemma Forall2_tail :
  forall (A B : Type) (R : A -> B -> Prop)
         (a : A) (b : B) xs ys,
    Forall2 R (a :: xs) (b :: ys) ->
    Forall2 R xs ys.
Proof.
  intros. inversion H; assumption.
Qed.
theorem Valid.dropHead
    (hv : Valid (.objS ((k, s) :: schemaFields))
               (.obj ((k', j) :: jsonFields))) :
    Valid (.objS schemaFields) (.obj jsonFields) := by
  cases hv with
  | obj hnames hvalues =>
      cases hnames
      cases hvalues
      exact .obj
        ‹Forall₂ _ schemaFields jsonFields›
        ‹Forall₂ _ schemaFields jsonFields›

Splitting the relation loses the single proof object that pairs each name equality with its recursive validation. I can recover that pairing with a mutual ValidFields relation, but then Lean’s induction tactic does not support mutual inductive types, and the generated recursor takes a motive for every relation. A custom induction theorem can hide that setup. Rocq keeps the standard Forall2 representation, and Scheme can generate combined principles when a mutual definition is needed.

Lean can express the same propositions without an index-based encoding, but it makes me rearrange the declaration and build more proof machinery. Neither system automatically supplies an elementwise induction principle for nested data such as Term containing list Term; both need a stronger recursor for hypotheses about the list elements (Meven also told me that Rocq 9.2 fixes it, see footnote for details: 1).

You can run the whole comparison yourself: NestedPain.v is the Rocq 9.0.0 side, and NestedPain.lean is the Lean 4.32.1 side. The Lean file wraps expected failures in #guard_msgs, so the errors are checked during compilation instead of being left as untested comments.

Program extraction

Eventually, I need these definitions to become programs I can run.

Lean is opinionated about extraction: its standard toolchain compiles through its own runtime. Sure, this is a genuine plus if you are writing Lean libraries and the runtime’s design fits your needs. And Lean’s standard toolchain deserves real credit on performance: Kim Morrison’s verified lean-zip can even compress faster than pure-Rust miniz_oxide! That is impressive. But performance is not the whole story for extraction. I also care whether I can read the generated code, choose its target, or put it through a verified pipeline.

Lean does not hand you a menu of alternate extraction backends, and the compilation pipeline it has offers no end-to-end correctness proof (hence the rare runtime bugs like the one Kiran Gopinathan found), nor is it readable in my opinion (which is normal as it is not designed for it! The produced code is very runtime-specific).

In contrast, Rocq gives me several routes from definitions to runnable programs, with different trade-offs on TCBs, readability, etc.:

Odds are, one of those routes will work.

Ecosystem

The ecosystem is the part I cannot casually replace. Most of the infrastructure below is written in Rocq; a few entries are external tools with an established Rocq backend or component.

You might skim that list and think, “None of this is a big deal; I can vibe-port the piece I need to Lean over a weekend.” Maybe you can. But hold that thought for one more section.

I should admit that some of these projects are not actively maintained. In my experience, though, I can usually throw an agent at one and get it building and running again pretty easily.

Regulatory acceptance

I have no firsthand experience of taking a tool through certification, and I am not an expert on regulatory acceptance. This point came from Meven, who noted that it may matter more to my European colleagues than it does to me.

ANSSI has published criteria for using Rocq in Common Criteria evaluations. The CompCert project reports that in 2026 the compiler was successfully qualified for the MFC_NG computer on ATR 42/72 aircraft, in work by AbsInt with guidance from Airbus.

I cannot say what a Lean port would be required to do in either setting. Even a clean weekend port would not automatically inherit that history; whether it would be accepted is a question for people familiar with these processes.

But what about the AI agents?

This is the question I actually get asked the most. I know all the hype is on making AI agents write Lean, but the agents are perfectly good at writing Rocq too.

“But the AI only knows the popular language” is an argument with a short shelf life, and it is not a reason for me to switch proof assistants.

Epilogue

Lean is doing serious program-verification work (look at mvcgen and Velvet!) but moving my work there would still mean reshaping definitions and replacing extraction pipelines, libraries, and institutional history I already rely on. Given the work I actually do, Rocq is the better fit for me today.

  1. Rocq 9.2 generates induction hypotheses for nested arguments, once an All predicate and its theorem are registered for the nesting type. The stdlib does not register any, so you still write one line yourself: put Scheme All for list. before the Term declaration and the generated Term_ind and Term_rect gain a list_all Term P l hypothesis on the app case, with the body calling list_all_forall. That is exactly the Term_rect_strong I hand-wrote, so ParRed_refl goes through with a plain induction term. It works for the nested relation too: after Scheme All for Forall2., ParRed_ind gives an induction hypothesis for the Forall2 ParRed args args' premise. Without the Scheme All line you get the old weak principle plus a [register-all] warning telling you to add it. Lean still needs the stronger recursor.↩︎