PyRank

Smt Solver Python Packages

Python packages with the GitHub topic smt-solver. Sorted by monthly downloads, with stars and forks.
gowrishankar-infra
velaris-lang

Run code an AI wrote without handing it everything you can reach. Each function declares what it may touch. You grant the run one folder, one host or a number of calls, and the runtime refuses anything else the moment it's tried.

23K 4 0
QWED-AI
qwed

Open-source AI verification infrastructure for deterministic verification of LLM outputs, tool calls, code, schemas, and agent state before production execution.

18K 60 13
SRI-CSL
yices

Python bindings for yices2

5K 13 6
alcides
aeonlang

Programming Language designed for Program Synthesis with SMT-validation.

5K 43 6
nicdard
ffg

A generator for Semantic Fusion

3K 2 0
noise01
endoxa

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

3K 0 0
dreal
dreal

Automated Reasoning in Nonlinear Theories of Reals

2K 193 37
gowrishankar-infra
sabline-lang

Run code an AI wrote without handing it everything you can reach. Each function declares what it may touch. You grant the run one folder, one host or a number of calls, and the runtime refuses anything else the moment it's tried.

2K 4 0
formalmethods
intrepyd

Intrepyd Model Checker

2K 19 1
anirbanbasu
smt-sudoku-mcp

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

870 0 0
eduardstan
reasonsmith

Prove which legally-owed reasons a decision system deleted, and from whom — by re-running its own inference, not reading its log. Every verdict states how it was reached.

473 4 4
j4ngzzz
nightjar-verify

Math doesn't hallucinate. Formal verification for AI-generated Python code.

140 0 0
vishk23
arbiter-debate

Open-source framework for formally verifying academic paper claims using multi-agent LLM debate + Z3/Knuckledragger proof certificates. Supports OpenAI, Anthropic, Google, Grok.

139 0 0
TendTo
pydlinear

Refactor of dLinear4 https://github.com/martinjos/dlinear4

128 3 0
testsmt
yinyang

A fuzzing framework for SMT solvers

126 199 26
ZJU-PL
pyaria

Automated Reasoning Infrastructure & Applications

114 17 5
NicholasEhsanRoy
stelling

Static precondition checker for numerical JAX programs: declare a box, get a stamped VERIFIED/REFUTED/UNKNOWN with a runnable witness. Zero required dependencies.

108 1 0
Bhargs24
trespass-rls

Prove your tenants cannot read each other's data. A formal analyzer for Postgres and Supabase row-level security: returns a reproducing exploit or a proof of isolation.

94 0 0
j4ngzzz
nightjarzzz

Math doesn't hallucinate. Formal verification for AI-generated Python code.

91 0 0