Mike Dodds
@m-dodds.bsky.social
Formal methods nitwit. https://mikedodds.github.io
AI / math / formal methods paper feed: @ai-fm-papers.bsky.social
AI / math / formal methods paper feed: @ai-fm-papers.bsky.social
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...
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
mikedodds.org
October 9, 2025 at 11:48 PM
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...
Claude Can (Sometimes) Prove It
www.galois.com
September 16, 2025 at 10:46 PM
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...
July 16, 2025 at 12:48 AM
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...
Reposted by Mike Dodds
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 :)
I saw a *ton* of parallels with resilience engineering too :)
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...
What Works (and Doesn't) Selling Formal Methods
www.galois.com
June 25, 2025 at 1:25 AM
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 :)
I saw a *ton* of parallels with resilience engineering too :)
Reposted by Mike Dodds
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...
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...
May 27, 2025 at 5:56 PM
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...
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...
May 24, 2025 at 2:12 AM
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...
Reposted by Mike Dodds
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...
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...
May 8, 2025 at 4:32 PM
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...
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...
Reposted by Mike Dodds
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
April 14, 2025 at 2:52 PM
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...
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.
www.wsj.com
February 6, 2025 at 5:21 AM
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
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-...
Learn more:
www.galois.com/articles/o3-...
January 29, 2025 at 11:24 PM
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
- 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
January 20, 2025 at 9:52 PM
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
- 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
January 20, 2025 at 8:09 PM
I’m bringing these cute Galois stickers to POPL so if you want one, come find me
Reposted by Mike Dodds
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
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
December 21, 2024 at 5:19 PM
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
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/...
December 17, 2024 at 3:10 AM
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)
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.
December 15, 2024 at 5:48 PM
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)
Reposted by Mike Dodds
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.
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
December 15, 2024 at 2:32 PM
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
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
December 4, 2024 at 9:58 PM
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
December 1, 2024 at 4:41 AM
AI personas are getting eerily accurate cc @jmct.bsky.social
Reposted by Mike Dodds
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...
drive.google.com/file/d/1ybQx...
November 29, 2024 at 2:37 PM
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...
drive.google.com/file/d/1ybQx...
Reposted by Mike Dodds
❌ all transpilers are just compilers
✅ all compilers are just transpilers
✅ all compilers are just transpilers
November 27, 2024 at 12:58 PM
❌ all transpilers are just compilers
✅ all compilers are just transpilers
✅ 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”
Typical X post: “an AI hacked my social bonding protocol and now Claude is my only friend”
November 26, 2024 at 5:04 AM
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”
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
November 24, 2024 at 7:48 PM
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
November 22, 2024 at 3:35 AM
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
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
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’...
galois.com
November 21, 2024 at 10:38 PM
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
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