OxiZ 0.1.3 Released — Pure Rust SMT Solver Aiming to Replace Z3

A quiet revolution in formal methods and verification.

On February 6 we released OxiZ 0.1.3 — a high-performance Satisfiability Modulo Theories (SMT) solver built 100% in Rust as a pure-Rust reimplementation of Z3.

This is not a wrapper or binding.
This is a ground-up rewrite: 284,414 lines of clean, safe Rust with no C/C++, no FFI, no unsafe code in the kernel, and full SMT-LIB2 compatibility.

The goal is ambitious: deliver Z3-level (or better) performance and features while giving the Rust ecosystem native, auditable, memory-safe formal reasoning capabilities.

Why OxiZ matters

Modern software verification, program synthesis, AI safety, and hardware design all rely on SMT solvers.
Z3 has been the de-facto standard for over 15 years — incredibly powerful, but written in C++ with all the usual risks (memory bugs, complex build system, large attack surface).

OxiZ changes the rules:

• Memory-safe by construction
• Compiles to a tiny static binary or WASM (<2 MB)
• Seamless integration with the Rust ecosystem (cargo, oxilean, oxirs, etc.)
• Proof generation that can be verified in Lean, Coq, or Isabelle

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

OxiZ follows a clean, modular CDCL(T) (Conflict-Driven Clause Learning with Theory) design:

1. SAT Core (oxiz-sat)
   Modern CDCL with two-watched literals, multiple branching heuristics (VSIDS, LRB, VMTF, CHB), clause minimization, preprocessing (BCE, BVE), and full DRAT proof logging.

2. Theory Solvers (oxiz-theories)
   Fully modular and extensible:

   • EUF: Congruence closure
   • LRA / LIA: Simplex + branch-and-bound + cutting planes
   • Bit-Vectors (BV): Bit-blasting + word-level reasoning
   • Arrays: Extensionality and read-over-write
   • Strings: Automata-based solver
   • Floating-Point: Full IEEE 754 semantics
   • Datatypes: ADT with testers and selectors

3. SMT Orchestration Layer (oxiz-solver)
   Theory combination, Model-Based Quantifier Instantiation (MBQI), E-matching, Skolemization, and Destructive Equality Resolution (DER).

4. Proof & Verification (oxiz-proof)
   DRAT, Alethe, LFSC, and export to Coq/Lean/Isabelle — enabling machine-checkable proofs for safety-critical systems.

What’s New in 0.1.3

• 100% Z3 parity on 88 SMT-LIB benchmarks across 8 logics
• All core theory solvers validated against Z3
• Improved nonlinear arithmetic (NLSAT with CAD)
• Production-ready Python bindings (oxiz-py)
• WASM bundle under 2 MB with lazy theory loading
• 5,814 passing tests and full incremental solving (push/pop)

Benchmarks (preliminary SMT-LIB results)

(Optimizations are still ongoing — target is full parity or better by v1.0.)

This is the foundation

OxiZ is now the formal reasoning engine for the entire COOLJAPAN stack:

• oxilean uses OxiZ as its SMT backend for proof automation
• oxirs leverages it for SHACL validation and GraphRAG
• oxictl proves correctness of control laws
• oxiphoton verifies optical device properties
• mielinOS agents get mathematically verified reasoning

Imagine writing #[prove] attributes that the compiler checks using a full SMT solver — all inside pure Rust.

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

Star the repo if you believe formal verification should be as safe and fast as Rust itself.

The “trust me bro” era of verification is ending.
Proof is now native to Rust.

— KitaSan at COOLJAPAN OÜ
February 6, 2026