Some personal news: I’ve left @galoisinc.bsky.social to start Oath Technologies / @oathtech.bsky.social, a new FRO that will work on AI oversight via formal methods

How do we use AI to build formal tools? Notes from a few months of building semantics, verifiers, and proof toolchains with AI agents doing most of the work oath.tech/pub/2026/08/...

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...

GitHub - septract/claudes-cycles-lean

Contribute to septract/claudes-cycles-lean development by creating an account on GitHub.

github.com

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)

GitHub - OathTech/lean-tcb

Contribute to OathTech/lean-tcb development by creating an account on GitHub.

github.com

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 :)

Susan Potter@susanpotter.net · last yr.

Nobody cares about correctness and do cheap things first are great takeaways from this but this article illustrates these and other points especially well: www.galois.com/articles/wha...

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

Compiler Explorer - C (C2Rust (master))

/* Type your code here, or load an example. */ int square(int num) { return num * num; }

godbolt.org

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

Why Amazon is Betting on ‘Automated Reasoning’ to Reduce AI’s Hallucinations

Amazon is using math to help solve one of artificial intelligence’s most intractable problems: its tendency to make up answers, and to repeat them back to us with confidence.

wsj.com

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

Galois@galoisinc.bsky.social · 2y ago

OpenAI recently announced their new model, o3. Most media attention focused on its impressive results on the ARC-AGI benchmark, but for us at Galois, the most significant result was the model’s 25% score on a benchmark called Frontier Math. Learn more: www.galois.com/articles/o3-...

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

emojikitchen.dev

Emoji Kitchen - Browse Google's unique emoji combinations

Unique illustrations of combined emoji, cooked up in Google's Emoji Kitchen, and comprehensively available on the web

emojikitchen.dev

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)

Sam Tobin-Hochstadt@samth.bsky.social · 2y ago

Also I think a lot of people who are hostile to the existence of modern LLMs and hope they will go away aren't aware that you can effectively download and run the original chatgpt on your laptop now, for free.

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.

Kevin A. Bryan@afinetheorem.bsky.social · 2y ago

Super excited to publicly launch "All Day TA" (http://www.alldayta.com), a product @joshgans.bsky.social and I have been working on with our team over the last year. Short version: if you teach in spring, you will want to use this! It's the future of higher education. A short thread: 1/x

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

Verifying Cake-Cutting, Faster

Envy-free cake-cutting protocols procedurally divide an infinitely divisible good among a set of agents so that no agent prefers another's allocation to their own. These protocols are highly complex a...

arxiv.org

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