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

OxiZ 0.3.0 Released — Ground-String Solving, a Sound FP Model Finder, and 0 Wrong Answers on 154 Decisive Z3 Comparisons

OxiZ 0.3.0 is a hardening-and-capability wave: a new ground string decision procedure and concrete floating-point model finder lift qf_s and qf_fp from partial to 10/10 on the Z3 parity suite, MBQI SAT certification advances three quantified logics, and a dozen soundness bugs are fixed — 8,119 tests passing, 0 Wrong verdicts across 154 decisive Z3 comparisons. Pure Rust, Apache-2.0.

release oxiz smt-solver z3 formal-verification pure-rust floating-point webassembly

A division routine that silently returns 0.0 instead of the right answer is worse than one that panics — the panic gets noticed.

Today we released OxiZ 0.3.0 — a large hardening-and-capability wave built directly on 0.2.4’s production-readiness audit. Confirmed at release time: 8,119 tests passing, 8 skipped, plus 106 doc-tests, all --all-features, clippy/rustdoc -D warnings clean.

No C. No C++. No Fortran. OxiZ reimplements Z3 entirely in Rust — the SAT core, theory solvers, quantifier instantiation, optimization, and proof system are all memory-safe Rust you can read end to end. 0.3.0 keeps auditing that Rust against itself: this release’s soundness fixes came from the same adversarial mindset as 0.2.4’s, turned on the code 0.2.4 shipped.

Why OxiZ 0.3.0 is a game changer

The 0.2.4 audit closed a first wave of silent-wrong-answer bugs. Going deeper into the same crates surfaced a second wave — smaller in scope, just as dangerous:

0.3.0 ends all of that — plus it adds real decision procedures where OxiZ used to fall through to Unknown. The results, re-measured against a real z3 4.15.4 binary on bench/z3_parity:

This is not a “100% parity” claim — three quantified logics (AUFLIA, UFLIA, UFLRA) still have honest Unknown/Timeout gaps. Every gap is disclosed in TODO.md, never silently rounded up.

Technical Deep Dive: where the new decision procedures live

Ground string solving (oxiz-theories/src/string/ground_solver.rs). Gathers a formula’s string constraints, builds a candidate model via definitional propagation and concat-splitting by known operand lengths, then runs a per-variable regular-constraint intersection search reusing the existing Brzozowski-derivative automaton engine. Crucially, it verifies the candidate by concretely evaluating every assertion before it is ever allowed to return Sat — it can only add newly-verified Sat answers, never mask a genuine Unsat.

Concrete FP model finder (oxiz-solver/src/solver/check_fp_model.rs). Pins every FP-sorted term to a bit-exact IEEE-754 value: definitional-equality propagation for variables, the bit-exact engine for operations, predicate-driven witness synthesis for free NaN/Infinity-typed variables. Reports Sat only after verifying every assertion — honest Unknown otherwise, since there’s no complete FP theory in the CDCL(T) core.

MBQI SAT certification. A real completeness certifier for quantified-logic verdicts, built from bounded-box enumeration over finite-interval Int variables, essentially-uninterpreted range-bound detection, and monotone-guard analysis — the difference between “we didn’t find a counterexample” and “we can prove none exists.”

Simplex/ArithSolver hardening. A new ensure_var(idx) chokepoint routes every per-variable-array write through one place that grows assignment/lower/upper/basic in lockstep, so a stale or out-of-range index can neither be silently dropped nor panic. pop() now drains var_to_term’s tail and removes each drained term from term_to_var in lockstep, an O(delta) trail-based undo that closes the recycled-VarId bug above.

Getting Started

Add OxiZ to your project:

cargo add oxiz

Try the new (get-consequences ...) SMT-LIB command — it extracts the unit consequences over queried variables entailed by the current assertions plus a set of assumptions:

use oxiz_solver::Context;

let mut ctx = Context::new();
let output = ctx.execute_script(r#"
    (set-logic QF_UF)
    (declare-const a Bool)
    (declare-const b Bool)
    (declare-const c Bool)
    (assert (=> a b))
    (assert (=> b c))
    (get-consequences (a) (b c))
"#).expect("script should parse and run");

assert_eq!(output[0], "sat");
// output[1] reports both (=> a b) and (=> a c) as consequences of assuming `a`

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.3.0

Added

Fixed

Full itemized detail, crate by crate, is in the CHANGELOG.

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 22, 2026

↑ Back to all posts