◉ COOLJAPAN
← All posts
July 2, 2026 • 9 min read

OxigenAI 0.1.1 Released — Real SMT Contradiction Detection, Three Jurisdictions, and Judgment Prediction

OxigenAI 0.1.1 replaces its contradiction heuristic with genuine OxiZ SMT verification, adds JP/US/EU multi-jurisdiction statute registries via a new -j flag, and ships /predict-ruling and /translate-check — 231 tests passing. The sovereign computational-law layer for the COOLJAPAN ecosystem.

release oxigenai govtech legal-tech computational-law smt legalis pure-rust multi-jurisdiction

0.1.0 said the contradiction check was SMT-backed. 0.1.1 is the release where that became true.

Today we released OxigenAI 0.1.1 — the release that replaces a discriminant-based contradiction heuristic with genuine OxiZ SMT satisfiability checking, extends the platform from one jurisdiction to three, and ships two entirely new capabilities: judgment prediction and offline translation verification.

No C. No C++. No Fortran. No Z3. OxigenAI’s contradiction detector runs on OxiZ, COOLJAPAN’s Pure Rust SMT solver, reached through legalis-verifier’s smt-solver feature — and as of 0.1.1, verifier/contradiction.rs actually calls SmtVerifier::is_satisfiable instead of approximating the answer with a discriminant-based heuristic. It still compiles to one static oxigenai binary serving both the HTTP API and the full CLI, and now it speaks for Japan, the United States, and the European Union instead of Japan alone.

Why OxigenAI 0.1.1 is a game changer

The Digital Agency’s GenAI (源内) — the Python / Vertex AI / BigQuery system OxigenAI reimplements — is built for one jurisdiction and one mode of trust:

OxigenAI 0.1.1 ends all of that.

Technical Deep Dive: four layers, three jurisdictions

  1. Verification core (verifier/contradiction.rs, verifier/jurisdiction.rs). Selected provisions go through SmtVerifier::is_satisfiable (OxiZ, via legalis-verifier’s smt-solver feature) for genuine joint-satisfiability checking, alongside the restored ID-collision, jurisdictional-overlap, and temporal-conflict heuristics. verifier/jp_statutes.rs, verifier/eu_statutes.rs, and verifier/us_statutes.rs hold the seed statute sets that the MultiJurisdictionMatcher registry dispatches across — and this release converted their numeric and categorical preconditions from free-text Condition::Custom to structured, SMT-visible Threshold/Duration/AttributeEquals/SetMembership variants, since an SMT solver can only reason about what it can actually parse. Genuinely open-textured standards (constitutional balancing, fair use, public-policy clauses) were deliberately left as Custom.
  2. Generative Jurisprudence (verifier/jurisprudence.rs, handlers/predict.rs). The 8-precedent curated corpus is searched and ranked by relevance × precedent authority, then handed to a two-call Gemini pipeline — web-grounded retrieval, then temperature-0 synthesis — before the result is classified through legalis-core::LegalResult<T>.
  3. Translation verification (verifier/translate_check.rs, handlers/translate.rs). Both XML documents compile to Legalis DSL independently, and the comparison — statute count, effect-type multiset, recursive precondition-kind multiset, combined into a weighted Sørensen–Dice score — runs entirely offline, with no LLM or network call anywhere in the path.
  4. Pipeline & handlers (services/pipeline.rs, handlers/report.rs, handlers/simulate.rs, handlers/formalize.rs, handlers/jurisdictions.rs). The existing law-name-inference → BigQuery-retrieval → verification → LegalResult<T> classification → report-generation pipeline now threads an optional jurisdiction field end to end on POST /, and the new handlers/jurisdictions.rs backs the GET /jurisdictions discovery endpoint.

Five new criterion benchmarks (benches/domain_matching.rs, dsl_compile.rs, contradiction_smt.rs, simulation.rs, jurisprudence.rs) now cover these hot paths directly, run via cargo bench.

Getting Started

cargo install oxigenai

Query a new jurisdiction directly from the CLI:

# EU query — pulls from the new GDPR statute set instead of Japanese law
oxigenai "What is the lawful basis for processing personal data under GDPR?" -j EU

# predicted ruling (Generative Jurisprudence)
oxigenai predict "5年勤続の有期社員を経営不振で解雇できるか" --facts "解雇回避努力なし"

# statute vs. translation consistency check — fully offline, no GCP needed
oxigenai translate-check --source ja.xml --target en.xml

Or hit the HTTP API directly:

PORT=8080 oxigenai serve

curl -s -X POST http://localhost:8080/ \
  -H 'Content-Type: application/json' \
  -d '{"inputs":{"input_text":"What counts as overtime under the FLSA?"},"jurisdiction":"US"}'

curl -s http://localhost:8080/jurisdictions

What’s New in 0.1.1

Tips

This is the foundation

OxigenAI 0.1.1 goes deeper into the Legalis-RS stack it was already built on — legalis-core, legalis-verifier, legalis-dsl, legalis-sim, and legalis-jp, all now at 0.1.6 — and turns what 0.1.0 described as SMT-backed verification into code that genuinely performs it. The new EU and US statute registries are a first step toward a Legalis-RS that speaks more than one legal system, and /predict-ruling’s precedent-ranking and /translate-check’s structural DSL comparison are both built entirely on primitives — LegalResult<T>, the DSL compiler, the SMT verifier — that already existed elsewhere in the ecosystem. OxiZ, COOLJAPAN’s Pure Rust SMT solver, is what makes the contradiction claim provable rather than merely asserted; every jurisdiction OxigenAI adds from here just gives that same solver more law to prove things about.

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

Star the repo if you think a legal-tech platform’s contradiction claims should be provable, not just plausible.

The era of “trust the LLM” government legal AI is over. Pure Rust computational law — verified, multi-jurisdictional, and sovereign — is here.

— KitaSan at COOLJAPAN OÜ July 2, 2026

↑ Back to all posts