Show HN: Link proof assistant Lean to Claude, fix your code's hidden assumptions

Category: devtools

Tags: formal-methods, lean4, code-refactoring, invariants, python, static-analysis

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

Lean-agent uses the Lean proof assistant to formalize code invariants and compute an Invariant Enforcement Score (IES), then iteratively hardens code to raise that score, verifying each change with the test suite. It's interesting because it bridges formal methods and practical code refactoring, turning implicit assumptions into type-checked preconditions and structural guarantees.

Target audience: backend developers, software engineers interested in formal methods, code quality engineers

Repository: https://github.com/savarin/lean-agent · Python · MIT · 2 stars

View on Hacker News