◉ COOLJAPAN
← All posts
April 26, 2026 • 7 min read

OxiZ 0.2.1 Released — Faster Congruence Closure, Where Every SMT Query Lives

OxiZ is a pure-Rust SMT solver and Z3 replacement. 0.2.1 sharpens the EUF (congruence-closure) hot path: reusable allocation buffers, O(k) incremental pop() via a sig_table/fingerprint_table trail, cache-friendly ENode layout, and new production EUF criterion benchmarks. 100% Z3 parity, still pure Rust.

release oxiz smt-solver formal-verification pure-rust z3 congruence-closure

The fastest part of an SMT solver should be the part it touches the most.

Today we released OxiZ 0.2.1 — a focused performance release that tightens the EUF congruence-closure engine, the equality reasoning core that every single SMT query passes through.

No C. No C++. No Fortran. OxiZ is a complete reimplementation of Z3 in Pure Rust — the AST, the SMT-LIB parser, CDCL SAT, nonlinear arithmetic, the theory solvers, and the proof machinery, all the way down. Where the C++ SMT world hands you a 20MB shared object and a CMake build that fights your toolchain, OxiZ compiles to a single static binary or a sub-2MB WASM module. Nothing to link. Nothing to chase. No undefined behavior lurking under your verifier.

Why OxiZ 0.2.1 matters

Z3 is brilliant, and Z3 is also a large C++ codebase. That means the usual C++ tax: memory bugs that surface as crashes in your CI, a heavy build that you cache and pray over, and a WASM bundle around 20MB that’s a non-starter for the browser. When your verifier is a black box you can’t audit and can’t trust to be memory-safe, the whole reasoning stack inherits that risk.

OxiZ 0.2.1 spends its effort exactly where it pays off: congruence closure. Every theory combination in CDCL(T) leans on the E-graph to decide which terms are equal, so even a small per-call saving compounds across millions of equality checks. This release delivers:

Congruence closure is the hot path. Making it leaner makes everything above it — arithmetic, bit-vectors, arrays, strings, quantifiers — faster too.

Technical Deep Dive: how the equality core sits in the stack

OxiZ is 408,320 lines of production Rust across 17 crates, built on Rust Edition 2024 (Rust 1.85+), with 6,415 tests passing at a 100% pass rate and 100% Z3 parity across 88 benchmarks (8/8 logics at 100%: QF_LIA 16/16, QF_LRA 16/16, QF_NIA 1/1, QF_S 10/10, QF_BV 15/15, QF_FP 10/10, QF_DT 10/10, QF_A 10/10). Here is where 0.2.1’s work lands.

Layer 1 — oxiz-sat: the CDCL core. A modern conflict-driven clause-learning SAT engine with VSIDS, LRB, VMTF, and CHB decision heuristics, two-watched-literal propagation, and DRAT proof logging. This is the propositional skeleton that the theory solvers extend.

Layer 2 — oxiz-theories: where EUF lives. This crate houses the theory solvers — EUF, LRA, LIA, BV, Arrays, Strings, FP, and Datatypes. The 0.2.1 optimizations target the EUF (congruence-closure) solver here: the reusable buffers, the incremental sig_table/fingerprint_table trail, the ENode re-layout, and the allocation-free explain_equality all live in this layer. Because the other theories combine through equality, sharpening EUF lifts the whole crate.

Layer 3 — oxiz-solver: CDCL(T) orchestration. The orchestrator that drives SAT and the theories together, including MBQI (Model-Based Quantifier Instantiation) for quantified formulas. Every theory propagation and every equality query it issues now hits the leaner EUF path.

Layer 4 — oxiz-proof: certificates you can check. Proof production with DRAT, Alethe, and LFSC, plus export to Coq, Lean, and Isabelle. The allocation-free explain_equality improvements feed directly into faster proof generation on equality reasoning.

Around these sit oxiz-core (AST, sorts, the SMT-LIB parser, tactics, rewriters), oxiz-math (polynomials, matrices, LP), oxiz-nlsat (CAD and algebraic numbers), oxiz-opt (MaxSAT/OMT), oxiz-spacer (CHC solving via PDR/IC3 and BMC), plus oxiz-wasm, oxiz-cli, oxiz-smtcomp, oxiz-ml (neural-net-guided heuristics), and oxiz-py.

Getting Started

Add OxiZ with a single command — the default solver feature is all you need to start:

cargo add oxiz

Here’s a minimal, copy-pasteable example using the SMT-LIB script API:

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);
    }
}

Feature flags nlsat, optimization, proof, and full unlock nonlinear arithmetic, MaxSMT/OMT, and proof export to Coq/Lean/Isabelle when you need them.

What’s New in 0.2.1

Performance

Added

Fixed

This release builds on 0.2.0 (2026-04-04), which refactored the solver, SAT, NLSAT, and optimization modules into subdirectories and added Skolemization plus no_std improvements.

Tips

This is the foundation

As of late April 2026, OxiZ is already the equality-and-arithmetic engine under a growing slice of the COOLJAPAN ecosystem. OxiLean, our Lean-4-style theorem prover, uses OxiZ as its SMT proof backend. OxiRS, our Semantic Web and SPARQL stack, uses it for validation. Legalis-RS leans on it for legal formal verification. And OxiZ itself is built on pure-Rust OxiARC (via oxiarc-deflate and oxiarc-brotli) for compression — alongside ecosystem siblings like OxiBLAS, Oxicode, and OxiFFT. Every layer is Rust, end to end.

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

Star the repo if you want a memory-safe SMT solver you can audit, bundle, and ship anywhere Rust runs.

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

— KitaSan at COOLJAPAN OÜ April 26, 2026

↑ Back to all posts