namin

Thanks, we will provide case studies. Already today, lemmafit doesn't need familiarity with Dafny. It is used under the hood, so you just use Claude Code normally and lemmafit adds the verification harness. You don't need to interact with Dafny or the proofs at all.

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.

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.

Ha. At least you can check the theorem statements and see that the proofs verify :)

Harvard SEAS | https://metareflection.seas.harvard.edu and https://namin.seas.harvard.edu | Postdoctoral Fellow | Greater Boston Area | ONSITE

I am looking for a postdoctoral fellow interested in the intersection of programming languages and artificial intelligence, in particular verification and large language models.

Our main goal is to create a PL+AI system that is the best at verified program synthesis. We will use the verification-aware programming language Dafny and co-evolve an LLM and a discovery system for Dafny.

Please contact me at [email protected] if interested. Include a CV and GitHub link.

Harvard SEAS, ONSITE (Boston area, MA, US)

I have one opening in a new project around AI for precision medicine. One thrust is about combining biomedical knowledge graphs and large language models into a biomedical-fluent core platform. Another thrust is about UI for data-rich programmable systems. The opening is for either a research engineer or a postdoc, with different criteria in each case. The research engineer would be responsible for quarterly demo-driven deliverables. The postdoc would be expected to develop a research agenda with these applications in mind.

Contact: [email protected]

Awesome, thank you! I'll check it out.

This seems cool! Is there a way to try it locally with an open LLM? If you provide a way to set the OpenAI server URL and other parameters, that would be enough. Is the API_URL server documented, so a mock a local one can be created?

Thanks.

Not dumb! The verifier lets slide an error on the last line, while it's still in progress.

Yes. The verifier check already ensures syntactic correctness, but the search could goes faster if the underlying LLM doesn't generate bad syntax to begin with.

> How does the MCTS distinguish between 'generated a stupid lemma that is true' and 'generated a valid lemma'?

It does not, though I would like to add validation as part of the check as future work.

> Is there any reason to expect that a 'good' partial subtree will result in a 'good' output?

Yes. I am using Phind Code Llama and it generates a lot of invalid Dafny out of the box. Now, all these false starts get pruned.

I do suspect that if we try to scale this to Coq proof, we will run in local optima rabbit holes.

> Why do you think this approach will generate valid lemmas? > (Not structurally valid; valid as in, they assert a solution to the given problem).

Because the LLM tries to follow instructions.

> "Generate me a function for X and a bunch of tests that verify X". > "If the tests pass, the function is good" > ...but, there's no specific reason to expect that to be true?

Indeed, there are complementary approaches like Speculyzer that help validate specs and code at once.

> How is what you're doing different?

That's not the problem I am solving at the moment. What I solve is that I am able to generate verified code (that still need to be inspected) while the LLM struggles to do in one go.

> I guess I'm struggling to see how this is superior / novel to existing approaches in that space.

It's not that novel, see the planning in LLM work that I credit in the README.md. This transfers from a setting of checks by tests to a setting of checks by a verifier. The code is very simple, and it actually brings open models to reliably solve problems that even ChatGPT only sometimes solve. I think it's a good foundation to build more sophisticated verification with LLMs.

Interesting! Is the end goal similar to the outlines library: https://github.com/outlines-dev/outlines ?

Thanks. I adapted this old MCTS library: https://github.com/ImparaAI/monte-carlo-tree-search which is also very short and understandable.

Thanks for taking a look!

This is not the main loop. This just generates one completion that succeeds (or gives up) deferring to the Dafny checker to decide.

The main loop is the simulate function of the MCTS library. https://github.com/namin/llm-verified-with-monte-carlo-tree-...

The main advantage of MCTS is that it takes care of the exploitation/exploration trade off based on the scores propagated by the child finder.

I hope this helps. Let me know if this addresses your question.