◉ COOLJAPAN
← All posts
March 5, 2026 • 9 min read

OxiLean 0.1.0 Released — A Pure Rust Interactive Theorem Prover, Native to Rust

OxiLean 0.1.0 is the debut of a memory-safe Interactive Theorem Prover written entirely in Rust, inspired by Lean 4 — a zero-dependency kernel implementing the full Calculus of Inductive Constructions, a complete tactic framework, and a WASM REPL that runs in the browser.

release oxilean formal-verification theorem-prover pure-rust lean4 type-theory

Formal verification just became native to Rust — proof-checked theorems, a zero-dependency kernel, and no C++ or OCaml in sight.

Today we released OxiLean 0.1.0 — a Lean 4-inspired Interactive Theorem Prover, implementing the Calculus of Inductive Constructions (CiC), written entirely in pure Rust.

No C. No Fortran. No OCaml. The serious theorem provers have always been other people’s runtimes: Lean 4 ships a C++ kernel with a self-hosted Lean frontend, Coq is an OCaml toolchain, and Isabelle is built on Standard ML. Each is a remarkable piece of engineering — and each is a large foreign toolchain you bolt onto the side of your project rather than something native to the language you already work in. OxiLean is different. The kernel, the elaborator, the parser, the tactic framework, the standard library, the code generator — all of it is Rust, with zero C or Fortran dependencies. It compiles to a single static binary, and it also runs as WebAssembly in the browser with no server required. This is the debut release: early but solid, and it already does real proof checking.

Why 0.1.0 matters

Bringing formal verification into a project today usually means adopting a separate ecosystem. Theorem provers are big OCaml and C++ toolchains with their own build systems, their own package managers, and their own runtimes. Embedding one inside a Rust application is awkward, the trusted core is hard to audit because it spans languages and unsafe FFI boundaries, and none of it is native to the way Rust developers actually build and ship software.

OxiLean 0.1.0 is the first real release, and it is deliberately small in surface but honest in substance. The early wins:

It is a 0.1.0 — not a drop-in replacement for a mature prover’s massive mathematical library — but the foundations are real and the kernel is sound.

Technical Deep Dive: a layered, auditable architecture

OxiLean is built as eleven workspace crates, layered so that trust flows outward from a tiny, dependency-free core. At 0.1.0 it already totals 1,221,710 SLOC across 5,380 Rust files — and just for fun, COCOMO puts the cost of writing all that at over $47M.

oxilean-kernel (113,179 SLOC) — the Trusted Computing Base. This is the heart, and it has zero external dependencies. It defines Arena<T>, a typed arena allocator addressed by Idx<T>; Name, hierarchical names (Anonymous / Str / Num) with a name! macro; Level, the universe levels (Zero / Succ / Max / IMax / Param); and Expr, the core term type with its variants BVar, FVar, Sort, Const, App, Lam, Pi, Let, Lit, and Proj. Binders carry BinderInfo (Default / Implicit / StrictImplicit / InstImplicit), and Literal holds native Nat and String values. On top of this sit the substitution engine (instantiate, abstract, lift_bvars), WHNF reduction with beta / delta / zeta / iota / projection / quotient reduction, type inference for every Expr variant, definitional equality with proof irrelevance, declaration checking (Axiom / Definition / Theorem / Opaque), inductive types with strict positivity checking, recursor generation plus iota-reduction rules, quotient types (Quot.mk, Quot.lift, Quot.sound), and the bootstrap types Bool / Unit / Empty / Nat / String.

oxilean-meta (150,298 SLOC) — metavariables and tactics. Metavar-aware WHNF, a higher-order unification engine, type class synthesis and instance resolution, the tactic infrastructure and metaprogramming framework, and AST manipulation live here.

oxilean-parse (61,225 SLOC) — the front end. A UTF-8 lexer with full Unicode identifier support, 60+ token types carrying source spans, a Pratt parser for operator precedence, 27 SurfaceExpr variants and 16 Command variants, a tactic parser covering 40+ tactic forms, a hygienic macro system, a notation system, a module system with dependency-graph resolution, a pattern compiler, a pretty printer, a source map, and error recovery.

