◉ COOLJAPAN
← All posts
January 12, 2026 • 6 min read

OxiZ 0.1.1 Released — A Unified `oxiz` Meta-Crate for the Pure Rust SMT Solver

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

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

The Pure Rust SMT solver just got a single, ergonomic front door — one dependency, capabilities on demand.

Today we released OxiZ 0.1.1 — a same-day usability patch that introduces the unified oxiz meta-crate (add one dependency, turn features on with flags) and lands real correctness fixes in quantifier instantiation and theory propagation.

No C. No Fortran. No FFI. For roughly fifteen years, Z3 (C++) has been the de-facto SMT standard, and for good reason — but it brings a C++ toolchain and an FFI boundary along with it. OxiZ is the Pure Rust alternative: it compiles to a single static binary (or WASM), it is memory-safe by construction, and every line of the solver is auditable Rust. No linking against a foreign object you can’t read.

Why 0.1.1 matters

The day after a big debut, the most-requested thing is almost never a new theory — it’s an ergonomic way in. OxiZ 0.1.0 shipped eleven crates: a CDCL SAT core, a theory layer, a DPLL(T) solver, proof generation, and more. Powerful, but wiring up around eleven separate dependencies by hand is friction.

0.1.1 fixes exactly that. The new oxiz meta-crate means you add one dependency and switch capabilities on with Cargo feature flags. Want just a solver? That’s the default. Need nonlinear arithmetic, optimization, or a CHC engine? Flip a flag. No version-juggling across a constellation of sub-crates.

It is also more than packaging. 0.1.1 lands genuine correctness fixes — Model-Based Quantifier Instantiation comparison handlers, CDCL(T) theory propagation, and basic bitvector support — so formulas that previously stumbled now solve.

The numbers behind it (from the 0.1.1 README/CHANGELOG): roughly 90–92% Z3 feature parity, about 173,500 lines of Rust, 3,670 tests, with 84/84 solver tests passing for this fix release. It was also verified against the Legalis formal-verification framework — 467/467 tests passing.

Technical Deep Dive

The meta-crate feature map. The oxiz crate is a thin, well-documented umbrella over the workspace. The feature surface (straight from its Cargo.toml):

The CDCL(T) stack it wraps. Under the umbrella, the architecture is unchanged and battle-tested:

The fixes. See What’s New below for the full list — the headline trio is MBQI comparison evaluation, correct incremental backtracking in the arithmetic theory, and bounded-integer bitvector comparisons.

Getting Started

Install is one line:

cargo add oxiz

Pick exactly the capabilities you want with feature flags:

[dependencies]
oxiz = "0.1.1"                                            # default: solver
# oxiz = { version = "0.1.1", features = ["nlsat", "optimization"] }
# oxiz = { version = "0.1.1", features = ["full"] }

A minimal, copy-pasteable example using the 0.1.1 builder API — solve x + y = 10 with x > 5:

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

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

    // x + y = 10, with x > 5
    let x = tm.mk_var("x", tm.sorts.int_sort);
    let y = tm.mk_var("y", tm.sorts.int_sort);
    let sum = tm.mk_add([x, y]);
    let ten = tm.mk_int(BigInt::from(10));
    let eq = tm.mk_eq(sum, ten);
    let five = tm.mk_int(BigInt::from(5));
    let gt = tm.mk_gt(x, five);

    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"),
    }
}

Prefer to feed raw SMT-LIB2? That path is still here: oxiz::solver::Context together with execute_script will run a standard SMT-LIB script for you.

What’s New in 0.1.1

Added

Changed

Fixed

Compatibility

Tips

This is the foundation

Even at 0.1.1, OxiZ is already doing real work: it was verified with the Legalis formal-verification framework, passing all 467/467 tests — early evidence that a Pure Rust SMT solver can underpin serious verification, not just toy benchmarks. As the broader Pure Rust ecosystem grows, a fast, auditable, FFI-free SMT solver is the kind of bedrock everything else can stand on.

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

Star the repo if a Pure Rust Z3 replacement is something you’ve been waiting for — it genuinely helps.

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

— KitaSan at COOLJAPAN OÜ January 12, 2026

↑ Back to all posts