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

OxiZ 0.1.0 Released — A Pure Rust SMT Solver, the First Step Toward Replacing Z3

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.

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

Formal reasoning, the foundation under verification and program synthesis, no longer has to be written in C++.

Today we released OxiZ 0.1.0 — a Pure Rust Satisfiability Modulo Theories (SMT) solver that reimplements the Z3 architecture from the SAT core up, and the first concrete step toward a sovereign, auditable replacement for Z3.

No C. No Fortran. No FFI. For roughly fifteen years, Z3 — written in C++ — has been the de-facto standard SMT solver, the engine quietly sitting under a huge fraction of the world’s formal verification, symbolic execution, and program-synthesis tooling. OxiZ is written entirely in safe Rust. It compiles to a single static binary (or to WASM), it is memory-safe by construction, and every line of it is auditable. There is no opaque native library to trust, no separate toolchain to build, and no segfault waiting in a corner of a decade-old C++ codebase.

Why 0.1.0 matters

Z3 is genuinely excellent, and we want to be clear about that. But it is also a large C++ project, which brings the familiar costs: memory-safety bugs, a heavy build, and a broad attack surface — costs that matter all the more because SMT solvers sit at the bottom of the trust stack. They underpin formal verification, program synthesis, AI-safety reasoning, and hardware design. When the engine you use to prove things correct can itself crash or be exploited, that is not a small problem.

OxiZ 0.1.0 is our answer, and it starts from a deliberately honest position. This first release reaches roughly 90–92% Z3 feature parity in about 25% of the codebase size — around 173,500 lines of Rust, 3,670 tests, organized into 11 crates. That is a first release, not a finished one: there are rough edges and known gaps (listed below). But it is already a real solver that handles real problems, not a toy.

Technical Deep Dive: The CDCL(T) Architecture in Pure Rust

OxiZ is a faithful CDCL(T) solver — a CDCL SAT core driving a set of cooperating theory solvers — laid out across focused crates:

Getting Started

Add the solver crate:

cargo add oxiz-solver

A minimal, copy-pasteable example — drive the solver with an SMT-LIB2 script straight from Rust:

use oxiz_solver::Context;

fn main() {
    let mut ctx = Context::new();

    let results = ctx.execute_script(r#"
        (set-logic QF_LIA)
        (declare-const x Int)
        (declare-const y Int)
        (assert (> x 0))
        (assert (< y 10))
        (assert (= (+ x y) 15))
        (check-sat)
        (get-model)
    "#).unwrap();

    for result in results {
        println!("{}", result);
    }
}

You can also reach for the CLI, which solves SMT-LIB2 files directly and ships an interactive REPL:

cargo run --release -p oxiz-cli -- input.smt2     # solve a file
cargo run --release -p oxiz-cli -- --interactive  # REPL

What’s inside

Everything in this first release, in plain terms:

And, just as honestly, the known limitations in 0.1.0:

These are on the roadmap, not hidden.

Tips

A few concrete ways to get more out of 0.1.0:

This is the foundation

OxiZ gives the young Pure-Rust ecosystem something it did not have before: a native, auditable formal-reasoning engine, with no C++ underneath. It is built for exactly the places where correctness is the whole point — formal verification, legal-tech reasoning, and program analysis — and it has already been exercised against the Legalis formal verification framework. This is a first release, so we are keeping our claims modest, but the direction is clear.

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

Star the repo if a memory-safe, single-binary SMT solver is something you’ve been waiting for — it genuinely helps us gauge where to push next.

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

— KitaSan at COOLJAPAN OÜ January 12, 2026

↑ Back to all posts