OxiZ 0.2.3 Released — Sound Incremental Solving, Real Algorithms, and In-Memory Proofs

Correctness is not a feature you bolt on later — it is the floor you build on.

Today we released OxiZ 0.2.3 — a soundness-focused release that replaces stub logic with real algorithms across nonlinear arithmetic, optimization, theories, and model checking, while fixing subtle soundness bugs in incremental bit-vector and Simplex solving.

No C. No C++. No Fortran. OxiZ reimplements the world’s most-used SMT solver — Z3 — entirely in Rust, and it owes the C++ SMT/SAT world nothing at link time. Where Z3 drags a sprawling native toolchain and a ~20MB WASM payload behind it, OxiZ ships as a single static binary or a sub-2MB WebAssembly bundle. The whole decision procedure — SAT core, theory combination, quantifier instantiation, optimization, proofs — is memory-safe Rust you can audit end to end.

Why OxiZ 0.2.3 is a game changer

Z3 is the gold standard, and it is also a black box: a 20-year-old C++ codebase where an incremental push/pop soundness bug is somebody else’s segfault to chase. Worse, when you reach for a solver in an automated pipeline, you don’t just want an answer — you want the right answer, every time, including the awkward incremental cases where you assert, check, backtrack, and check again.

0.2.3 is about exactly that. This release is a correctness pass, not a feature-count pass:

• Incremental bit-vector solving is now sound. Previously, a satisfying assignment from one incremental check() probe could persist on the trail and contradict the next probe’s constants, producing a false UNSAT. We now roll back the committed trail and forget the learned clauses after every SAT probe, so search residue can no longer poison the next query. And get_value now reads from a stable last_sat_model snapshot, so model readback after backtracking is no longer all-zero.
• Simplex push/pop is correct by construction. Simplex::push now saves a full tableau snapshot, so pivots that happen during a check() inside a pushed scope are correctly undone on pop(). No more tableau corruption after in-scope pivots.
• Nelson-Oppen equality propagation is sound. Equalities x = y are encoded straight into the Simplex tableau as x - y <= 0 and y - x <= 0, and shared equalities are derived by a probe-and-pop procedure that only emits x = y when both x < y and x > y are infeasible.
• A full term-level MaxSMT/OMT pipeline. OptContext::check_sat now makes a real oxiz_solver::Solver call (it used to always return Unknown). MaxSMT uses a binary-search selector-variable encoding; single-objective and Pareto optimization delegate to the real Optimizer. The stubs that quietly returned Unknown are gone.
• Real BMC and sound k-induction. oxiz-spacer now builds Init(s0) ∧ ⋀ Trans(si, si+1) ∧ Bad(sk) and only reports Unsafe when that is genuinely SAT, runs a sound k-induction procedure across depths, and extracts concrete counterexamples via eval_in_model.
• Nonlinear arithmetic that actually finds roots. oxiz-nlsat now solves degree ≥ 3 polynomials through a complete rational-root-theorem search (replacing a stub that returned the empty set) and computes real resultants and leading coefficients instead of returning zero.

The correctness floor under all of this: 6,826 tests passing (100% pass rate) and 100% Z3 parity across 88 benchmarks (88/88), with all eight logics at 100%.

Technical Deep Dive: where the soundness lives

OxiZ is 17 crates of pure Rust. The 0.2.3 work concentrates in four of them.

oxiz-theories — sound theory solving. This is the heart of the release. Incremental BV solving is made sound by trail rollback: check() captures committed_trail and learned_before, then after each SAT probe calls restore_to_trail_size and forget_learned_since to discard search residue. BvSolver::get_value reads its result from the last_sat_model snapshot so post-backtrack readback is stable, and assert_uge rounds out the unsigned comparison set. Simplex gets snapshot-based push/pop so the tableau survives in-scope pivots, plus a new simplex_opt.rs primal optimization phase: Simplex::optimize_linexpr implements Bland’s rule and returns a SimplexOptStatus (Optimal/Unbounded/Infeasible/Unknown), which LraOptimizer::optimize_min now actually calls instead of returning zero. Nelson-Oppen combination encodes x = y as x - y <= 0 ∧ y - x <= 0 and uses model-based probe-and-pop to derive only the shared equalities that are truly entailed.

oxiz-opt — optimization that optimizes. The MaxSMT path allocates a fresh boolean selector and cost variable per soft constraint, adds the b_i → t_i implications, encodes the total cost with ite, and binary-searches the cost budget. Single-objective optimization delegates to Optimizer::optimize; Pareto search to Optimizer::pareto_optimize. New OptResult::Unbounded plus pareto_front() and config() accessors round out the surface. On the solver side, the Optimizer got a convergence guard: integer and real objective loops now break immediately when model evaluation yields no concrete value, so abstract terms can no longer spin the search forever.

oxiz-spacer — model checking with real witnesses. Bmc::check_bad_at_depth constructs the standard bounded-model-checking formula and calls check_sat, reporting Unsafe only on SAT. check_kinduction is a sound k-induction procedure, run_kinduction loops depth 1..max_depth, and extract_model uses the solver’s new eval_in_model to produce concrete counterexample traces.

oxiz-sat — generic, in-memory proofs. The DRAT/LRAT proof writers are now generic over any W: Write + Send. DratWriter<W> and LratWriter<W> replace the old DratProof/LratProof types that were hard-coded to BufWriter<File>; new with_writer(w) and enable_writer(&mut self, w) let you capture proofs straight into a Cursor<Vec<u8>> for in-memory inspection, and Default impls stay specialized on BufWriter<File> so existing file-based call sites compile unchanged.

Getting Started

