If you haven't heard of Lean, it's a mathematical proof assistant. lean-refine plugs it into Claude Code to find every assumption your code makes but doesn't enforce - then fixes them one by one

Before: https://github.com/savarin/ledger/blob/67d6e236296e4787e8924...

After: https://github.com/savarin/ledger/blob/506584542d1c1c2751e2d...