Smt Python Packages

manticore

Symbolic execution tool

certo-math

Between having a mathematical idea and having a proof of it there is a lot of work that is not proving: find the object, break the false claims, measure what survives, reduce it to what it really is, assemble the rest. certo does that work, and every step returns a certificate anyone can re-check without trusting it. CLI + MCP.

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.

touchstone-prover

An SMT-based verifier and type inferencer for Python: proves contracts, equivalence, and trap-freedom (with counterexamples) over a Rocq trust base.

ffg

A generator for Semantic Fusion

endoxa

Governed beliefs for LLM agents: an append-only ledger, SMT-checked consistency, defeasible revision, and calibration instruments.

isla-solver

The ISLa (Input Specification Language) language & solver.

unicode-fol-kit

Parse, translate, prove and model-check logic formulas in Unicode notation: first-order, modal, description and higher-order logic, one API over a dozen provers, and an MCP server

cadl-lang

CADL (Contract Architecture Description Language): a DSL and toolchain for specifying, verifying and generating code from institutional designs in Systems of Systems

erdl-formal

Determinism isn't tested — it's proven. SMT-based formal verification for ERDL, the rule language of enterprise AI agents.

package-maximizer

Модульная система для максимизации непротиворечивого множества пакетов

iamprover

Formally verify AWS IAM security invariants with Z3 — SMT proofs and counterexample traces, not pattern-matching. CI-gate your Terraform IAM changes.

smt-sudoku-mcp

An MCP server to work with Sudoku puzzles using satisfiability modulo theories (SMT).

autoguess

An easy-to-use, general and open-source tool to solve the guess-and-determine problem

py2many

Transpiler of Python to many other languages

decern

Deterministic authorization + tamper-evident audit for AI agents, humans, and workloads — one principal type, safety invariants machine-checked by an SMT solver (cvc5), every decision independently verifiable offline. Pure Rust.

unicode-logic-kit

Parse, translate, prove and model-check logic formulas in Unicode notation: first-order, modal, description and higher-order logic, one API over a dozen provers, and an MCP server

eleph

A language whose programs cannot lie.

formulagate

Physics-aware LLM guardrail — deterministic dimensional analysis with Z3 SMT proof and calibrated abstention

clauz3

Static contract experiments for agent-authored Python

smt-portfolio

A simple wrapper to run multiple SMT solvers in parallel

dataforge-07-mcp

Verifiable data-mutation protocol for tabular data: changes only what it can prove correct against stated constraints, refuses the rest with a reason, is byte-for-byte reversible, and emits a portable attestation a third party can verify without trusting it.

provensql

Sound-by-construction semantic diff for SQL: know whether a query edit changes the answer.

provably

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