◉ COOLJAPAN
← All posts
July 19, 2026 • 8 min read

OxiZ 0.2.4 Released — A 19-Agent Production-Readiness Audit, Five Fix Waves, and Python String/FP/Quantifier Bindings

OxiZ is a high-performance SMT solver in pure Rust — a Z3 replacement. 0.2.4 lands the results of a 19-agent production-readiness audit and five fix waves — real Sturm sequences, sound SAT conflict analysis, honest Cooper QE, corrected BV division — plus new oxiz-py string, floating-point, and quantifier bindings, with 7,666 tests passing workspace-wide.

release oxiz smt-solver z3 formal-verification audit pure-rust

An SMT solver that quietly returns the wrong answer is worse than one that crashes.

Today we released OxiZ 0.2.4 — the release where we stopped trusting our own test suite and went looking for exactly that failure mode. Starting July 16, a 19-agent deep-audit pass swept every crate, cross-referencing the upstream Z3 source for expected semantics, then five follow-on fix waves worked the findings crate-by-crate.

No C. No C++. No Fortran. OxiZ reimplements Z3 entirely in Rust, and it owes the C++ SMT/SAT world nothing at link time. The whole decision procedure — SAT core, theory combination, quantifier instantiation, optimization, proofs — is memory-safe Rust you can audit end to end. This release is proof of exactly that: we audited it, ourselves, hard.

Why OxiZ 0.2.4 is a game changer

A 20-year-old solver like Z3 has had two decades of users hitting its edge cases. A young pure-Rust solver has not — which means silent wrong answers can hide in plain sight until an audit goes looking:

0.2.4 ends all of that. The baseline going in was already clean — cargo check, cargo clippy -D warnings, and 6,826 --all-features tests all green — which is exactly the point: every finding below is a real behavioral gap the existing suite didn’t exercise, not a regression. Initial triage: 20 confirmed-critical (P0), 30 confirmed-major (P1), plus a much larger sampled P2–P4 backlog. Re-verification at release time confirms 17/20 P0 and 28/30 P1 items fixed with a real code change — the remainder are called out honestly as still-open in TODO.md, not claimed fixed.

Alongside the audit, oxiz-py picked up real feature work: string, floating-point, and quantifier theory bindings.

Technical Deep Dive: where the soundness lives

SMT-LIB parser & core AST (oxiz-core). (div a b)/(mod a b) now route to mk_div/mk_mod instead of silently parsing as subtraction; indexed BV ops (zero_extend, sign_extend, rotate_left/right, repeat) get real constructors instead of degrading to Bool-sorted uninterpreted applies; undeclared symbols are now a hard ParseError instead of a fabricated fresh Bool variable. TermManager::substitute now handles every TermKind (previously several term kinds passed through unchanged) and hash-conses on (TermKind, SortId) so same-named variables of different sorts can no longer alias. Cooper’s method and the omega test in qe/arith/ are now real eliminations — boundary/minus-infinity case splits, divisibility periods, real gap/threshold computations — instead of stubs.

SAT & NLSAT (oxiz-sat, oxiz-nlsat). Conflict analysis (solver/conflict.rs) now resolves reason-clause literals by value instead of assuming index 0, fixing unsound backtracking that on-the-fly theory clauses could trigger; clause-slot reuse via the free list was removed to stop stale watchers from driving bogus unit propagations. PortfolioSolver workers now clone the real problem via snapshot_problem instead of solving nothing; Sturm-sequence root counts are now correct under a sign-normalized divisor (mirrored in oxiz-math); root isolation bisects with exact rationals instead of merging roots within a 1e-6 window.

Theories (oxiz-theories). LIA now runs real branch-and-bound after the LP relaxation instead of reporting Sat on a fractional assignment; LIA cuts are real Gomory/GMI cuts derived from the tableau row. BV division/remainder (bv/solver/division.rs) compute the quotient product at double width with a non-wrapping adder, closing the wraparound that admitted spurious quotients; the barrel shifters (bv/solver/shifts.rs) now explicitly detect over-shift. assert_fp_lt/assert_fp_le encode real IEEE-754 ordering with NaN handling instead of an ad hoc sign-only check.

Proof, Spacer, and Optimization (oxiz-proof, oxiz-spacer, oxiz-opt). Proof-rule validators now recompute and compare the expected result instead of unconditionally returning Valid; Craig interpolation colors axioms against the caller’s real A/B partition (new oxiz-proof::premise API) instead of coloring everything A. Spacer’s is_init_reachable and predecessor-finding issue real SMT queries instead of stub placeholders, so Unsafe is reachable again. MaxSAT’s weighted-to-unweighted reduction is now textbook-exact instead of ignoring weights.

Getting Started

Add OxiZ to your project:

cargo add oxiz

Try the new Python bindings for strings, floats, and quantifiers:

from oxiz import Solver, StringVal, Concat, Length, ForAll, FPSort, FPVal, fp_add

s = Solver()
s.add(Length(Concat(StringVal("smt"), StringVal("solver"))) == 9)
print(s.check())  # sat

Feature flags layer in the heavier machinery: nlsat for nonlinear arithmetic, optimization for MaxSMT/OMT, spacer for CHC model checking, proof for DRAT/Alethe/LFSC export. Use full to enable everything.

What’s New in 0.2.4

Added

Changed / Fixed

Known remaining gaps (honestly not fixed this release — tracked in TODO.md): oxiz-nlsat’s root isolation still misses irrational discriminants in a few paths; one disjunctive-input backtrack still risks an infinite loop; NiaSolver::floor_ceil still truncates toward zero instead of computing a true floor/ceil. The stricter undeclared-symbol parser check also surfaced two honest new parse errors (to_fp rounding-mode arguments, re.allchar) that regress QF_FP/QF_S on the quickstart Z3-parity suite from 100% — see README.md’s updated parity table.

Confirmed at release time: 7,507/7,507 tests passing with default features, 7,666/7,666 with --all-features (up from the 6,826-test baseline recorded at audit start), plus 107 doc-tests across all 17 crates — clippy -D warnings and rustdoc -D warnings both clean.

Tips

This is the foundation

OxiZ is the formal-reasoning backbone of the COOLJAPAN ecosystem. OxiLean uses it as its SMT proof backend; OxiRS leans on it for validation; Legalis-RS uses it for legal formal verification, and OxigenAI builds on Legalis-RS and OxiZ together. OxiCAD, OxiCar, OxiEDA, OxiAutoRS, OxiMed, and OxiQuant all depend on oxiz-core/oxiz-solver/oxiz-proof for constraint solving. Underneath, OxiZ relies on pure-Rust OxiARC for compression. The whole stack is C/C++/Fortran-free — sovereign from the SAT core all the way up to the application.

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

Star the repo if you want an SMT solver that tells you when it doesn’t know, rather than confidently telling you the wrong thing.

Pure Rust formal reasoning is here — audited, honest, and sovereign.

— KitaSan at COOLJAPAN OÜ July 19, 2026

↑ Back to all posts