Someone should build seL4-ablate-bench. Progressively delete proofs, lemmas, theorems and see how much a long-running AI agent can reconstruct. End state: just give it the code + top spec, and rebuild the whole 1m+ line Isabelle proof

I formalised the Knuth / Stappers / Claude theorem in Lean4. Claude for scaffolding and Harmonic‘s Aristotle AI for the core proofs This is just the construction Claude found, not all 760 constructions (Disclaimer: theorems look plausible to me, but mistakes possible) github.com/septract/cla...

Weekend project w/ Claude: in Lean, it can be hard to know which definitions you need to review to trust a theorem. So I built lean-tcb. It figures out your trusted computing base, ie the definitions that actually give a theorem its meaning (vs proof machinery the kernel checks)

I got curious whether Claude Code could handle a low-representation theorem prover like ACL2 - turns out yes! I proved a bunch of small to medium theorem, and for good measure built a MCP server, all in about 4 hrs. I’ve never used ACL2 before. Write-up here: mikedodds.org/posts/2025/1...

I wrote about Claude Code, which to my absolute astonishment is quite good at theorem proving. For people who don't know theorem proving, this is like spending your whole life building F1 engines and getting lapped by a Tesco's shopping trolley www.galois.com/articles/cla...

New Galois blog: “Specifications Don’t Exist”. If we want to formally verify more systems, we need formal specifications, but most real systems are hard to specify for very deep reasons www.galois.com/articles/spe...

I’m not sure how I missed this but it’s an extremely good article and you should absolutely read it. It’s about formal methods, but anyone who cares about integrating research into industry will find it valuable! I saw a *ton* of parallels with resilience engineering too :)

At Galois, we often say things like: “Formal methods form the backbone of everything we do.” But what exactly are formal methods? How do they work, and why are they so important? We created a handy reference page to explain: www.galois.com/what-are-for...

New-ish @galoisinc.bsky.social blog: “What Works (and Doesn't) Selling Formal Methods”. The boring truth: engineers are rational and adoption is all about cost/benefit tradeoffs www.galois.com/articles/wha...

What actually works when selling formal methods in industry? What doesn't? The way Galois Principal Scientist @m-dodds.bsky.social sees it, many FM projects don’t pencil out not because clients are irrational, but because the cost/benefit tradeoffs don’t make sense. www.galois.com/articles/wha...

c2rust is available on the Godbolt Compiler Explorer! c2rust is a tool we developed with Immunant that can convert nearly any piece of C code into compilable Rust godbolt.org/z/crsWEGEKM

Formal methods go great with AI www.wsj.com/articles/why...

I wrote about o3, the Frontier Math benchmark, and what it means if AI math keeps getting better

Hot take for POPL: the PL community is still mostly in denial about AI. This is bad because PL+AI go great together - PL can solve the hardest problem with AI - trusting the output it produces - AI can solve the hardest problem with PL - finding enough engineers who can even use the tools

I’m bringing these cute Galois stickers to POPL so if you want one, come find me

Re o3 - this is the big one for me. The Frontier Math benchmark is designed to be extremely difficult, and it has a private test set (no data contamination). Today, o3 is v expensive. But seems inevitable it’ll soon be cheap. If these results hold up, that means MUCH more powerful automated math

I gave a talk recently about proof technologies - what people deploy today, what might be available soon, and what seems far off even with fancy AI. Slides here: mikedodds.github.io/files/talks/...

I have had conversations with professor types who say “oh I don’t think an LLM will be able solve <whatever> for a long time” and I show them the base ChatGPT model doing <whatever> first time with simple prompting. Many people’s intuitions are stuck (especially LLM critics)

I think many of the (quite gross) reactions to this are not grappling yet with how many their students already have what they think is this product in the form of chatgpt.

One of my favourite papers recently: “Verified Cake-Cutting, Faster” arxiv.org/abs/2405.14068

AI personas are getting eerily accurate cc @jmct.bsky.social

Since all my Twitter content is now gone, I will start reposting some of it here. Here are the slides for my talk on the coming wave of ML-accelerated formal methods, given at the Isaac Newton Institute last month. May interest some of you. drive.google.com/file/d/1ybQx...

❌ all transpilers are just compilers ✅ all compilers are just transpilers

Typical Bluesky post: “I went out on my bike today” Typical X post: “an AI hacked my social bonding protocol and now Claude is my only friend”

I’ve been reading a lot AI / math / formal methods papers, so I made an account @mdai.bsky.social to post them

Pretty, pretty, pretty good

New post: Function Argument Nullability Using an LLM Writing a static analysis is annoying so what if you just asked an LLM instead? Turns out GPT-4o is good at analysing simple properties. Cheap to build, expensive to run, makes some mistakes. But for some applications, that’s a fine tradeoff