OxiLean

July 16, 2026 · View on GitHub

Pure Rust Interactive Theorem Prover An implementation of the Calculus of Inductive Constructions (CiC), inspired by Lean 4

Overview

OxiLean is a memory-safe, high-performance Interactive Theorem Prover (ITP) written entirely in Rust with zero C/Fortran dependencies. Inspired by Lean 4, it brings formal verification to the Rust ecosystem with:

Zero-dependency kernel -- Trusted Computing Base with zero external crate dependencies
1.35M+ lines of Rust across 6,050 source files and 17 crates
33,238 tests passing -- comprehensive test suite with zero warnings (746 ignored)
WASM support -- Runs in the browser with no server required
Full tactic framework -- intro, apply, simp, ring, omega, and more
Interactive REPL -- Theorem proving from the command line
oxilean-verify -- Independent Lean 4 proof checker over lean4export files ("Kernel in a Tab")

oxilean-verify — Independent Lean 4 Proof Checker

oxilean-verify is an independent re-implementation of the Lean 4 kernel's checking rules that reads Lean's own export format (lean4export NDJSON) and re-checks every declaration from scratch — no Lean binary, no olean loading, no C++. Its Trusted Computing Base is exactly two crates, oxilean-kernel + oxilean-export, both with zero external runtime dependencies and #![forbid(unsafe_code)] (enforced by CI gates on every push: scripts/gate-zero-deps.sh, gate-forbid-unsafe.sh, gate-allow-list.sh). The CLI crate oxilean-verify itself is in the same zero-dep, no-unsafe regime — argument parsing and JSON reporting are hand-rolled.

Three-bucket semantics (never a wrong verdict)

Every declaration gets exactly one verdict; nothing is skipped silently:

Verdict	Meaning	Exit code
`verified`	checked against our independent implementation of the kernel rules and accepted	`0` (when nothing was rejected)
`unsupported`	a named missing feature (e.g. `nested inductives`); the checker declines rather than guess	`0` (counted + named in the report)
`rejected`	the alarm: we checked it and it is not a proof	`1`
— broken input file, bad flag, I/O error	"this file is broken" is a different conversation than "this proof is wrong"	`2`

Over all 57,277 declarations of Lean 4 core's Init export (v4.32.0-rc1, 6,453,270 NDJSON lines, 345 MB), in one process, one pass:

35424 verified · 21853 unsupported · 0 rejected      (exit status 0)

bucket	count	share
verified	35,424	61.8%
unsupported (named buckets)	21,853	38.2%
rejected	0	0%

Qualifiers that must travel with the number: the unsupported bucket is dominated by a single root cause — one nested-inductive type (Lean.Syntax) whose dependency cascade accounts for the overwhelming majority of it; "0 rejected" means nothing in Lean core was mis-flagged and the checker found no incorrect proof — it does not mean everything was verified, because the checker refuses to guess.

Structural sharing (wave5, 2026-07-16). The kernel Expr moved from a deep Box tree to reference-counted, cached-header Node edges (Box<Expr> → Rc<Expr> → a Node caching each subterm's looseBVarRange and rebuild-cost), and the export reader now materialises the shared DAG once (Init's 908,550,041 tree nodes are 552,915 distinct exprs, a ~1,643× factor) instead of re-expanding it per parent. Full-Init wall fell from 1 h 20 m 44 s to 11 m 28 s (≈7×, ~83 decls/s) and peak RSS from 9.98 GiB + ~6.7 GiB of swap-thrash to ≈6 GiB with no swap — the verdicts are a strict superset of the pre-sharing 35,223 (the +201 is exactly explained: with clones now O(1) refcount bumps the deterministic per-declaration fuel stops over-charging shared subterms, and the untouched-subtree substitution skip charges the same fuel a rebuild would, so declarations that previously hit the resource limit now verify — nothing regresses, rejected stays 0). The lean4lean per-declaration compute gap (below) predates this work and has not been re-measured on Init.Prelude. Full report of the pre-sharing run with the follower attribution table and reproduction command: docs/reports/2026-07-15-lean-core-init.md.

Kernel in a Tab (WASM, 144 KB gzip)

The same checker compiles to a 144 KB gzipped WASM artifact — 147,132 B measured at 0.1.3 (oxilean-verify-wasm: kernel + export + verify + wasm-bindgen only) — and runs entirely client-side — drop an .ndjson export on the page, watch streaming verdicts, 0 bytes uploaded:

cd web/verify-demo
python3 -m http.server 8000
# open http://localhost:8000

No CDN, no framework, no server round-trips; the browser demo and the native binary drive the identical verify_stream code path.

Differential testing vs lean4lean

