[Update] LemmaScript, Discord, BugBash, and more!
Hey,
We have enough updates to warrant taking up room in your inbox.
First up: LemmaScript. lemmafit is incredible for greenfield projects, but we wanted to explore a way to more easily approach brownfield projects, without the overhead of integrating the Dafny runtime into running code. Specifically, we wanted to get a closer correspondence between the code that gets proved and the code that already runs. So, naturally, Nada built a compiler that models TypeScript in Dafny, opening up verification as a complementary pipeline rather than taking over the compilation pipeline. You can read about it here.
Next: Discord Server! A couple of months ago, someone told me we should start a Discord. Looking back, we should have done that two months ago! Now we have one. It's invite-only so we can keep the conversation high quality and engaging. The formal verification + AI space is moving fast and a million ideas and opinions are flying around. We're open to all of them. Here's the invite form. If you already submitted a request (thanks!), you'll get an invite to the server soon.
Finally: BugBash Today, Nada and I gave a seminar at BugBash titled "Integrating formal verification into AI-assisted development workflows". There were no empty chairs and several people standing — including some top leaders in the field. It was a lively discussion and we feel more energized than ever. Tomorrow, I'll be giving a Lightning Talk on integrating formal verification seamlessly into a web dev workflow.
If you're at BugBash, come say hi!
Up next: lemmacore Cursor for verified program logic core. We handle the verification overhead, your agent builds the shell around it. Stay tuned.
As always, we love replies and thoughts. Even if those thoughts are that we are out of our minds.
Til next update,
fernanda