Where we started (left, 1979) vs. where we are now (right, 2026)

Thank god. Finally

Very touched by @ljsv89 's story and the work with @ShriramKMurthi and @JoePolitz. AI without PL and Systems foundations leads to mirages. Fundamental research is driven by curiosity, interest, and the desire to learn and to understand. Sometimes, it's hard to connect dots forward and calculate the immediate practical benefits. Most importantly, one can do fundamental research even through MOOC (see @ShriramKMurthi 's blog post: blog.brownplt.org/2013/06/18…). > the three outsiders were an undergraduate student, a professional programmer, and a retired IT professional who now does triathlons [...] from Argentina, China, and India. The result is a tested operational semantics for Python, which is used by Anthropic after 13 years. Congrats, everyone! What a story!

Do moms ever get like, thirty minutes to rest and do nothing

From the appendix: Claude, in the hands of experts, indirectly attacked the Python semantics by @JoePolitz (OOPSLA 2013) and a random gang of Brown undergrads. Seems like it survived the assault and helped bootstrap a new Claude-verified Python implementation.

Three days before I was pushed out of OpenAI I posted a Formal Verification Manifesto in a core research Slack channel. It listed OpenAI systems that could benefit from formal verification. The only person who responded was @sama, who was very supportive. Not sure what the moral of this story is, but it's never too late for OpenAI to invest seriously in software & hardware formal verification! On a more serious note, @theoremlabs and @AnthropicAI did something amazing. They showed how to verify software at scale without requiring developers to write specifications in Rocq or Lean. Instead, they used existing fuzz harnesses as specifications and LLMs to generate machine-checked proofs. Of course, fuzz harnesses specify only some correctness properties. In the simplest case, the proofs establish crash-safety, not full functional correctness. We need community-maintained open-source projects with reusable formal specifications and correctness proofs for major libraries, kernels, compilers, virtual machines and hardware. Human review of critical specifications and LLM-generated patches is essential. A model could satisfy a specification simply by removing functionality. As AI writes and rewrites critical infrastructure, formal verification should become a key part of AI control. Critical properties of AI-generated code should be machine-checked rather than taken on faith. AI is making vulnerabilities easier to find and exploit. Frontier LLMs and reusable formal specifications could finally make formal verification practical and economical at scale, while keeping it understandable to humans. Kudos to Theorem co-founders @rajashree and @diagram_chaser!

POV: you're teaching yourself ukulele to play songs for your toddler

Wild story: the Python semantics Anthropic used was defined at Brown by @JoePolitz and students from a *MOOC*. Summary here, which also explains what Anthropic depends on: blog.brownplt.org/2013/06/18… Funnily, the last sentence says, "Once again, machines may put people out of work".

Specification was always (and is especially now) the hard part of verification. This is a creative use of fuzz tests: proving (at the binary level!) that a fuzz test w/ asserts capturing functional correctness never crashes is a neat way to squeeze a lot out of an existing spec!

This is amazing

Lol I am pretty sure someone is runing a deepseek swarm to remotely patch unpatched php boxes. Well good on them.

You won't believe how many people told me over the past 10+ years that proof assistants would never achieve widespread use, and that my work was therefore not useful. Ignore people who discount entire fields of research because they are hard. All the more motivation for research

this is what has bugged me. The vulnerabilities *were there already*. We've been trying to tell people for years/decades to add types and formalize their systems to avoid this. Now that we have the tools (LLMs) to actually find these vulnerabilities, *don't blame the tool*!!