OxiLean 0.1.1 Released — A Memory-Safe Interactive Theorem Prover Natively in Rust

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.

Why OxiLean is revolutionary

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:

• Universe hierarchy (Prop : Type 0 : Type 1 : …)
• Dependent types (Π (x : A), B) and inductive types
• Proof irrelevance and universe polymorphism
• Full metaprogramming layer (oxilean-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.

What’s inside 0.1.1

• Core tactics: intro, apply, exact, simp, rfl, ring, omega, cases, induction, constructor, sorry
• Elaborator & unification: Full metavariable-aware WHNF, type class synthesis, and dependent pattern matching
• Mathlib4 compatibility: 99.7% parse success on 7,759 files (181,890 declarations). 320 hand-ported theorems already verified end-to-end.
• Rust-native tooling: .oxilean files checked via cargo oxilean, proc-macro integration, WASM REPL for browser-based verification
• Code generation: oxilean-codegen turns proven theorems into optimized Rust code (LCNF → Rust)
• WASM/npm support: Run full theorem proving in the browser or from Node.js

This is the foundation

OxiLean is now the formal verification layer for the entire COOLJAPAN stack:

• Proving correctness of OxiBLAS / OxiFFT kernels
• Verifying control laws in OxiCtl
• Proving optical device properties in OxiPhoton
• Mathematical safety for AI agents in mielinOS

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