SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).
A friendly functional language for finding counterexamples 🎯
ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance. Neurosymbolic theorem-prover orchestrator: 12 core provers, 105 backend integrations (141 ProverKind variants; see docs/PROVER_COUNT.adoc), trust pipeline.
Find soundness bugs in SMT solvers through equivalent transformations
Generate correct-by-construction code for critical functions using Dafny
PARQ is an automatic parallelization engine based on Skolem Function Synthesis and Quantified Invariant Generation. It is aimed at parallelization of array modifying programs written as Constrained Horn Clause (CHC) formulas.
Julia package ecosystem: 34 packages spanning formal verification, cryptography, risk analysis, knot theory, cliodynamics, hardware introspection, and more
A pure-Julia SMT-LIB 2 interface for building constraints, checking satisfiability, retrieving models and working incrementally with solvers such as Z3, CVC5, Yices and MathSAT.
A puzzle game where solutions are cryptographically verified - prove your work, literally.
Practical cvc5 resources for the mathematics and verification communities.
Three-layer formal verification suite for Elixir/OTP/BEAM: sequential pure subsets with TINI + MPR R5 non-interference, choreographic K-CUT GenServer protocols, and Idris2 QTT ABI + verified Zig NIFs under MaxPlus 1 ms scheduler bounds, backed by Z3, CVC5, Alethe proof checking, and ECHIDNA mutation gates.
Experimental verification for a closed Zig subset: source-bound obligations, checked models, explicit trust limits, and proof replay toward a verifier for Zig.
Verification of the Total Coloring Conjecture for all graphs with at most 14 vertices using a SAT Modulo Symmetry Solver.
Combinatorial optimization project solving the Single Round Robin tournament scheduling problem using CP, SAT, SMT, and MIP models, with experiments on symmetry breaking and home–away balance optimization.
To associate your repository with the smt-solving topic, visit your repo's landing page and select "manage topics."