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

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 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.

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

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)

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.

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.

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.

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

                         +-----------------------+
                         |     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

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

• 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

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

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

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

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.

• 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

# 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

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

# 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

• Pure Rust -- zero C/Fortran dependencies
• No unwrap() -- all error handling is explicit
• No warnings -- cargo clippy must pass cleanly
• No unsafe in the kernel
• Workspace-managed versions -- version set once in root Cargo.toml
• cargo fmt mandatory before commits

• TODO.md -- Master task list
• CHANGELOG.md -- Version history and release notes
• CONTRIBUTING.md -- Contribution guidelines

Contributions are welcome! This project follows:

• Commit discipline: one logical change per commit
• Testing: all new functions must have tests
• Documentation: public APIs must be documented

See CONTRIBUTING.md for details.

OxiLean is developed and maintained by COOLJAPAN OU (Team Kitasan).

If you find OxiLean useful, please consider sponsoring the project to support continued development of the Pure Rust ecosystem.

https://github.com/sponsors/cool-japan

Your sponsorship helps us:

• Maintain and improve the COOLJAPAN ecosystem
• Keep the entire ecosystem (OxiBLAS, OxiFFT, SciRS2, etc.) 100% Pure Rust
• Provide long-term support and security updates

Copyright (c) COOLJAPAN OU (Team Kitasan). Licensed under Apache-2.0.

• OxiZ -- Pure Rust SMT solver
• Legalis-RS -- Law-as-Code framework
• SciRS2 -- Scientific computing library
• OxiBLAS -- Pure Rust BLAS
• OxiFFT -- Pure Rust FFT

• Inspired by Lean 4
• Built by COOLJAPAN OU (Team Kitasan)

v0.1.3 (2026-07-16) | Under active development