Joomy Korkut - Why Rocq is better than Lean for program verification

Home page | Back

Joomy Korkut's blog

Why Rocq is better than Lean for program verification

A write-up on why I don't give in to the hype and switch to Lean for formal verification of programs.

Posted on July 28, 2026,

tags: rocq, lean, formal verification

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 :=<br>| co_unit_loop : co_unit.

codata CoUnit where<br>| loop : CoUnit

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

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 :=<br>| node : a -> forest a -> tree a<br>with forest (a : Type) : Type :=<br>| fnil : forest a<br>| fcons : tree a -> forest a -> forest a.

mutual<br>codata Tree α where<br>| node : α → Forest α → Tree α

codata Forest α where<br>| fnil : Forest α<br>| fcons : Tree α → Forest α → Forest α<br>end

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

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 :=<br>| icons : forall n, a -> istream a (S n) -> istream a n.

codata IStream α : Nat → Type where<br>| icons : α → IStream α (n + 1) → IStream α n

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

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<br>and 'a __cotree =<br>| Conode of 'a * 'a cotree colist

(* other definitions ... *)

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

let rec unfold_cotree next init =<br>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...