◉ COOLJAPAN
← All posts
May 3, 2026 • 8 min read

OxiLean 0.1.2 Released — Real SMT Solving, a Full WASM Interpreter, and Keccak-Correct EVM Codegen

OxiLean 0.1.2 lands real SMT solving via OxiZ, a complete 157-instruction WebAssembly bytecode interpreter wired to the real kernel/parse/elab pipeline, keccak256-correct EVM/Solidity ABI selectors, real Gröbner-basis reduction for polyrith, and 33,091 passing tests — all in a Pure Rust theorem prover.

release oxilean formal-verification theorem-prover pure-rust smt webassembly lean4

The tactics stopped pretending. SMT, polyrith, and the WASM backend are now the real thing — in 100% Pure Rust.

Today we released OxiLean 0.1.2 — real SMT solving, a full 157-instruction WebAssembly bytecode interpreter, and keccak-correct EVM/Solidity selectors all landing in the Pure Rust theorem prover, alongside a clean codegen build and a jump to 33,091 passing tests.

OxiLean is a Pure Rust Interactive Theorem Prover implementing the Calculus of Inductive Constructions, inspired by Lean 4. Its Trusted Computing Base — the oxilean-kernel crate — carries zero dependencies and is sealed with #![forbid(unsafe_code)]. On top of it sits a full tactic framework, an interactive REPL, and WASM support shipped to npm as @cooljapan/oxilean. As of v0.1.1 it reached 99.7% Mathlib4 parse compatibility across 181,890 declarations and 7,759 files. 0.1.2 is an incremental release, but a substantive one: the tactic backends that were placeholders are now real solvers, and the WASM path that was a stub now runs the actual kernel.

No C. No C++. No Fortran. No OCaml. Lean 4 is built on C++ and bootstrapped Lean; Coq and Isabelle ride on OCaml and ML; and when those provers reach for an SMT oracle they shell out to Z3, a sprawling C++ codebase. OxiLean takes a different path end to end. The kernel is Pure Rust, the elaborator is Pure Rust, and as of 0.1.2 the SMT tactic is Pure Rust too — backed by OxiZ (oxiz-solver), the COOLJAPAN Pure Rust SMT solver that replaces Z3 outright. The result compiles to a single static binary or a WASM module that runs in any browser, with no C toolchain anywhere in the build graph.

Why OxiLean 0.1.2 is a game changer

The incumbents make you assemble a verification stack out of mismatched parts: a prover in one language, an SMT oracle in another, a separate toolchain to extract verified code, and a foreign-function bridge gluing it together. Every seam is a place for unsafe code, version skew, and a broken build to creep in. 0.1.2 closes those seams.

Technical Deep Dive: the tactics get teeth

The elaborator’s tactic backends are now real. Two of the most-requested automation tactics moved off their stubs in this release. The SMT path — SmtContext::check_sat driving run_smt_tactic — now delegates to oxiz-solver 0.2.1 and surfaces the solver’s actual verdict, so arithmetic and decidable goals can be discharged without a hand-written proof term. The polyrith tactic now stands on a genuine GroebnerBasis::reduce implementing full multivariate polynomial division per Cox–Little–O’Shea §2.3; with contains now meaningful for ideal membership, polynomial goals reduce the way the textbook says they should.

Multi-backend codegen, with correct selectors. oxilean-codegen lowers LCNF to a remarkably wide set of targets — Rust, x86_64, WASM, EVM/Solidity, MATLAB, Elixir, Kotlin, and Lua, surfaced concretely in this release through the matlab_backend, wasm_backend, elixir_backend, evm_backend, kotlin_backend, lua_backend, and x86_64_backend modules. The EVM backend now emits spec-correct keccak256 4-byte selectors (via tiny-keccak), so verified Solidity-targeting code interoperates with real chains. New in 0.1.2 is a real optimization pass: InliningPass::run_all / run_with_context in opt_copy_prop is a fixed-point function inliner with variable-ID freshening and a configurable cost threshold.

The WebAssembly interpreter, end to end. WasmModule::call_function in oxilean-wasm now implements all 157 WasmInstruction variants: structured control flow (Block / Loop / If / Else / End), branch instructions (Br / BrIf / BrTable / Return), and frame-stack call dispatch (Call / CallIndirect, with locals and return-PC bookkeeping). Critically, the crate no longer relies on mock or stub stand-ins — it integrates with the real oxilean-kernel, oxilean-parse, and oxilean-elab pipeline, which is the headline fix that unblocked the rest of the release.

Engineering hygiene. Five files in the 1,945–1,985-line range were proactively split with splitrs down to ≤1,004 lines each. The rand dependency moved 0.9.2 → 0.9.4 to resolve RUSTSEC-2026-0097; wasm-bindgen went 0.2.118 → 0.2.120, js-sys 0.3.95 → 0.3.97, and fastrand 2.4.0 → 2.4.1 (the prior version was yanked). And 1,041 rustdoc broken_intra_doc_links / HTML-tag errors were fixed across oxilean-std (math bracket escaping), oxilean-elab, oxilean-parse, and oxilean-wasm.

Getting Started

Add the kernel crate to your project:

cargo add oxilean-kernel

Prefer the browser or Node? OxiLean ships to npm, now backed by the real kernel/parse/elab pipeline:

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
ox.free();

Or clone and drive the REPL directly:

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

What’s New in 0.1.2

Tips

This is the foundation

OxiLean 0.1.2 is where the COOLJAPAN ecosystem’s “Pure Rust all the way down” thesis reaches the proof automation layer. The defining dependency this release is OxiZ (oxiz-solver 0.2.1): OxiLean’s SMT tactic now offloads to it, which means the prover discharges decidable goals without ever leaving the Rust toolchain or touching Z3. That is the whole point — a theorem prover whose automation is as sovereign as its kernel.

It also fits naturally alongside the Pure Rust siblings already shipping: SciRS2 for scientific computing, OxiBLAS for dense linear algebra, OxiFFT for transforms, and Legalis-RS for legal technology. As OxiLean’s multi-backend codegen and verification mature, those are exactly the domains where machine-checked guarantees pay off.

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

Star the repo if you want a theorem prover that solves, compiles, and runs without a single line of C.

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

— KitaSan at COOLJAPAN OÜ May 3, 2026

↑ Back to all posts