[Announce] OxiZ 0.1.1: A Pure Rust SMT Solver (aiming for Z3 compatibility)

announcements
1

Hi Rustaceans!

I’m excited to share the first release of OxiZ, a purely Rust-based SMT solver.

Why another SMT solver? Like many of you, I love Z3, but I hate dealing with C++ bindings (FFI), complex build chains, and the difficulty of compiling for WASM or embedded targets. I wanted a solver that I could just add to Cargo.toml and compile anywhere—no system dependencies required.

Key Features of v0.1.1:

  • Pure Rust: No C++ code. Zero unsafe blocks (mostly).
  • Z3-Compatible API: Designed to look and feel like the Z3 Rust bindings, making migration easier.
  • WASM Ready: Runs in the browser or on edge runtimes.
  • Core Logic: Implements CDCL (Conflict-Driven Clause Learning) and basic theory solving.

Example Usage: It solves constraints just like you'd expect:

use oxiz::Context;

fn main() {
    let ctx = Context::new();
    let x = ctx.int_const("x");
    let y = ctx.int_const("y");
    
    let solver = ctx.solver();
    // x > 10 AND y < 5 AND x + y = 20
    solver.assert(&x.gt(&ctx.int_val(10)));
    solver.assert(&y.lt(&ctx.int_val(5)));
    solver.assert(&x.add(&y).eq(&ctx.int_val(20)));

    assert_eq!(solver.check(), Status::Satisfiable);
    // Model generation is coming soon!
}

Roadmap: This is still early alpha. We are working on:

  • BitVectors and Array theory support.
  • Performance optimization (currently focusing on correctness).
  • Full SMT-LIB 2 parsing.

I wrote a blog post about the philosophy behind this project (and how it connects to my other projects like physics simulation): [ OxiZ 0.1.1: Why We Are Re-inventing the SMT Solver in Pure Rust (Z3-Compatible SMT Solver)]

I’d love to hear your feedback, and PRs are always welcome!

5 Likes
2

This is SOOOO GOOD! Finally! We have a SMT/SAt library implemented in 100% Rust. How I can get involved? do you have a discord group?

1 Like
3

Thank you so much! I'm really glad to hear that. (I've just released 0.1.2)

I built this exactly because I was tired of fighting with C++ bindings and wanted a pure Rust ecosystem.

Regarding communication, we don't have a Discord server yet -- I'd prefer to keep conversations on GitHub Discussions for now so that knowledge can be shared openly and archived.

How to get involved: Since it's still v0.1.2, there are plenty of things to do!

  1. Break it: Try using OxiZ in your projects and report panic/bugs.
  2. Missing Theories: We need help implementing BitVectors and Arrays.
  3. SMT-LIB 2: We are working on a parser to be fully compatible with Z3 inputs.

Feel free to open an issue or start a discussion on GitHub. Let's build the best logic engine together!