OxiZ: A Pure Rust SMT Solver for Formal Verification

[cool-japan]

Project Name

OxiZ: A Pure Rust SMT Solver for Formal Verification

Project Category

Development Tools / Infrastructure

Project Description

Problem:
Formal verification is crucial for Web3 security. However, most SMT solvers (Z3, CVC4) are C++ based, making them unsuitable for Wasm environments and hard to integrate into pure Rust chains like Polkadot/Substrate without complex FFI.

Solution:
OxiZ is an existing, high-performance SMT solver written entirely in Pure Rust.
Unlike other "planned" projects, OxiZ is already live (v0.1.1) and available on crates.io. It currently supports SAT solving (CDCL), basic theories, and even optimization (MaxSAT).

We are applying for this grant to take OxiZ to the next level: Full Substrate Compatibility and Advanced BitVector Support.

1. Wasm-First: Optimizing the existing codebase to run efficiently in no_std and Wasm environments (browser/on-chain).
2. Smart Contract Logic: Implementing Fixed-Size BitVectors (QF_BV), which is mandatory for verifying Solidity/ink! contracts (u256 arithmetic).
3. Proof Generation: Enhancing the proof checker to ensure the solver's results are trustless.

Team Name

COOLJAPAN OU (Team KitaSan)

Team Members

• GitHub: @cool-japan
• Role: Lead Developer, Researcher & Maintainer

Team's Experience

I am a legal professional turned systems engineer (Univ. of Tokyo, Law). I have a strong track record in the Rust ecosystem, having already designed and released the core architecture of OxiZ.
My focus is on "Legalis" (Law as Code), where I research the intersection of formal logic, law, and software correctness. OxiZ is a core component of this initiative, designed to mathematically prove the correctness of logic.

Team Code Repos

• https://github.com/cool-japan/oxiz (Active, v0.1.1 released)
• https://github.com/cool-japan

Team LinkedIn Profiles

• https://www.linkedin.com/in/tetsuya/

Development Status

• Current State: ALREADY WORKING.
  • Core SAT (CDCL), MaxSAT, and basic theories are implemented.
  • Crates (oxiz, oxiz-core, oxiz-opt) are published on crates.io.
• Differentiation: This is the only active, feature-rich SMT solver in Pure Rust that aims for Z3 compatibility without FFI.

Development Roadmap

Overview:

• Total Estimated Duration: 3 months
• Full-Time Equivalent (FTE): 1 FTE
• Total Costs: 30,000 USD

Milestone 1 — BitVectors Theory (QF_BV) & Arithmetic

Taking the solver from "academic math" to "blockchain math" (u256).

• Estimated duration: 1 month
• FTE: 1
• Costs: 10,000 USD

Number	Deliverable	Specification
1.	BitVector Theory	Implement QF_BV (Quantifier-Free Bit-Vectors) theory solver, crucial for EVM/Wasm contract verification.
2.	Modular Arithmetic	Optimize for 256-bit arithmetic operations common in smart contracts.
3.	SMT-LIB2 Compliance	Extend the existing parser to support the full SMT-LIB2 BitVector logic.
4.	Test Suite	Validate against standard SMT-COMP benchmarks for BitVectors.

Milestone 2 — Wasm/no_std Support & Ink! Integration

Making it run inside the browser and Substrate runtime.

• Estimated duration: 1 month
• FTE: 1
• Costs: 10,000 USD

Number	Deliverable	Specification
1.	no_std Support	Refactor oxiz-core to rely only on core and alloc crates, removing standard library dependencies.
2.	Wasm Optimization	Optimize memory usage and panic handling for wasm32-unknown-unknown target.
3.	Browser Demo	A fully client-side web interface where developers can verify logic using OxiZ in Wasm.

Milestone 3 — Proof Production & Advanced Tactics

Ensuring the solver's output can be trusted (Proof-carrying code).

• Estimated duration: 1 month
• FTE: 1
• Costs: 10,000 USD

Number	Deliverable	Specification
1.	Proof Generation	Enhance oxiz-proof to generate standard proof certificates (DRAT/Alethe) for UNSAT results.
2.	Parallel Solving	Implement portfolio solving (running multiple strategies in parallel) using Rust's async/await.
3.	Case Study	Publish a technical article demonstrating a formal verification of a simple ink! smart contract using OxiZ.

Future Plans

• Official integration as a backend for the ink! verification toolchain.
• Developing a DSL (Domain Specific Language) for "Legal Logic" on top of OxiZ.
• Collaboration with ink! developers to provide static analysis tools.

Additional Information

I am based in Southeast Asia and operate through my Estonian entity, COOLJAPAN OU. I am dedicated to building open-source infrastructure that enhances the reliability of the decentralized web.

[semuelle]

Hey, @cool-japan, thanks for reaching out. Unfortunately, the Grants Program is closed. You can find alternative funding opportunities on the W3F Funding and Support page. In any case, good luck with the project!