verify/differential/ runs oxilean-verify and lean4lean over the same declarations and joins per-declaration verdicts by name. On Init.Prelude the harness first surfaced 20 real disagreements (all oxilean false-rejections of multi-constructor *.noConfusion — one systematic kernel bug, since fixed); the post-fix re-run joins at 0 disagreements across 1,987 declarations. Caveats recorded in the harness README: lean4lean master pins Lean v4.29.0 vs our v4.32.0-rc1 corpus (declaration-set skew lands in ONLY-ONE-SIDE, not DISAGREE), and lean4lean's default replayFromImports path segfaults on that toolchain, so the harness drives it with --fresh. Baseline throughput measured there: lean4lean ~3,280 decls/s vs oxilean-verify ~398 decls/s on the same Init.Prelude set (~8.2× slower — outside the 5× budget, tracked). See verify/differential/RESULTS-2026-07-12.md.

Pins

what	pin
lean4export	`3de59f10bc4b4a0f2de698597aeb1246caa0df0a`
Lean	`v4.32.0-rc1` (githash `b4812ae53eea93439ad5dce5a5c26591c31cb697`)
NDJSON format	`3.1.0`

oxilean-verify --version prints the pins. Full schema, exit codes, JSON report format, and the unsupported-feature list: docs/VERIFY.md.

Architecture

                         +-----------------------+
                         |     oxilean-wasm      |  Browser / JS bindings
                         +-----------+-----------+
                                     |
+----------------+  +----------------+  +----------------+  +----------------+
|  oxilean-cli   |  | oxilean-build  |  | oxilean-codegen|  |  oxilean-lint  |
|  (REPL, check) |  | (project mgmt) |  | (LCNF compile) |  | (static anal.) |
+-------+--------+  +-------+--------+  +-------+--------+  +-------+--------+
        |                    |                   |                    |
        +--------------------+-------------------+--------------------+
                             |
               +-------------+-------------+
               |        oxilean-std        |  Standard library
               +-------------+-------------+
                             |
               +-------------+-------------+
               |       oxilean-runtime     |  Memory, closures, I/O
               +-------------+-------------+
                             |
               +-------------+-------------+
               |        oxilean-elab       |  Elaborator
               +-------------+-------------+
                             |
               +-------------+-------------+
               |        oxilean-meta       |  Unification, tactics,
               |                           |  type class synthesis
               +-------------+-------------+
                             |
               +-------------+-------------+
               |       oxilean-parse       |  Lexer, parser, AST
               +-------------+-------------+
                             |
        +--------------------+--------------------+
        |          oxilean-kernel (TCB)           |
        |    Type checking core -- ZERO deps      |
        +-----------------------------------------+

Layer summary: kernel (TCB) -> meta -> parse -> elab -> cli / build / codegen / runtime / lint / std -> wasm

Workspace Crates

Crate	SLOC	Tests	Description
`oxilean-kernel`	127,298	3,485	Trusted Computing Base -- type checking core (zero external deps, `#![forbid(unsafe_code)]`)
`oxilean-export`	4,100	77	lean4export NDJSON v3.1.0 reader + replay (TCB, zero external deps)
`oxilean-verify`	2,205	47	Independent Lean 4 proof checker CLI (three-bucket verdicts)
`oxilean-verify-wasm`	399	4	"Kernel in a Tab" WASM bindings (144 KB gzip)
`oxilean-meta`	162,760	5,410	Metavar-aware WHNF, unification, type class synthesis, tactics
`oxilean-parse`	67,245	2,341	Concrete syntax to abstract syntax parser
`oxilean-elab`	101,970	3,497	Surface syntax to kernel terms elaborator
`oxilean-cli`	72,892	2,191	Command-line interface with REPL
`oxilean-std`	440,384	7,934	Standard library (mathematics, logic, data structures)
`oxilean-codegen`	247,202	4,713	LCNF-based compilation and optimization code generator
`oxilean-runtime`	35,229	1,162	Memory management, closures, I/O, task scheduling
`oxilean-build`	30,782	783	Project compilation and dependency management
`oxilean-lint`	22,111	425	Static analysis and lint rules
`oxilean-doc`	2,685	97	Documentation generation
`oxilake`	2,543	63	Lake-style project/package tooling
`oxilean-wasm`	1,797	59	WebAssembly bindings (browser support)
`oxilean` (umbrella)	22	0	Facade crate re-exporting the workspace
workspace `tests/`	—	1,689	Root integration suites (incl. Mathlib compat harness)
Total	1,345,501	33,984	17 crates, 6,050 Rust files (33,238 run + 746 ignored)

Fun fact: The COCOMO cost estimate for this codebase is $47M+.

Feature Status

Type Theory

Universe hierarchy: Prop : Type 0 : Type 1 : ...
Dependent types: Pi (x : A), B
Inductive types: Nat, List, Eq, etc.
Proof irrelevance: two proofs of the same proposition are definitionally equal
Universe polymorphism: definitions can be polymorphic over universe levels

Tactics

