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.
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.
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.
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.
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 namin@seas.harvard.edu if interested. Include a CV and GitHub link.
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.
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?
Definitely, it is something we are super focused on as it seems to be a use case that is important for folks. Opening up the proxy server and adding local LLM support is my main focus for today and will hopefully update on this comment when it is done :)
Ollama support would be amazing. There's a stack of people in organizations (data rich places) who would likely love something like this, but who cannot get to OpenAI due to organizational policies.
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.
