AutoProv is an autonomous, agentic CI/CD pipeline that bridges the gap between natural language requirements and mathematically infallible production code. By combining the creative reasoning of Large Language Models (LLMs) with the absolute rigor of SMT solvers (Microsoft Dafny) inside a zero-trust sandbox, AutoProv guarantees logical correctness for mission-critical software.
- 🧠 The Architecture
- 🌍 Industry Applications (8 Use Cases)
- 🔌 Supported LLM Providers
- 📚 Academic Foundation
- 🚀 Getting Started
AutoProv utilizes a Neuro-Symbolic architecture. It uses Neural Networks to write the code, and Symbolic Logic to prove it.
graph TD
A[Human Natural Language Request] -->|Prompt| B(Specifier Agent)
B -->|Mathematical Contracts| C(Coder Agent)
C -->|Unverified Code| D{Dafny SMT Sandbox}
D -- Constraints Violated --> E(Repair Agent)
E -->|Patched Code| D
D -- Zero Errors --> F[Dafny Transpiler]
F --> G((Production Python Artifact))
- Specifier Agent: Translates human requirements into formal mathematical contracts (
requirespreconditions andensurespostconditions). - Coder Agent: Implements the algorithmic logic using strict loop
invariantsanddecreasesclauses. - Verifier Sandbox: Executes the Microsoft Dafny SMT solver inside an ephemeral, network-isolated Docker container to prove the mathematics against infinity.
- Repair Agent: Analyzes solver trace logs and autonomously patches the logic if verification fails.
- Transpiler: Compiles the proven logic into production-ready Python (
verified_output.py). - Observability: Integrated with LangSmith for real-time telemetry, token-tracking, and prompt tracing.
Traditional Unit Testing tests a handful of scenarios. Formal Verification tests all possible numbers in the universe simultaneously. AutoProv is designed for sectors where a software bug results in catastrophic loss.
- Problem: An "off-by-one" array error in an automated IV pump could deliver a fatal dose of medication.
- Solution: AutoProv generates dosage algorithms with strict math guarantees (e.g.,
ensures patient_weight < 12 ==> rate <= 15). The Python artifact is logically incapable of exceeding safety thresholds.
- Problem: A sensor edge-case in a Load Moment Indicator (LMI) could cause a crane to tip.
- Solution: AutoProv builds "kill-switches" proven to never return
True(safe to lift) if wind speed or boom angle exceed boundaries.
- Problem: A single vulnerability in a blockchain smart contract can allow hackers to drain millions (e.g., Re-entrancy attacks).
- Solution: AutoProv mathematically audits transactional logic, guaranteeing ledger balances cannot be manipulated outside of approved constraints.
- Problem: Stock routing algorithms operating in microseconds cost millions if they hit an out-of-bounds error.
- Solution: SMT solvers prove HFT array-parsing loops will always terminate and never access an invalid index.
- Problem: Integer overflows in navigation algorithms can cause catastrophic flight envelope failures (e.g., the Ariane 5 rocket disaster).
- Solution: AutoProv verifies navigation subroutines to guarantee variables never overflow memory limits during high-velocity floating-point calculations.
- Problem: A race condition or logic flaw in Advanced Driver Assistance Systems (ADAS) fails to trigger emergency brakes.
- Solution: AutoProv generates collision-avoidance logic with proven timing bounds and response invariants, meeting ISO 26262 ASIL D safety standards.
- Problem: Logic flaws in encryption implementations (like the Heartbleed bug) leak secure memory to attackers.
- Solution: AutoProv ensures memory safety and bounds-checking for cryptographic hashing functions, similar to how AWS uses Dafny to verify their
s2n-tlsencryption.
- Problem: Temperature monitoring systems fail to activate cooling pumps due to a variable logic error.
- Solution: AutoProv provides invariants guaranteeing that pump-activation methods absolutely will execute when threshold variables are breached.
AutoProv is built with LiteLLM, an abstraction layer allowing you to use almost any foundational model. Simply update your .env file:
- OpenAI:
MODEL_NAME="gpt-4o" - Anthropic:
MODEL_NAME="claude-3-5-sonnet-20240620" - Google:
MODEL_NAME="gemini/gemini-3.5-flash"
This repository builds upon recent breakthroughs in combining generative AI with formal methods:
- Z3 Theorem Proving: Relies on the Z3 SMT Solver developed by Microsoft Research (De Moura & Bjørner, 2008) to prove absolute program correctness mathematically.
- Auto-Formalization: Inspired by research into LLM-driven Auto-formalization (Wu et al., 2022), which utilizes neural networks to translate ambiguous natural language specifications into strict mathematical boundaries.
- LLM-Assisted Formal Verification: Addresses the steep learning curve of verification languages (Coq, Lean, Dafny) by utilizing agents to generate whole-proof repairs (e.g., the Baldur architecture, First et al., 2023).
AutoProv is fully automated via GitHub Actions.
Ensure the following GitHub Repository Secrets are set:
GEMINI_API_KEY,OPENAI_API_KEY, orANTHROPIC_API_KEY(Depending on your preferred provider).LANGCHAIN_API_KEY: For the Observability Dashboard.
- Modify the
challengestring at the bottom ofautoprov_orchestrator.pywith your natural language request. - Commit and push the code to the
mainbranch. - GitHub Actions will automatically provision the environment, build the secure Docker sandbox, and run the pipeline.
- Monitoring: Log into your LangSmith dashboard to watch the agents reason and resolve errors in real-time.
- Retrieval: Download the
mathematically-verified-pythonartifact from the Actions Summary page.