# Prove Guar

- **Event:** [Zero to Agent: Vercel x Deepmind Hackathon SF](https://cerebralvalley.ai/e/zero-to-agent-sf)
- **When:** Sat, Mar 21 at 9:00 AM – 10:00 PM (PDT)
- **Where:** Shack15, San Francisco, CA
- **Team:** [David S](https://cerebralvalley.ai/u/david-s)
- **GitHub:** https://github.com/dsaccon/prove-guard
- **Demo video:** https://youtu.be/axmYk5XNOxs
- **Gallery:** https://cerebralvalley.ai/e/zero-to-agent-sf/hackathon/gallery
- **Page:** https://cerebralvalley.ai/e/zero-to-agent-sf/hackathon/gallery/62

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.

---

Markdown version of https://cerebralvalley.ai/e/zero-to-agent-sf/hackathon/gallery/62. Site index for agents: https://cerebralvalley.ai/llms.txt · full text: https://cerebralvalley.ai/llms-full.txt