Show HN: Lemmafit: Make agents prove that their code is correct

Show HN: Lemmafit: Make agents prove that their code is correct(github.com)

7 points by namin 85 days ago | 5 comments

namin 85 days ago |

Hey HN! We've been experimenting with Dafny formal verification in web apps. We've been using AI to write verified state machines, proving undo/redo preserves invariants, verifying business logic, and creating apps with this logic. That work has lived in blog posts and research experiments so far. lemmafit is the first time we've packaged it into something you can npm install.

lemmafit is an npm package that gives AI coding agents (currently only Claude Code) a formal verification loop. Any effect-free logic gets written in Dafny, verified on every save, and auto-compiled to TypeScript. The agent then hooks the logic up to a React UI, and you get an app with state transitions and business logic with guarantees of correctness.

Happy to answer questions about the verification pipeline or the Dafny integration.

Karrot_Kream 85 days ago |

Curious if there is any analysis on how often an LLM can create proofs correctly without special prompting.

namin 84 days ago | |

Since around Opus 4.5, systems like Claude Code are very good at Dafny proofs. They don’t get everything right in one shot but can iterate with verifier feedback. Some proofs take over 20 minutes to complete. The system knows to put temporary axioms to tackle proofs step by step.

Karrot_Kream 84 days ago | | |

Awesome thanks! Would be nice to have a sort of "worked example" where you take a simple project and derive Typescript and Dafny for it and have the LLM (Claude) generate proofs. Just some feedback to broaden it up to folks not as familiar with Dafny.