If I recall correctly, I met @diagram_chaser and @rajashree at a YC event sometime around F24, which I believe was their batch. They were the second FM YC company, after us, and the first to do interactive theorem proving. To the best of my knowledge, they were the second overall company to do LLM-based ITP after @HarmonicMath . We were dealing with gpt-4o in those days, and I couldn't even get the model to write a good fuzz test, or set up a sandbox (or an AWS lambda or similar) with someone's repo. There was a bunch of demand -- we launched agentic PBT and __immediately__ had >100 users, which was way more than we could keep up with at the time -- but the tech wasn't even remotely there. I thought Jason and Rajashree were fucking nuts to be trying to actually prove stuff, when literally just testing was borderline impossible. Later, I heard rumors of research projects with Redwood and maybe ARIA, and I thought, huh, I guess that's a reasonable way to keep your company alive and learn things without taking on more non-dilutive funding. Good for them, they found a way to do the research lab thing for a while and have some fun. FM is about the fun we have along the way! But I was hella wrong to be remotely skeptical. The reality is that, Jason and Rajashree spent two years becoming state of the art at large scale agentic verification. Later, when a biglab asked me "who should we talk to if we want to do formal methods", I was like, "I mean obviously, Theorem." I think a **lot** of other people said the same thing. Who else? (To be clear, there are a couple other quite meaningful players in this space, like @axiommathai and @mathematics_inc , but they've largely positioned themselves as AI neo-labs themselves, which makes them awkward partners for a biglab, so ...) I'm not convinced that a world where we formally verify assembly code is really ideal. I am concerned it enables a world where we LLM-generate assembly, which I view as an uninterpretable and harmful outcome for humans (here I disagree with both Elon and my employer ..). I would like to believe that there are all kinds of really elegant, important properties that are best expressed over more abstract representations. But a world where we've proven *anything at all* about a giant proportion of software is actually a **massive improvement** over the counterfactual. So even if I feel inclined to nitpick the approach, the reality is that this looks like a phenomenal overall uplift in cybersecurity and a totally worthwhile and important endeavor. This is a great time to start learning formal methods. And it's a great time to work in formal methods. I really couldn't be more excited about where we're at, and can't wait to see what's next from the folks re-inventing the field!

When I think about what the future of programming looks like, I think about formal methods. It’s the natural answer to both increasing levels of abstraction and increasing needs for assurance. But what’s the future of formal methods exactly? Here are two projects I think give a glimpse: 1. Simon Henniger’s Djinn, a spec first language which reimagines logic programming in an era where the synthesis of both code and proof can be done agentically: henniger.dev/post/djinn/ . Look closely at the resulting performance gains! Making ripgrep 3% faster while being provably equivalent is not easy. 2. Sam Xifaras’s ruby semantics done quick: samx.io/blog/topics/devlog/2… . Sam smartly dodges the inevitable “@kirancodes found a bug in my semantics” moment by leading with known limitations up front — and he presents a really interesting take on how to vibe semantics, with differential fuzzing for comparison.