Prove Guar

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.