14 posts
OxiZ is a high-performance SMT solver in pure Rust — a Z3 replacement. 0.2.3 lands sound incremental BV & Simplex solving, a full term-level MaxSMT/OMT optimization pipeline, real BMC and k-induction model checking, and generic in-memory DRAT/LRAT proof writers — with 6,826 tests passing and 100% Z3 parity.
OxiZ is a pure-Rust SMT solver reimplementing Z3. 0.2.2 ships real LBD clause scoring (replacing the old stub), Big-M primal simplex for LP, an LRU lemma cache, ML conflict-hook branching, and deeper Z3-compat APIs — all with 100% Z3 parity and zero C/C++/Fortran.
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.
OxiZ is a pure-Rust SMT solver and Z3 replacement. 0.2.1 sharpens the EUF (congruence-closure) hot path: reusable allocation buffers, O(k) incremental pop() via a sig_table/fingerprint_table trail, cache-friendly ENode layout, and new production EUF criterion benchmarks. 100% Z3 parity, still pure Rust.
OxiZ 0.2.0 ships an ergonomic EasySolver builder, no_std support for bare-metal/zkVM (RISC-V), a Pure-Rust ML heuristics crate (oxiz-ml), Skolemization, a modular WASM js_api, and 100% Z3 parity across 88 benchmarks. Zero C/C++.
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.
A complete, high-performance Satisfiability Modulo Theories solver written entirely in Rust. Full CDCL(T) architecture, comprehensive theory support, proof generation, and Z3-level performance — with zero C/C++ dependencies and full memory safety.
OxiZ 0.1.2 adds PyO3 Python bindings (oxiz-py), a Pure-Rust BLAS + multi-precision (MPFR-style) math layer, an SMT-COMP benchmark suite, and a vastly expanded CLI (dashboard/server/distributed/TPTP/interpolation). A Pure Rust Z3 replacement with zero C/C++.
Legalis-RS 0.1.2 replaces the C++ Z3 backend in its legal verifier with OxiZ, the Pure-Rust SMT solver — rigorous proofs with no native toolchain. Plus a zero-warning build across 25 crates and 11,365 passing tests.
OxiZ is a Pure Rust Satisfiability Modulo Theories solver reimplementing Z3 — a full CDCL(T) architecture with EUF/LRA/LIA/BV/Arrays/Strings/FP/Datatypes theories, SMT-LIB2 support, and roughly 90% Z3 feature parity, all with zero C/C++. This is its first public release.
OxiZ 0.1.1 ships a new unified `oxiz` meta-crate with feature-flagged modular usage (solver/nlsat/optimization/spacer/proof/full), plus MBQI and CDCL(T) theory-propagation fixes. A Pure Rust Z3 replacement with zero C/C++.
Legalis-RS 0.1.1 adds United Kingdom and Singapore jurisdictions to the Pure Rust legal-DX framework and grows the test suite from 6,100+ to 9,568 across 23 crates, with a near-zero-warning quality pass.
Legalis-RS is a Pure Rust framework that turns legal statutes into structured, machine-verifiable code — a Legal DSL parser, formal verifier, population simulator, and multi-jurisdiction support (JP/DE/FR/US). An honest first release.