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 namin@seas.harvard.edu 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: namin@seas.harvard.edu

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.

You can play with the software online here: http://io.livecode.ch/learn/namin/scheme-mechanics

The notation chapter with live snippets is reproduced here: http://io.livecode.ch/learn/namin/scheme-mechanics/chapter9

What browsers are you using? Can you file an issue?

Thanks.

Apart the character of physical laws and the easy pieces, what's the gateway book to understand feynann more advanced work?

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."

http://worrydream.com/dbx/ (quote taken from this helpful transcription of the talk at http://glamour-and-discourse.blogspot.ch/p/the-future-of-pro...)

I liked the Vagrant env but I don't see it mentioned as an option here: https://docs.docker.com/installation/#installation

Are there any up-to-date installation instructions for the Vagrant env?

Quantum Computing since Democritus http://www.scottaaronson.com/democritus/

How I cancelled my phone plan in <1 minute. Me: I would like to cancel my plan. Rep: Why? Me: I am leaving the country. Rep: Congratulations! Your plan is cancelled. Best wishes. Me: Thank you!

Revised the game above: http://www.puzzlescript.net/play.html?p=6857334

And here's another game: http://www.puzzlescript.net/play.html?p=6854805

Very inspiring and fun. I just create a clone of lunar lockout: http://www.puzzlescript.net/play.html?p=6853173

http://www.infoq.com/presentations/miniKanren

miniKanren is an embedding of logic programming in Scheme. In this interactive presentation, William E. Byrd and Dan Friedman introduce miniKanren, from the basic building blocks to the methodology for translating regular programs to relational program, which can run "backwards". Their examples are fun and convincing: a relational environment-passing interpreter that can trivially generate quines, a relational type checker that doubles as a generator of well-typed terms and a type inferencer.

Does anybody know what tool he is using to make the little demo samples with the play button?

Switzerland

It seems that this 'article' is lots of copy-pasting of most of the reviews from this Amazon user: http://www.amazon.com/gp/cdp/member-reviews/A3CC0TO2YD3P5A/

Arguably, types are a form of verification, and they already lead to better optimizations.

Calculus on Manifolds by Spivak is a good book to read before (the first few chapters anyways).