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.
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.
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?
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.
The challenge they envision to address reminds me of a section in Bret Victor's talk, The Future of Programming.
"[13:54]
So, say you’ve got this network of computers, and you’ve got some program out here that was written by somebody at some time in some language; it speaks some protocol. You’ve got another program over here written by somebody else some other time, speaks a totally different language, written in a totally different language. These two programs know nothing about each other. But at some point, this program will figure out that there’s a service it needs from that program, that they have to talk to each other. So you’ve got these two programs—don’t know anything about each other—written in totally different times, and now they need to be able to communicate. So how are they going to do that? Well, there’s only one real answer to that that scales, that’s actually going to work, which is they have to figure out how to talk to each other. Right? They need to negotiate with each other. They have to probe each other. They have to dynamically figure out a common language so they can exchange information and fulfill the goals that the human programmer gave to them. So that’s why this goal-directed stuff is going to be so important when we have this internet—is because you can’t write a procedure because we won’t know the procedures for talking to these remote programs. These programs themselves have to figure out procedures for talking to each other and fulfill higher-level goals. So if we have this worldwide network, I think that this is the only model that’s going to scale. What won’t work, what would be a total disaster, is—I’m going to make up a term here, API [Application Programming Interface]—this notion that you have a human programmer that writes against a fixed interface that’s exposed by some remote program. First of all, this requires the programs to already know about each other, right? And when you’re writing this program in this one’s language, now they’re tied together so the first program can’t go out and hunt and find other programs that implement the same service. They’re tied together. If this one’s language changes, it breaks this one, it’s really brutal, it doesn’t scale. And, worst of all, you have—it’s basically the machine code problem. You have a human doing low-level details that should be taken care of by the machine. So I’m pretty confident this is never going to happen. We’re not going to have API’s in the future. What we are going to have are programs that know how to figure out how to talk to each other, and that’s going to require programming in goals."