Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
DIG is a numerical invariant generation tool. It infers program invariants or properties over (i) program execution traces or (ii) program source code. DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations.
Information about verification tools. Browse the data at https://slebok.github.io/proverb/
BAP python bindings
AProver: Agentic Prover for AI-Generated Code — LLM agents + BMC for automated verification of systems software
Artifact for paper "Chronosymbolic: Efficient CHC Solving with Symbolic Reasoning and Inductive Learning" in Python
Hoare Logic weakest precondition (WP) calculus engine computing verification conditions for imperative program correctness.
Hoare Logic weakest precondition (WP) calculus engine computing verification conditions for imperative program correctness.
Formal-verification sidecar for typed mathematical Python. For LLM and human research coding workflows.
Bitween: a neuro-symbolic system that learns randomized self-reductions (RSRs) automatically. ICML 2026 (Spotlight).
Flask workbench for parsing MiniLang with ANTLR4, transforming programs to SSA, generating SMT-LIB, and verifying assertions with Z3.
Width-independent proof certificates for KnownBits and word programs, with research tools and a Lean 4 formalization pilot.
Behavior-first program synthesis engine that discovers compact implementations, collapses semantically equivalent programs, and exhaustively verifies behavior across bounded input domains.
Forseti — a formal verifier (ESBMC) inside the agent coding loop: write → verify → counterexample → fix. Q.E.D. is the new LGTM.
Open Verification Kernel (OVK) is an open-source, solver-agnostic verification layer for AI-agent engineering workflows.
A small educational program verification system using Hoare logic, verification conditions, and Z3/SMT solving.
A Neuro-Symbolic Cyber Range Compiler bridging Large Language Models with Z3 Formal Verification.
Bounded equivalence checker that proves an AI-refactored function matches the original—or finds a counterexample—using differential testing and Z3 symbolic execution
To associate your repository with the program-verification topic, visit your repo's landing page and select "manage topics."