OxiZ 0.2.0 Released — An Easy API, no_std/zkVM Support, and ML-Guided Heuristics for the Pure Rust SMT Solver

A few-line EasySolver API, a solver that now runs on bare metal and inside zkVMs, ML-guided branching — and still 100% Z3 parity across all 88 benchmarks.

Today we released OxiZ 0.2.0 — a confident, benchmark-forward minor bump that makes the Pure Rust SMT solver easier to reach for, lets its core run where no C++ solver can, and adds a Pure-Rust ML layer to guide its search.

No C. No Fortran. No FFI. Z3 — the de-facto standard SMT solver — is a large C++ codebase, and that choice has always set a hard ceiling on where it can run. OxiZ takes the opposite path, and 0.2.0 is where that choice pays off most visibly. Being Pure Rust is exactly what lets OxiZ compile to a single self-contained static binary, to WebAssembly for the browser, and to no_std bare-metal and zero-knowledge VM targets — places where a C++ solver simply cannot go. It is memory-safe by construction and auditable end to end: no opaque native blob in the trust boundary.

Why OxiZ 0.2.0 is a game changer

The incumbent is excellent at solving — but it is C++. That means it cannot target no_std or zkVM environments, it brings a heavy build and toolchain, and it carries a large native attack surface into anything that links it. For verification that needs to run inside a proof system, in a browser sandbox, or on an embedded controller, that ceiling is a wall.

OxiZ 0.2.0 walks straight through it, with concrete wins:

• EasySolver — a fluent builder so simple problems take a few lines. No manual term plumbing, no sort bookkeeping; declare variables, assert constraints, check.
• no_std / zkVM — the core solver now compiles for bare-metal and zero-knowledge VMs (RISC-V) via default-features = false. You can run real SMT inside a proof system.
• oxiz-ml — a Pure-Rust ML framework to guide branching and heuristics: neural nets, optimizers, and formula feature extraction.
• Skolemization for existential quantifiers.
• WASM js_api overhaul — a modular, TypeScript-friendly browser API with framework wrappers.
• Benchmarks — greatly expanded SMT-LIB coverage, with sustained 100% Z3 parity (88/88, 8/8 logics).

The numbers behind this release are real and measured: 312,495 lines of production Rust, 6,155 tests passing (100%), and 100.0% Z3 parity across 88 benchmarks spanning 8 of 8 core logics. That parity did not arrive by accident — it is the end of a deliberate journey from 64.8% (57/88) → 100% (88/88).

The per-logic breakdown, all at 100%:

Technical Deep Dive

These wins are grounded in real 0.2.0 changes, not slideware.

Easy API (oxiz::easy). The new EasySolver builder is the headline ergonomics story. You set_logic, declare with int_var / real_var / bool_var, and assert with a fluent vocabulary: assert_gt, assert_lt, assert_ge, assert_le, assert_eq_int, assert_eq_vars, assert_neq_vars, assert_true, assert_false, and assert_sum_eq. Resource knobs — timeout, conflict_limit, decision_limit — keep searches bounded. You drive the solve with check_sat / is_sat / is_unsat, then read models back, typed, via get_int_value, get_bool_value, and get_model_value. Incremental work is supported through push / pop / reset, and for the simplest cases there is a one-shot EasySolver::check_sat_str(script) that takes an SMT-LIB string directly.

no_std core. The oxiz meta-crate is now #![cfg_attr(not(feature = "std"), no_std)], with default = ["std"]. The core modules — oxiz-core, math, sat, theories, and solver — are no_std-capable, so the essential CDCL(T) engine compiles for bare-metal and zkVM targets. The heavier, allocation- and OS-leaning features — nlsat, optimization, spacer, and proof — require std. The meta-crate re-exports the working surface you need: Solver, SolverResult, TermManager, Sort, SortId, and friends.

oxiz-ml. A from-scratch, Pure-Rust ML framework aimed at solver heuristics. It ships dense, convolutional, recurrent, and attention layers; SGD, Adam, RMSprop, and AdaGrad optimizers; feature extraction directly from formulas; and the training infrastructure to put it all together — wired in as branching guidance for the search.

WASM js_api. The browser binding was refactored from a monolithic ~4,000-line lib into focused submodules — solver_core, term_builders, model, optimize, assertions, declarations, diagnostics, and config — shipped with TypeScript typings and React / Vue / Svelte wrappers. The result is a modular API that tree-shakes and types cleanly in a modern front-end build.

