OxiLean 0.1.3 Released — An Independent Lean 4 Proof Checker, a 144 KB 'Kernel in a Tab,' and a 7× Verification Speedup

A second Lean 4 kernel, written independently from scratch, that agrees with the original — and fits in 144 KB.

Today we released OxiLean 0.1.3 — headlined by oxilean-verify, an independent Lean 4 proof checker with three-bucket verdicts; oxilean-verify-wasm, a 144 KB gzip “Kernel in a Tab” that checks proofs entirely client-side; a kernel soundness overhaul closing a real overflow bug; and a structural-sharing rewrite of the kernel’s Expr representation that took a full run over Lean 4 core’s Init library from 1 hour 20 minutes down to 11 minutes 28 seconds.

No C. No C++. No OCaml. Lean 4’s reference kernel is a C++ program under a bootstrapped Lean compiler, so trusting a Lean proof has always meant trusting that C++ codebase, transitively, however deep the proof goes. OxiLean’s trusted computing base for independent checking is exactly two Pure Rust crates — oxilean-kernel and oxilean-export — both with zero external runtime dependencies and #![forbid(unsafe_code)], enforced on every push by CI gates (gate-zero-deps.sh, gate-forbid-unsafe.sh, gate-allow-list.sh). The identical code compiles to a single static binary or to a 144 KB gzip WASM artifact that runs in any browser tab, with zero bytes uploaded.

Why OxiLean 0.1.3 is a game changer

Independently checking a Lean proof has historically meant picking from a short list of bad options:

• Trust Lean’s own C++ kernel, because there’s no small, separately-written second implementation to check it against
• Stand up a full Lean toolchain, olean files, and a running Lean process just to re-verify something that should be a pure function of an export file
• Accept that a kernel’s own fast-path literal arithmetic might be silently wrong at the boundary — a u64 overflow doesn’t announce itself
• Give up on running any of this in a browser, because “proof checker” has always implied “native binary with a build system attached”

OxiLean 0.1.3 ends all of that.

• A genuinely independent checker. oxilean-verify reads Lean’s own lean4export NDJSON format and re-checks every declaration from scratch against oxilean-kernel — no Lean binary, no olean loading, no C++ anywhere in the loop.
• A first full-corpus result. Over all 57,277 declarations of Lean 4 core’s Init export (v4.32.0-rc1, 345 MB of NDJSON): 35,424 verified · 21,853 unsupported · 0 rejected, exit code 0.
• A 7× verification speedup, found and shipped in the same release. Structural sharing of the kernel Expr took the same full-Init run from 1h 20m 44s to 11m 28s, and peak RSS from 9.98 GiB plus ~6.7 GiB of swap-thrash down to about 6 GiB with no swap at all — with the verdict set a strict superset of the pre-sharing run (zero regressions, zero new rejections).
• A real kernel bug, found by differential testing and fixed. Running oxilean-verify against lean4lean over the same declarations surfaced 20 real disagreements — all false rejections from one systematic bug in multi-constructor .noConfusion handling. Fixed; the re-run joins at 0 disagreements across 1,987 declarations of Init.Prelude.
• Kernel in a Tab. The identical checker compiles to a 144 KB gzip WASM module (oxilean-verify-wasm) plus a static demo page (web/verify-demo) that verifies a dropped .ndjson file entirely in-browser — 0 bytes uploaded, no server, no CDN.

Technical Deep Dive: how the independent checker is built

1. Export & replay — oxilean-export. A budgeted, memory-limited reader for lean4export’s NDJSON v3.1.0 format, supporting inductive families, quotients, and recursor verification. Zero external dependencies, #![forbid(unsafe_code)] — the same TCB discipline as the kernel it feeds.
2. The kernel — oxilean-kernel, hardened. This release is a soundness pass as much as a feature: arbitrary-precision BigNat (schoolbook and Karatsuba multiplication, Knuth-D division) replaces the old u64 literal fast path that could silently wrap 2^32 * 2^32 to 0; quotient types are now validated against kernel-built canonical types instead of trusted from the export data; recursors are re-derived from first principles rather than trusted; and level/order.rs implements complete universe-level definitional equality (the trepplein/nanoda algorithm: smart constructors plus a full param-case-split ≤ procedure).
3. The checker — oxilean-verify. A streaming CLI that assigns every declaration to exactly one of three buckets — verified, unsupported (a named missing feature), or rejected (the alarm) — and exits non-zero only on a real rejection. Argument parsing and JSON reporting are hand-rolled: no clap, no serde, so the TCB stays at exactly two crates plus this one.
4. Structural sharing, underneath all of it. Every recursive Expr field is now a cached-header Node { range, cost, rc: Rc<Expr> } instead of a Box<Expr> — cloning becomes an O(1) refcount bump, and the export reader materializes each shared subterm exactly once. Init’s 908,550,041 tree nodes collapse to 552,915 distinct expressions, a ~1,643× sharing factor, which is where the 7× wall-clock win comes from.

Getting Started

Install the checker and point it at a lean4export NDJSON file:

cargo install oxilean-verify

$ oxilean-verify Mathlib.Analysis.SpecialFunctions.Log.Basic.ndjson