oxilean-elab (91,008 SLOC) — elaboration. The MetaContext handles metavar creation, assignment, and zonking; a constraint-based unification solver drives full elaboration — name resolution, implicit-argument insertion, universe polymorphism — alongside pattern-match compilation with exhaustiveness and redundancy checking, declaration elaboration for def / theorem / inductive / structure / class / instance, an attribute system, a coercion system, a derive system, parallel elaboration, and termination checking. This is also where the core tactics live: intro, apply, exact, simp, omega, ring, cases, induction, constructor, rewrite, have, let, suffices, show, assumption, contradiction, exfalso, trivial, decide, norm_num, linarith, field_simp, ring_nf, push_neg, by_contra, by_cases, ext, funext, congr, calc, rfl, symm, and trans.

oxilean-std (413,202 SLOC) — the library. Core data structures (Nat, Bool, List, Option, Result), a math and proof library, an algebraic hierarchy (Semigroup, Monoid, Group, Ring, Field), type classes (Eq, Ord, Functor, Monad, Applicative, Decidable), and decision procedures.

oxilean-codegen (240,840 SLOC) — compilation. An LCNF (lambda-lifted closure-free normal form) IR, an LCNF-based compilation pipeline with optimization passes, and a Rust code generation backend — so proofs and definitions can be lowered to actual Rust.

oxilean-runtime (31,115 SLOC), oxilean-build (25,194 SLOC), oxilean-cli (64,163 SLOC), oxilean-lint (17,061 SLOC), oxilean-wasm (381 SLOC). The runtime handles memory management, object representation, closure allocation and application, an I/O monad, and task scheduling. The build crate does multi-file project compilation with topological dependency ordering and incremental builds. The CLI provides the interactive REPL — line editing, history, multi-line input, colorized output, file checking for .oxilean and .lean files, and #check / #eval / #print. The lint crate runs static analysis, style enforcement, and best-practice recommendations. And the wasm crate exposes check / repl / completions / hover / format through wasm-bindgen.

Throughout: clippy is clean, there are zero warnings, no unwrap() in production code, no unsafe in the kernel, and all versions are workspace-managed.

Getting Started

OxiLean requires Rust 1.70+ and is Apache-2.0 licensed. The publishable entry library crate is oxilean-kernel:

cargo add oxilean-kernel

The fastest way to actually prove something is the REPL. Clone, build, and run:

git clone https://github.com/cool-japan/oxilean
cd oxilean
cargo build --release
cargo run --bin oxilean                                  # REPL
cargo run --bin oxilean -- check examples/hello.oxilean  # check a file

A tiny REPL session, using the real commands:

> theorem foo : True := trivial
> #check foo
foo : True
> #print foo
theorem foo : True := trivial
> #eval 2 + 2
4

And because OxiLean ships as WebAssembly, you can prove theorems in the browser with no server. Install the npm package:

npm install @cooljapan/oxilean

import { WasmOxiLean } 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();

What’s inside

Tips

This is the foundation

OxiLean is the formal-verification and mathematical-correctness layer of the COOLJAPAN ecosystem. The other pure-Rust pieces give you the computation; OxiLean lets you prove things about it. It sits naturally alongside OxiZ, our pure-Rust SMT solver, for automated reasoning; SciRS2 for scientific computing; OxiBLAS for pure-Rust linear algebra; and OxiFFT for pure-Rust transforms — OxiLean can state and check the correctness properties those libraries rely on. And it pairs with Legalis-RS, our law-as-code project, where machine-checked reasoning is exactly the point. Every layer is Rust, every layer is sovereign, and now there is a layer for proofs.

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

Star the repo if a memory-safe, dependency-free theorem prover native to Rust is something you’ve been waiting for — and tell us what you prove with it.

Pure Rust formal verification is here — fast, safe, auditable, and sovereign.

— KitaSan at COOLJAPAN OÜ March 5, 2026

↑ Back to all posts