◉ COOLJAPAN
← All posts
January 17, 2026 • 6 min read

Legalis-RS 0.1.2 Released — SMT Verification Goes Pure Rust with OxiZ

Legalis-RS 0.1.2 replaces the C++ Z3 backend in its legal verifier with OxiZ, the Pure-Rust SMT solver — rigorous proofs with no native toolchain. Plus a zero-warning build across 25 crates and 11,365 passing tests.

release legalis legal-tech rust smt-solver oxiz formal-verification pure-rust

Formal legal verification just went fully Pure Rust.

Today we released Legalis-RS 0.1.2 — the legal verifier swaps its C++ Z3 dependency for OxiZ, the Pure-Rust SMT solver, so rigorous proofs now build like any other Rust crate, alongside a zero-warning hardening pass across the whole workspace.

No C. No C++. No Fortran. Legalis-RS is a Pure Rust framework for parsing, analyzing, and simulating legal statutes — Legal DX — cleanly separating Deterministic Logic from Judicial Discretion. The whole stack compiles to a single static binary or to WASM, with no native toolchain in the way. Until now, one optional path broke that promise: the formal verifier’s SMT backend leaned on the C++ Z3 library. As of 0.1.2 that last non-Pure-Rust dependency is gone, replaced by OxiZ — which means even the rigorous proofs are sovereign Pure Rust, end to end.

In a world of closed legal SaaS, Java/Python legal stacks, and verification engines bolted to a C++ solver, Legalis-RS stays small, inspectable, and yours: one binary, one toolchain, no surprises at deploy time.

Why 0.1.2 is a milestone

Formal legal verification with Z3 always came with a tax. To prove that a body of statutes contained no contradictions — no unsatisfiable conditions, no logical dead ends — you had to bring in the C++ Z3 library: brew install z3, then source setup-z3-env.sh to wire up the environment, then hope the system solver matched what your build expected. It was fragile, platform-specific, and effectively un-shippable as a clean Rust artifact.

0.1.2 removes that tax. OxiZ delivers the same SMT-backed contradiction and unsatisfiability checking with a plain cargo build. The concrete wins:

Technical Deep Dive: from Z3 to OxiZ

In 0.1.0 and 0.1.1, the legalis-verifier crate’s optional SMT backend was the C++ Z3 library. Its Cargo.toml pulled z3 = "0.12" behind a z3-solver feature, and using it required a system Z3 install plus an environment setup script.

In 0.1.2, that z3 dependency is removed and replaced with OxiZ — the COOLJAPAN Pure-Rust Z3 alternative — via oxiz-solver = "0.1.1" and oxiz-core = "0.1.1". The verifier’s feature is now:

smt-solver = ["oxiz-solver", "oxiz-core", "num-bigint"]

The old z3-solver feature is gone.

What the verifier does is unchanged. It still performs circular-reference detection, dead-statute and unsatisfiable-condition detection, and constitutional-compliance checking. Only the proof engine underneath changed — and it’s now Pure Rust. The default build still ships with no SMT backend at all, keeping it lean; enabling smt-solver stays entirely C/C++-free.

OxiZ is a COOLJAPAN sibling that first shipped on 2026-01-12, just five days before this release. It is the Pure-Rust SMT solver that makes this migration possible — a drop-in spirit replacement for Z3 that fits the Pure Rust deployment model rather than fighting it.

Getting Started

Add the core library:

cargo add legalis-core

This also provides the legalis CLI binary.

To opt into rigorous, SMT-backed proofs (no system Z3 required anymore):

cargo add legalis-verifier --features smt-solver

Then build and verify a statute:

use legalis_core::{Statute, Condition, Effect, EffectType, ComparisonOp};
use legalis_verifier::StatuteVerifier;

let statute = Statute::new(
    "voting-rights",
    "Voting Rights Act",
    Effect::new(EffectType::Grant, "Right to vote in elections"),
)
.with_precondition(Condition::Age {
    operator: ComparisonOp::GreaterOrEqual,
    value: 18,
});

let verifier = StatuteVerifier::new();
let result = verifier.verify(&[statute]);
if !result.passed {
    for error in result.errors {
        eprintln!("Verification error: {}", error);
    }
}

What’s New in 0.1.2

Tips

Part of the COOLJAPAN ecosystem

Legalis-RS 0.1.2 builds directly on OxiZ, the COOLJAPAN Pure-Rust SMT solver, joining a family of sovereign Pure-Rust libraries — including SciRS2 for scientific computing — that share one principle: no C, no C++, no Fortran in the default path.

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

Star the repo if you believe legal technology — even the formal proofs — belongs in Pure Rust. Pure Rust legal-tech is here: fast, safe, and sovereign.

— KitaSan at COOLJAPAN OÜ January 17, 2026

↑ Back to all posts