Z3 Python Packages

crosshair-tool

An analysis tool for Python that blurs the line between testing and type systems.

manticore

Symbolic execution tool

oxiz

OxiZ is a high-performance Satisfiability Modulo Theories (SMT) solver written entirely in Rust. This project is part of an initiative to reimplement Z3 in Pure Rust. Pure Rust is a fundamental requirement - no C/C++ dependencies, no FFI bindings, just clean, safe Rust code.

cryptanalysis

Automated cryptanalysis of substitution permutation network cipher

a2a-greenhelix-sdk

Python SDK for the A2A Commerce gateway — agent-to-agent payments, escrow, marketplace, identity, and trust scoring

str8ts-solver

str8ts solver using z3

nxuskit-py

Provider-agnostic AI SDK for Rust, Go, Python, and C ABI: LLMs, local models, CLIPS rules, Z3 solvers, Bayesian networks, ZEN decision tables, and nxuskit-cli.

qwed-finance

Deterministic verification middleware for banking and financial AI. NPV, IRR, loan amortization, and interest calculations with QWED precision.

grilops

a GRId LOgic Puzzle Solver library

proofofthought

Proof of thought : LLM-based reasoning using Z3 theorem proving with multiple backend support (SMT2 and JSON DSL)

qwed-mcp

MCP Server for QWED Verification - Use QWED verification tools in Claude Desktop, VS Code, and any MCP client

csl-core

CSL-Core: Deterministic Safety Layer for Probabilistic AI Systems

intrepyd

Intrepyd Model Checker

clauz3

Static contract experiments for agent-authored Python

provably

Proof-carrying Python — Z3-backed formal verification via @verified decorators

arbiter-debate

Formally verified multi-agent debates

ffg

A generator for Semantic Fusion

astraintella

Verified AI reasoning SDK — formal verification layer between LLMs and constraint solvers

yinyang

A fuzzing framework for SMT solvers

verasolve

Verified AI reasoning SDK — placeholder reserving the PyPI name. Functional SDK coming soon.

z3-armor

Constraint-based obfuscation using z3.