20 posts
OxiZ 0.3.2 is a soundness release driven by an external differential-testing report: 8 pull requests, 0 merged, every fix independently reimplemented from scratch and backed by a regression test. EUF congruence, Bool/EUF encoding, Arithmetic⇄EUF combination, and NLSAT conflict analysis are all corrected — 168/168 Correct on the Z3 parity suite, 9,953 tests passing. Pure Rust, Apache-2.0.
OxiZ 0.3.1 is a soundness-and-honesty release: five reported GitHub issues plus 40+ bugs of the same silently-wrong-answer shape are fixed, wide (>64-bit) bit-vectors are now exact via BigUint, and MBQI completeness brings the Z3 differential parity suite to 168/168 Correct, 0 Wrong. 9,668 tests passing. Pure Rust, Apache-2.0.
OxiZ 0.3.0 is a hardening-and-capability wave: a new ground string decision procedure and concrete floating-point model finder lift qf_s and qf_fp from partial to 10/10 on the Z3 parity suite, MBQI SAT certification advances three quantified logics, and a dozen soundness bugs are fixed — 8,119 tests passing, 0 Wrong verdicts across 154 decisive Z3 comparisons. Pure Rust, Apache-2.0.
OxiZ is a high-performance SMT solver in pure Rust — a Z3 replacement. 0.2.4 lands the results of a 19-agent production-readiness audit and five fix waves — real Sturm sequences, sound SAT conflict analysis, honest Cooper QE, corrected BV division — plus new oxiz-py string, floating-point, and quantifier bindings, with 7,666 tests passing workspace-wide.
OxiLean 0.1.3 ships oxilean-verify, an independent Lean 4 proof checker with three-bucket verdicts, a 144 KB gzip WASM 'Kernel in a Tab,' a kernel soundness overhaul, and a structural-sharing rewrite cutting full-Init verification from 1h20m to 11m28s — the sovereign theorem-proving layer for the COOLJAPAN ecosystem.
OxiZ is a high-performance SMT solver in pure Rust — a Z3 replacement. 0.2.3 lands sound incremental BV & Simplex solving, a full term-level MaxSMT/OMT optimization pipeline, real BMC and k-induction model checking, and generic in-memory DRAT/LRAT proof writers — with 6,826 tests passing and 100% Z3 parity.
SplitRS 0.3.2 adds an SMT-verified extraction pass: it factors pure integer sub-blocks out of over-budget functions and commits the rewrite only when OxiZ proves the result is equivalent for all inputs. Plus array-splitting, a test-module splitter, shipped editor plugins, and 450 passing tests.
OxiZ is a pure-Rust SMT solver reimplementing Z3. 0.2.2 ships real LBD clause scoring (replacing the old stub), Big-M primal simplex for LP, an LRU lemma cache, ML conflict-hook branching, and deeper Z3-compat APIs — all with 100% Z3 parity and zero C/C++/Fortran.
OxiLean 0.1.2 lands real SMT solving via OxiZ, a complete 157-instruction WebAssembly bytecode interpreter wired to the real kernel/parse/elab pipeline, keccak256-correct EVM/Solidity ABI selectors, real Gröbner-basis reduction for polyrith, and 33,091 passing tests — all in a Pure Rust theorem prover.
OxiZ is a pure-Rust SMT solver and Z3 replacement. 0.2.1 sharpens the EUF (congruence-closure) hot path: reusable allocation buffers, O(k) incremental pop() via a sig_table/fingerprint_table trail, cache-friendly ENode layout, and new production EUF criterion benchmarks. 100% Z3 parity, still pure Rust.
OxiZ 0.2.0 ships an ergonomic EasySolver builder, no_std support for bare-metal/zkVM (RISC-V), a Pure-Rust ML heuristics crate (oxiz-ml), Skolemization, a modular WASM js_api, and 100% Z3 parity across 88 benchmarks. Zero C/C++.
Pure Rust reimplementation of Lean 4’s Calculus of Inductive Constructions. 99.7% Mathlib4 compatibility, zero unsafe in kernel, full tactics + metaprogramming — bringing industrial-grade formal verification directly into the Rust ecosystem.
OxiLean 0.1.0 is the debut of a memory-safe Interactive Theorem Prover written entirely in Rust, inspired by Lean 4 — a zero-dependency kernel implementing the full Calculus of Inductive Constructions, a complete tactic framework, and a WASM REPL that runs in the browser.
A complete, high-performance Satisfiability Modulo Theories solver written entirely in Rust. Full CDCL(T) architecture, comprehensive theory support, proof generation, and Z3-level performance — with zero C/C++ dependencies and full memory safety.
OxiZ 0.1.2 adds PyO3 Python bindings (oxiz-py), a Pure-Rust BLAS + multi-precision (MPFR-style) math layer, an SMT-COMP benchmark suite, and a vastly expanded CLI (dashboard/server/distributed/TPTP/interpolation). A Pure Rust Z3 replacement with zero C/C++.
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.
OxiZ is a Pure Rust Satisfiability Modulo Theories solver reimplementing Z3 — a full CDCL(T) architecture with EUF/LRA/LIA/BV/Arrays/Strings/FP/Datatypes theories, SMT-LIB2 support, and roughly 90% Z3 feature parity, all with zero C/C++. This is its first public release.
OxiZ 0.1.1 ships a new unified `oxiz` meta-crate with feature-flagged modular usage (solver/nlsat/optimization/spacer/proof/full), plus MBQI and CDCL(T) theory-propagation fixes. A Pure Rust Z3 replacement with zero C/C++.
Legalis-RS 0.1.1 adds United Kingdom and Singapore jurisdictions to the Pure Rust legal-DX framework and grows the test suite from 6,100+ to 9,568 across 23 crates, with a near-zero-warning quality pass.
Legalis-RS is a Pure Rust framework that turns legal statutes into structured, machine-verifiable code — a Legal DSL parser, formal verifier, population simulator, and multi-jurisdiction support (JP/DE/FR/US). An honest first release.