intro, apply, exact, simp, rfl, ring, omega, sorry, cases, induction, constructor

CLI

REPL mode: interactive theorem proving shell
File checking: oxilean check <file> for .oxilean and .lean files
REPL commands: :type, :check, :env, :clear, :help, :quit

Mathlib4 Compatibility

OxiLean includes a syntax compatibility test suite that parses real Lean 4 / Mathlib4 declarations after applying automated normalization. This measures how much of Mathlib4's surface syntax OxiLean can handle.

7,759 Mathlib4 source files parsed across 280+ categories
181,890 declarations tested -- 99.7% parse compatibility (181,326 parsed OK)
The 99.7% is a parse number (surface syntax accepted by the parser), not a verification number -- kernel-verification results live in the oxilean-verify section above and are measured on lean4export corpora, not Mathlib source
Categories span all 28+ top-level Mathlib directories: Algebra, Analysis, CategoryTheory, Combinatorics, Data, FieldTheory, Geometry, GroupTheory, LinearAlgebra, Logic, MeasureTheory, NumberTheory, Order, Probability, RingTheory, SetTheory, Topology, and more

Track 1 (parser compat): Reads .lean files from a local Mathlib4 checkout, normalizes syntax (=> to ->, Unicode shorthand, head binders to forall, 280+ Unicode operators, etc.), and parses with OxiLean. The normalization pipeline handles quantifier binders, set-builder notation, subscript indexing, proof replacement, and more.

Track 2 (curated theorems): 320 hand-adapted Mathlib4 theorems verified through parse + elaboration + tactic execution.

To run these tests locally, create .env.mathlib in the project root:

# .env.mathlib
MATHLIB4_ROOT=/path/to/mathlib4/Mathlib

# Run mathlib compat tests (ignored by default in normal test runs)
cargo test --test mathlib_compat_test -- --ignored --nocapture
cargo test --test mathlib_theorems_test

WASM / npm

Published as @cooljapan/oxilean on npm.

npm install @cooljapan/oxilean

import { WasmOxiLean, checkSource, getVersion } from '@cooljapan/oxilean';

const ox = new WasmOxiLean();
const result = ox.check('theorem foo : True := trivial');
console.log(result.success); // true
console.log(result.declarations); // [{ name: "decl_0", kind: "theorem", ty: "Prop" }]
ox.free();

Full API: check, repl, completions, hoverInfo, format, sessionId, history, clearHistory, version

Supports bundler (webpack/vite), web (browser), and Node.js targets. See oxilean-wasm README for details.

What's New in v0.1.3

oxilean-verify — independent Lean 4 proof checker: streaming three-bucket CLI (verified / unsupported (named) / rejected = alarm) over lean4export NDJSON v3.1.0; TCB = oxilean-kernel + oxilean-export, zero external runtime deps, #![forbid(unsafe_code)]
First full-corpus result — Lean core Init (all 57,277 declarations): 35,424 verified · 21,853 unsupported (named) · 0 rejected, exit 0 (report)
Structural sharing (wave5) — kernel Expr as reference-counted, cached-header Node edges + materialise-once export reader: full-Init wall 1 h 20 m → 11 m 28 s (≈7×), peak RSS 9.98 GiB + swap-thrash → ≈6 GiB, no swap, verdicts a strict superset (0 rejected). Plus a per-declaration wall-clock deadline and a file-streaming CLI so a whole-corpus export (Mathlib, ~6 GB) verifies without loading it into RAM
Kernel in a Tab — oxilean-verify-wasm at 144 KB gzip + static browser demo (web/verify-demo), all checking client-side, 0 bytes uploaded
Differential harness vs lean4lean — found 20 real disagreements (one systematic noConfusion kernel bug), fixed: post-fix re-run joins at 0 disagreements (results)
Kernel soundness overhaul — arbitrary-precision BigNat literals (u64-overflow hole closed), quotients re-checked against kernel-built canonical types, recursors re-derived (never trusted from the export), kernel-decided large elimination, complete universe-level def-eq
CI/TCB gates + fuzzing — zero-deps / forbid-unsafe / allow-list gates, WASM export & size gates, three cargo-fuzz targets with a weekly CI workflow

Quick Start

# Clone the repository
git clone https://github.com/cool-japan/oxilean
cd oxilean

# Build the project
cargo build --release

# Run the REPL
cargo run --bin oxilean

# Check a file
cargo run --bin oxilean -- check examples/hello.oxilean

# Run tests
cargo test --workspace

Development

Prerequisites

Rust 1.70 or later
No external (non-Rust) dependencies required

Running Tests

# All tests (33,238 tests, ~78s)
cargo test --workspace

# With cargo-nextest (recommended)
cargo nextest run --no-fail-fast

# Kernel tests only
cargo test -p oxilean-kernel

# With verbose output
cargo test --workspace -- --nocapture