Pure Rust reimplementation of Lean 4’s Calculus of Inductive Constructions. 99.7% Mathlib4 compatibility, zero unsafe in kernel, full tactics + metaprogramming — bringing industrial-grade formal verification directly into the Rust ecosystem.
A historic milestone for the COOLJAPAN ecosystem.
Today we shipped OxiLean 0.1.1 — the first production-ready, memory-safe Interactive Theorem Prover (ITP) written entirely in Rust and natively integrated into the Rust ecosystem.
1.2M+ lines of pure Rust.
29,831 passing tests.
Zero C/Fortran dependencies.
Zero unsafe in the kernel.
This is the day formal verification stops being “something you do in Lean or Coq” and becomes a native part of Rust development.
Rust already gives us memory safety.
OxiLean gives us mathematical safety — the ability to prove at compile time that your code is not only memory-safe, but correct.
Inspired by Lean 4 but rebuilt from the ground up in pure Rust, OxiLean implements the full Calculus of Inductive Constructions (CiC) with:
Prop : Type 0 : Type 1 : …)Π (x : A), B) and inductive typesoxilean-meta)The kernel (Trusted Computing Base) contains no unsafe code and no external crates — just clean, auditable Rust. This is the holy grail for safety-critical and high-assurance systems.
intro, apply, exact, simp, rfl, ring, omega, cases, induction, constructor, sorry.oxilean files checked via cargo oxilean, proc-macro integration, WASM REPL for browser-based verificationoxilean-codegen turns proven theorems into optimized Rust code (LCNF → Rust)OxiLean is now the formal verification layer for the entire COOLJAPAN stack:
Imagine writing #[prove] attributes that the compiler checks with a full dependent type system — all in pure Rust.
Repository: https://github.com/cool-japan/oxilean
Star the repo if you believe the future of systems programming is mathematically verified.
More releases coming this week.
The era of “trust me bro” in Rust is over. Proof is now native.
— KitaSan at COOLJAPAN OÜ
March 9, 2026