RT
@maxvonhippel: 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!