Theory / parity layer. Under the hood, OxiZ runs Nelson-Oppen theory combination over the same CDCL(T) stack: oxiz-sat provides CDCL with VSIDS / LRB / CHB heuristics, and oxiz-theories provides EUF, LRA, LIA, BV, Arrays, Strings, FP, and Datatypes. 0.2.0 adds Skolemization for existential quantifiers and refactors the solver, SAT, NLSAT, and optimization modules into subdirectories. All of it is now validated at 100% across the 8 benchmark logics.

Getting Started

Install the meta-crate:

cargo add oxiz

Feature flags let you choose your target — the default is std plus the core solver, but you can drop to no_std for zkVM / RISC-V, or opt into the heavier theories:

[dependencies]
oxiz = "0.2.0"                                            # default: std + core solver
# oxiz = { version = "0.2.0", default-features = false }  # no_std (e.g. zkVM / RISC-V)
# oxiz = { version = "0.2.0", features = ["nlsat", "optimization"] }

A minimal, copy-pasteable example with the new EasySolver API:

use oxiz::easy::EasySolver;

fn main() {
    let mut solver = EasySolver::new();

    // 0 < x < 10
    solver.int_var("x").assert_gt("x", 0).assert_lt("x", 10);

    if solver.check_sat().is_sat() {
        println!("x = {:?}", solver.get_int_value("x"));
    }
}

Or the one-shot string form when you already have an SMT-LIB script:

use oxiz::easy::EasySolver;

let result = EasySolver::check_sat_str(
    "(declare-const x Int) (assert (> x 5)) (check-sat)",
)?;

What’s New in 0.2.0

• NEW EasySolver high-level builder API (oxiz::easy) — fluent variable declaration, assertions, typed model readback, resource limits, push / pop / reset, and a one-shot check_sat_str.
• NEW no_std support — the core solver compiles for bare-metal / zkVM (RISC-V) via default-features = false; std is the default and gates nlsat, optimization, spacer, and proof.
• NEW oxiz-ml crate — a Pure-Rust ML framework (dense / conv / recurrent / attention layers; SGD / Adam / RMSprop / AdaGrad; formula feature extraction; training infra) for ML-guided branching heuristics.
• NEW Skolemization for existential quantifiers.
• CHANGED WASM — js_api split into modular, TypeScript-friendly submodules plus framework wrappers (React / Vue / Svelte).
• CHANGED — refactored solver, SAT, NLSAT, and opt modules into subdirectories; performance optimizations across solver components.
• Benchmarks — large new extended-theory + Z3-parity SMT-LIB suites (AUFLIA, AUFLIRA, QF_ABV, QF_ALIA, QF_AUFBV, QF_NIA_ext, QF_NIRA, UFLIA, UFLRA); sustained 100% Z3 parity (88/88, 8/8 logics). 312,495 lines of production Rust; 6,155 tests (100%).

Tips

• Reach for EasySolver first. For quick problems, solver.int_var("x").assert_gt("x", 0).check_sat() beats hand-building terms and managing sorts. Drop to the low-level Solver / TermManager only when you need it.

• Target zkVM / embedded with default-features = false. The no_std core gives you real SMT inside a proof system or on a microcontroller — just remember nlsat, optimization, spacer, and proof need std and won’t be available there.

• Cap runaway searches. Set timeout, conflict_limit, or decision_limit on the EasySolver so a hard instance can’t run forever:

  solver.timeout(5_000).conflict_limit(100_000);
  

• Read models back typed. Use get_int_value / get_bool_value (and get_model_value for the general case) instead of parsing strings.

• In the browser, use the new modular js_api. Import only the submodules you need, lean on the TypeScript typings, and reach for the React / Vue / Svelte wrappers.

• Let oxiz-ml guide branching. On structured industrial instances, ML-guided heuristics can pay off where generic activity scores plateau.

This is the foundation

OxiZ is the native, auditable reasoning core of the Pure-Rust ecosystem — a solver you can read, ship as one static binary, run in a browser, or fold inside a zero-knowledge proof, all without a line of C. That makes it a natural fit alongside the already-shipped peers it pairs with: theorem proving in OxiLean, legal-tech and verification in Legalis-RS, scientific and array compute in SciRS2 and NumRS2, the semantic web in OxiRS, and quantum in QuantRS2. OxiZ depends on none of them — it stands on its own — but native, memory-safe reasoning is the kind of foundation each of those is glad to build on.

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

Star the repo if a Pure Rust SMT solver that runs everywhere — and matches Z3 on every benchmark — is the kind of foundation you want to build on.

Pure Rust formal reasoning is here — fast, safe, sovereign, and now running anywhere from the browser to bare metal.

— KitaSan at COOLJAPAN OÜ April 4, 2026