◉ COOLJAPAN
← All posts
January 21, 2026 • 7 min read

OxiZ 0.1.2 Released — Python Bindings, a Native Math Stack, and SMT-COMP Tooling for the Pure Rust SMT Solver

OxiZ 0.1.2 adds PyO3 Python bindings (oxiz-py), a Pure-Rust BLAS + multi-precision (MPFR-style) math layer, an SMT-COMP benchmark suite, and a vastly expanded CLI (dashboard/server/distributed/TPTP/interpolation). A Pure Rust Z3 replacement with zero C/C++.

release oxiz smt-solver formal-verification pure-rust z3 python smt-comp

A real SMT solver in Python — no C toolchain, reproducible SMT-COMP benchmarks, and a hard-algebra math stack that is still 100% Pure Rust.

Today we released OxiZ 0.1.2 — an incremental release that gives the Pure Rust SMT solver first-class Python bindings, a self-contained native numeric stack, and the SMT-COMP-style tooling needed to make performance claims reproducible.

No C. No Fortran. No FFI.

Z3 is the de-facto standard for SMT solving, and it is a C++ project — a remarkable one, but one that ties you to a C/C++ toolchain, system libraries, and the long tail of build and supply-chain concerns that come with native code. OxiZ takes the opposite stance: every line is Rust.

The notable thing about 0.1.2 is that even the hard parts stay Pure Rust. The new math layer — Level 1/2/3 BLAS and MPFR-style arbitrary-precision arithmetic — links against no OpenBLAS, no GMP, and no MPFR C libraries. The exact algebra that historically forces projects to reach for battle-tested C numeric stacks is implemented natively here. The result compiles to a single static binary (or to WASM), is memory-safe by construction, and is auditable end to end: you can read every routine your solver actually runs.

Why 0.1.2 matters

This release is about reach and rigor.

The numbers behind this release: ~240,000 Rust LOC (up from ~173,500), 3,823 tests passing (100%), 13 crates, and roughly 90–92% Z3 parity. Still an early version, and honest about it — but a substantial one.

Technical Deep Dive

The new surface area in 0.1.2 lives in real, shipping crates and modules:

Getting Started

Both Rust and Python are first-class in 0.1.2.

Rust install:

cargo add oxiz

Python install (via maturin):

pip install maturin
cd oxiz-py && maturin develop --release

A minimal Python example using the real oxiz-py API:

import oxiz

tm = oxiz.TermManager()
solver = oxiz.Solver()

# integer variables
x = tm.mk_var("x", "Int")
y = tm.mk_var("y", "Int")

# constraints: x + y = 10, x > 5
ten = tm.mk_int(10)
five = tm.mk_int(5)
sum_xy = tm.mk_add([x, y])
solver.assert_term(tm.mk_eq(sum_xy, ten), tm)
solver.assert_term(tm.mk_gt(x, five), tm)

result = solver.check_sat(tm)
print(f"Result: {result}")  # sat

if result == oxiz.SolverResult.Sat:
    model = solver.get_model(tm)
    print(f"x = {model['x']}, y = {model['y']}")

What’s New in 0.1.2

Added

Fixed

Changed

Tips

This is the foundation

OxiZ is meant to be the native, auditable formal-reasoning engine for the Pure Rust ecosystem — the kind of solver that verification, program-analysis, and legal-tech tools build on. It has already been used to verify the Legalis framework. A memory-safe SMT core you can read, ship as one static binary, and run anywhere Rust runs is a different kind of building block than a C++ dependency you treat as a black box.

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

Star the repo if a Pure Rust SMT solver — in Rust and now in Python — is the kind of foundation you want to build on.

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

— KitaSan at COOLJAPAN OÜ January 21, 2026

↑ Back to all posts