Show HN: Provepy – A Python decorator that proves your code using Lean and LLMs

Category: devtools

Tags: formal-verification, ai-assisted, theorem-proving, python-decorator

Score: 6.3/10 (Innovation: 8, Technical: 7, Documentation: 6, Utility: 4)

Provepy is a Python decorator that attempts to automatically formalize and prove the correctness of Python functions using Lean theorem prover and LLMs. It's interesting because it bridges formal verification with everyday programming by hiding complex Lean syntax behind a simple decorator, making formal methods more accessible through AI-assisted autoformalization.

Target audience: backend devs, researchers, formal-methods enthusiasts

Repository: https://github.com/genie16/provepy · Python · MIT · 1 stars

View on Hacker News