Just Lean: a verified, fast sort🔗

Lean is mostly known as a proof assistant. It is also a programming language with a native compiler, and one file can hold a specification, an implementation, a machine-checked proof that the implementation meets the specification, and a main. There is no second language to bridge to and no second toolchain to keep in sync.

This tutorial goes through that pipeline on one example, sorting, three times over:

1. A merge sort on lists that is short enough to read, with a proof that is short enough to read.

2. The same idea on an unboxed array of UInt64, fifteen times faster, with the proof kept.

3. A port of the algorithm behind Rust's Vec::sort, verified, and only a little slower than the Rust version.

All three compile to native binaries. Everything is total (no partial), nothing is sorry, and every theorem depends only on Lean's standard axioms. The prompt was this exchange:

Regarding doing stuff in "just Lean," (which would be great IMO: less languages => less tooling/complexity => less headache), I could not really find any meaningful tutorials.

e.g., I'm thinking "here's a sorting spec in Lean, a merge sort implemented in Lean that you can compile and run and a proof that it sorts according to the spec."

— alin.apt (@alinush) September 8, 2026

One repository. The whole thing is one repository, zksecurity/just-lean. Every Lean snippet on these pages is elaborated when the site is built, against the code in that repository, so what you read is what was checked. The numbers below are for one million and ten million pseudo-random 64-bit integers, in milliseconds, on one machine (see the appendix for how they were measured).

implementation	1M	10M
Part 1: merge sort on lists	770	12300
Part 2: bottom-up merge sort on an unboxed array	50	590
Part 3: verified driftsort	28	300
Rust Vec::sort (driftsort)	19	270
Rust, the same bottom-up merge sort as Part 2	48	555

What is trusted. The theorems are about the model of the array, an ordinary Array UInt64. At runtime the array is a flat buffer of 8-byte elements, and four one-line C snippets in one file (MergeSort/UInt64Array.lean: size, read, write, allocate) are trusted to implement the model. They are not proved; they are the same lines the standard library uses for FloatArray, with the element type changed, and Part 2 shows them side by side. Beyond that: Lean's kernel, compiler and runtime, and clang, which every compiled Lean program trusts.

Following along. You need elan (which installs Lean and Lake from the lean-toolchain file) and a C toolchain. Rust is only needed for the comparison programs.

git clone https://github.com/zksecurity/just-lean
cd just-lean
lake build                      # the library and its proofs
lake exe sortdemo 1000000       # sort a million numbers with the verified driftsort
./check.sh                      # build, cross-check, print axioms, benchmark

Part 1 assumes no Lean beyond what a curious reader can pick up as it goes. Parts 2 and 3 assume you have seen a termination_by and a simp before.