Add OxiZ to your project:

cargo add oxiz

A minimal solve with the builder API:

use oxiz::{Solver, TermManager, SolverResult};
use num_bigint::BigInt;

let mut solver = Solver::new();
let mut tm = TermManager::new();

// Create variables
let x = tm.mk_var("x", tm.sorts.int_sort);
let y = tm.mk_var("y", tm.sorts.int_sort);

// x + y = 10
let sum = tm.mk_add([x, y]);
let ten = tm.mk_int(BigInt::from(10));
let eq = tm.mk_eq(sum, ten);

// x > 5
let five = tm.mk_int(BigInt::from(5));
let gt = tm.mk_gt(x, five);

// Assert and solve
solver.assert(eq, &mut tm);
solver.assert(gt, &mut tm);

match solver.check(&mut tm) {
    SolverResult::Sat => println!("SAT"),
    SolverResult::Unsat => println!("UNSAT"),
    SolverResult::Unknown => println!("Unknown"),
}

If you prefer SMT-LIB2, the script API is available too via Context::execute_script. Feature flags layer in the heavy machinery: nlsat unlocks nonlinear arithmetic, optimization enables MaxSMT/OMT, spacer brings CHC solving and model checking, and proof turns on proof export (DRAT/Alethe/LFSC, with export to Coq/Lean/Isabelle). Use full to enable everything.

What’s New in 0.2.3

Added

• oxiz-sat: Generic proof writers. DratWriter<W> / LratWriter<W> are now generic over any W: Write + Send; with_writer(w) / enable_writer(&mut self, w) enable in-memory proof capture (e.g. Cursor<Vec<u8>>).
• oxiz-solver/oxiz-theories: BvMul constant-shift optimization. bv_shl_const encodes a << shift directly from source bits; bvmul(x, 2^k) is detected and emitted as a shift, cutting clause count for power-of-2 multiplications.
• oxiz-nlsat: Rational root theorem for degree ≥ 3 polynomials, plus proper resultant and leading-coefficient extraction (delegating to Polynomial::resultant and leading_coeff_wrt).
• oxiz-opt: Full term-level optimization pipeline — real solver calls, binary-search MaxSMT selector encoding, single-objective and Pareto optimization, OptResult::Unbounded.
• oxiz-theories: Simplex optimization extension (simplex_opt.rs) with Bland’s rule; snapshot-based push/pop; sound Nelson-Oppen equality propagation; BvSolver soundness and incremental improvements (assert_uge, stable get_value readback, per-probe trail rollback).
• oxiz-solver: Context::eval_in_model — evaluate a term against the current SAT model.
• oxiz-spacer: Real BMC and sound k-induction with concrete counterexample extraction.

Changed

• oxiz-sat: BREAKING — DratProof/LratProof renamed to DratWriter/LratWriter to avoid a name collision with oxiz-proof::DratProof.
• oxiz-solver: Optimizer convergence guard — integer and real objective loops break immediately when model evaluation yields no concrete value, preventing infinite loops on abstract terms.
• Dependency bumps: pure-Rust OxiARC oxiarc-deflate and oxiarc-brotli 0.3.1 → 0.3.3; sysinfo 0.38 → 0.39; rhai 1.24 → 1.25; wide 1.3 → 1.5; lru 0.17 → 0.18; pdf-writer 0.14 → 0.15.

Fixed

• oxiz-sat: hardcoded absolute proof paths replaced with std::env::temp_dir() — all four proof-logger tests now use portable temp paths.
• oxiz-theories: BV incremental soundness — a satisfying assignment from one probe used to persist on the trail and cause false UNSAT; fixed by trail rollback plus forgetting learned clauses after every probe (regression test test_incremental_mul_aux_diseq_then_const_is_sat).
• oxiz-theories: Simplex pop() no longer corrupts the tableau after in-scope pivots — snapshot-based restore is correct by construction.

Tips

• Migration (BREAKING rename). If you named DratProof or LratProof directly, switch to DratWriter / LratWriter. Most call sites that relied on Default keep compiling because Default is specialized on BufWriter<File>; only explicit type references need updating.

• Capture proofs in memory. You no longer have to write proofs to a file. Capture them in a buffer:

  use std::io::Cursor;
  let mut writer = DratWriter::with_writer(Cursor::new(Vec::new()));
  // ... run the solver, then inspect the captured proof bytes
  

• Incremental BV solving — upgrade now. If you do bit-vector solving with push/pop, 0.2.3 fixes the false-UNSAT and all-zero-readback soundness bugs. You can safely reuse one solver across many probes.

• MaxSMT/OMT is real. Enable the optimization feature and use optimize_maxsmt and Pareto optimization; the old Unknown-returning stubs are gone.

• Program verification. oxiz-spacer now does sound BMC and k-induction with concrete counterexamples — enable the spacer feature.

• Nonlinear arithmetic. oxiz-nlsat now handles degree ≥ 3 polynomials via the rational root theorem — enable the nlsat feature.

This is the foundation

OxiZ is the formal-reasoning backbone of the COOLJAPAN ecosystem. OxiLean uses OxiZ as its SMT proof backend; OxiRS leans on it for validation; Legalis-RS uses it for legal formal verification; and OxigenAI — the GovTech legal AI platform — builds on Legalis-RS and OxiZ together. Underneath, OxiZ relies on pure-Rust OxiARC (oxiarc-deflate, oxiarc-brotli) for compression, alongside siblings like OxiBLAS, Oxicode, and OxiFFT. 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 you can trust on the awkward incremental cases — not just the easy ones.

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

— KitaSan at COOLJAPAN OÜ June 9, 2026