✓  Real.log_le_sub_one_of_pos                    1.2 ms
✓  Real.add_pow_le_pow_mul_pow_of_sq_le_sq       4.8 ms
✓  Real.exp_log                                  0.9 ms
⊘  Real.exp_approx        unsupported: Nat literal reduction
✓  Real.log_nonneg                               0.7 ms

1204 verified · 3 unsupported · 0 rejected

Prefer the browser? The same checker runs as the 144 KB WASM build, zero install, zero upload:

cd web/verify-demo
python3 -m http.server 8000
# open http://localhost:8000 and drop an .ndjson file

Or pull the theorem prover itself into a Rust project:

cargo add oxilean-kernel

What’s New in 0.1.3

• oxilean-verify — new independent proof checker CLI: streaming three-bucket verdicts over lean4export NDJSON v3.1.0, hand-rolled JSON reporting (--json, --json-full), --limits {default,corpus}, --fail-fast, --stack-size.
• oxilean-export — new zero-dependency, forbid(unsafe_code) NDJSON v3 reader and replay engine, with a budgeted index-node reader.
• oxilean-verify-wasm + web/verify-demo — “Kernel in a Tab”: a 144 KB gzip cdylib (kernel + export + verify + wasm-bindgen only) and a static drop-a-file browser demo.
• First full-corpus result — all 57,277 declarations of Lean core Init: 35,424 verified · 21,853 unsupported · 0 rejected.
• Structural sharing (wave5) — Box<Expr> → Rc<Expr>/Node edges and a materialize-once export reader; full-Init wall time 1h 20m 44s → 11m 28s (≈7×); peak RSS 9.98 GiB + ~6.7 GiB swap-thrash → ≈6 GiB, no swap.
• Kernel soundness overhaul — arbitrary-precision BigNat; quotients validated against kernel-built canonical types; recursors re-derived, never trusted from the export; complete universe-level definitional equality; definitional eta for structures.
• Fixed — the u64 literal overflow hole; a Quot.ind over-application off-by-one; de Bruijn capture in instantiate; is_prop now kernel-decided instead of trusted from export data; the wrong builtin Quot type; a WASM dead-code-elimination regression that had collapsed the kernel to a 22 KB stub; imax(u,u) normalization.
• Changed (breaking) — Literal::Int(i64) removed from the kernel’s Literal enum; Lean 4’s own kernel has no Int literal, so this is now a hard read error rather than silently accepted.
• CI / TCB gates + fuzzing — zero-deps, forbid-unsafe, and allow-list gates; WASM export-count and size-budget gates; three cargo-fuzz targets on a weekly CI workflow.
• Security — the one remaining unsafe block in oxilean-parse (a ptr::read-based eviction) replaced with a safe retain-based version; #![forbid(unsafe_code)] now propagated to parse, build, codegen, lint, and the umbrella crate.

Tips

• Pick the right --limits preset. default is a small per-declaration budget (2^24 cloned nodes) meant for untrusted input; corpus raises it to 2^26 for trusted whole-corpus runs like Lean core or Mathlib. Get this backwards and a legitimate large proof can land in unsupported for the wrong reason.
• Script CI against the exit code, not just the summary line. 0 means nothing was rejected, 1 means a real rejection (the alarm — treat it as a kernel bug or a genuine broken proof), 2 means the input file or invocation itself was broken. Conflating 1 and 2 silences the one signal this tool exists to give you.
• Use --json - for machine consumption. It routes the human-readable stream and summary to stderr and puts only the JSON report on stdout, so you can pipe it straight into another tool without scraping text.
• A slow declaration isn’t a hang. The per-declaration wall-clock deadline degrades an over-time declaration to a named unsupported: resource limit exceeded, exactly like fuel exhaustion — never a hang, never a guessed verdict.
• Try the browser demo with nothing installed. cd web/verify-demo && python3 -m http.server 8000 — no COOP/COEP, no SharedArrayBuffer, no framework, no CDN.
• Drop any Literal::Int handling. It’s a breaking change: Literal::Int(i64) no longer exists in the kernel’s Literal enum, and reading serialization tag 2 is now a hard error, not a silently-accepted legacy path.

This is the foundation

OxiLean’s verification layer leans directly on its Pure Rust COOLJAPAN siblings:

• OxiZ — the Pure Rust SMT solver (oxiz-solver, oxiz-math) behind OxiLean’s smt tactic.
• OxiArc — Pure Rust compression (oxiarc-deflate) used across the workspace, replacing flate2/zip/zstd.
• OxiCode — the COOLJAPAN Pure Rust serialization layer, replacing bincode.
• SciRS2, OxiBLAS, and OxiFFT — the scientific-computing siblings that a formally verified numerics story would eventually rest on.
• Legalis-RS — the Law-as-Code framework in the same machine-checked-guarantees family.

Repository: https://github.com/cool-japan/oxilean

Star the repo if you want a Lean 4 proof independently re-checked by a second kernel small enough to read in an afternoon and light enough to run in a browser tab.

The era of trusting one C++ kernel to grade its own homework is over. Pure Rust theorem proving is here — independent, auditable, and sovereign.

— KitaSan at COOLJAPAN OÜ July 17, 2026