Skip to content

Prove Guard

Prove Guard is an AI agent that formally verifies Python code for safety bugs using mathematical proofs.

Code Video Cerebral Valley

Core trick

AST extracts Python functions, Gemini drafts Lean 4 proofs of division, indexing, and None safety, and the Lean compiler checks each proof.

Tags

securitydev tools

Description

Prove Guard is an AI agent that formally verifies Python code for safety bugs using mathematical proofs. Point it at any public GitHub repo and it analyzes Python functions for three classes of runtime errors — division by zero, index out of bounds, and None dereference — using real formal verification, not heuristics. The pipeline extracts Python functions via AST, uses Gemini 3.1 Pro to translate them into Lean 4 theorem statements and proof attempts, then runs the Lean 4 compiler to mathematically verify each proof. A successful proof is a mathematical guarantee that the bug cannot occur. A failed proof flags a potential real bug with the Lean code as evidence.
dsaccon/prove-guard★ 00 forksTypeScriptCreated Mar 21, 2026 · last push Mar 22, 2026

README excerpt

# Prove Guard

Formal verification for Python, powered by AI. Paste a GitHub repo URL and get mathematical proofs about your code's safety.

Built at the [Zero to Agent: Vercel x DeepMind Hackathon SF](https://cerebralvalley.ai/e/zero-to-agent-sf/details) (March 21-22, 2026).

**Live demo:** [prove-guard.vercel.app](https://prove-guard.vercel.app)

**Video demo:** [Watch on YouTube](https://youtu.be/axmYk5XNOxs)

## What it does

Prove Guard analyzes Python functions for three classes of runtime safety bugs using formal verification — not heuristics, not AI guessing, but machine-checked mathematical proofs via the [Lean 4](https://lean-lang.org/) theorem prover.

### Safety properties checked

| Property | Detects | Example |
|---|---|---|
| **Division by Zero** | `/`, `//`, `%` operators | `sum(items) / len(items)` crashes on empty list |
| **Index Out of Bounds** | `list[i]`, `dict[key]` access | `items[0]` crashes on empty list |
| **None Dereference** | `None` defaults, `.get()`, `.find()` | `x.strip()` where `x=None` |

### Verdicts

- **Proven Safe** — Lean 4 verified the proof. The property holds for all inputs.
- **Potentially Unsafe** — Lean rejected the proof. Possible bug found.
- **Inconclusive** — Translation too complex or verification timed out.

## How it works

```
GitHub repo URL
    → Clone repo (shallow)
    → Extract Python functions (AST)
    → Classify safety properties (AST heuristics)
    → Translate to Lean 4 theorems (Gemini 3.1 Pro)
    → Verify pr

Team