4 posts
OxiLean 0.1.3 ships oxilean-verify, an independent Lean 4 proof checker with three-bucket verdicts, a 144 KB gzip WASM 'Kernel in a Tab,' a kernel soundness overhaul, and a structural-sharing rewrite cutting full-Init verification from 1h20m to 11m28s — the sovereign theorem-proving layer for the COOLJAPAN ecosystem.
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.
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.
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.