iiinova — where your digital self keeps evolving

Mike Dodds @m-dodds.bsky.social · 26/08/2026

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

040

Mike Dodds @m-dodds.bsky.social · 26/08/2026

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

050

Mike Dodds @m-dodds.bsky.social · 18/03/2026

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

011

Mike Dodds @m-dodds.bsky.social · 05/03/2026

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

GitHub - septract/claudes-cycles-lean

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

130

Mike Dodds @m-dodds.bsky.social · 22/02/2026

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

GitHub - OathTech/lean-tcb

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

130

Mike Dodds @m-dodds.bsky.social · 10/10/2025

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

mikedodds.org

Experimenting with ACL2 and Claude Code

TL;DR: Using only prompting with Claude Code, I created: 50+ ACL2 theorem proofs translated from Software Foundations An MCP server for ACL2 with stateful solver sessions

070

Mike Dodds @m-dodds.bsky.social · 16/09/2025

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

galois.com

Claude Can (Sometimes) Prove It

1165

Mike Dodds @m-dodds.bsky.social · 16/07/2025

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

Screenshot of article text: “Formal verification today is very useful, but for most systems it’s very difficult to write the kinds of complete specifications that verification needs. However, other kinds of specifications are popular: for example, a test case is a kind of limited, partial specification. The key is that a test case is immediately useful, and doesn’t impose undue costs on the development team. We need to find ways to specify systems that have these virtues, and avoid the trap of imposing a complete and coherent view that fundamentally does not exist.”

Screenshot of article text: “ I’ve come to think writing formal specifications is just a very difficult task. It requires a top-down view of the system that designers and engineers typically don’t have or, more importantly, need. In contrast, informal specifications can be ambiguous, partial, flexible. Informal specifications are intended as communication mechanisms between humans, and as a result they can be ‘wrong but useful’, and elide aspects of the system that are not of interest. This is a strength, but it also results in systems that can’t be easily formalized.”

Screenshot of article text: “ I think systems are typically both designed from the top and grown incrementally. Most systems have some degree of top-down structure, but few systems have a mathematically coherent specification that covers every behavior. The effect is that most systems obey some formal specification for some core functionality, but if outside this core, we rapidly enter muddy territory where it is unclear what the system should do, or whether the designer should even care”

Screenshot of article text: “ It’s a formal verification cliché that writing the specification tends to uncover most of the bugs in a system. To me, this suggests an analogy between specification and programming—both are tools for expressing what we want. In one way, this is a pessimistic thought: no tool can remove the burden of clarifying our ideas. But also, it gives me some hope. Programming is very difficult, but through careful tool design, we’ve made it available to hundreds of millions of people. With luck and skill, perhaps we can do the same for specifications.”

071

Reposted by Mike Dodds

Hazel Weakly @hazelweakly.me · 25/06/2025

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

1134

Reposted by Mike Dodds

Galois @galoisinc.bsky.social · 27/05/2025

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

A labyrinth icon, serving as a metaphor for the process of formal verification

012

Mike Dodds @m-dodds.bsky.social · 24/05/2025

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

A graph of costs and benefits plotted against each other. There is a line under which is “Your favourite under-appreciated formal method”. There are two arrows pointing orthogonally away: “be cheaper” and “be more beneficial”

151

Reposted by Mike Dodds

Galois @galoisinc.bsky.social · 08/05/2025

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

034

Reposted by Mike Dodds

Galois @galoisinc.bsky.social · 14/04/2025

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

godbolt.org

Compiler Explorer - C (C2Rust (master))

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

1132

Mike Dodds @m-dodds.bsky.social · 29/01/2025

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

071

Mike Dodds @m-dodds.bsky.social · 20/01/2025

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

2141

Mike Dodds @m-dodds.bsky.social · 20/01/2025

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

1110

Mike Dodds @m-dodds.bsky.social · 21/12/2024

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

332

Mike Dodds @m-dodds.bsky.social · 17/12/2024

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

1175

Mike Dodds @m-dodds.bsky.social · 15/12/2024

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)

181

Reposted by Mike Dodds

Sam Tobin-Hochstadt @samth.bsky.social · 15/12/2024

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.

39711

Mike Dodds @m-dodds.bsky.social · 01/12/2024

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

051

Reposted by Mike Dodds

Swarat Chaudhuri @swarat.bsky.social · 29/11/2024

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

2309

Reposted by Mike Dodds

ionchy @ionchy.ca · 27/11/2024

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

7565

Mike Dodds @m-dodds.bsky.social · 26/11/2024

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”

160

Mike Dodds @m-dodds.bsky.social · 24/11/2024

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

010

Mike Dodds @m-dodds.bsky.social · 22/11/2024

Pretty, pretty, pretty good

A pair of empty chairs in a theatre before a live show, with a sign above it showing Larry David and “Curb Your Enthusiasm”

030

Mike Dodds @m-dodds.bsky.social · 21/11/2024

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

galois.com

Function Argument Nullability Using an LLM - Galois, Inc.

by Mark Tullsen, Stuart Pernsteiner, and Mike Dodds Overview We think that Rust is a great language, and maybe you agree! Unfortunately, even if you do, there’s a good chance whatever application you’...

040