Mike Dodds

8.8K posts

Mike Dodds banner
Mike Dodds

Mike Dodds

@miike

Formal methods enthusiast. Principal scientist at @Galois. English immigrant. Nitwit. Opinions my own.

Portland, OR Katılım Şubat 2008
598 Takip Edilen1.2K Takipçiler
Mike Dodds
Mike Dodds@miike·
@intoverflow Right, one of the intriguing things is the agents might find a much shorter proof! Or a much longer one for that matter. My guess is the agents need abstractions just the same as humans so it wouldn’t just be a big incomprehensible blob
English
0
0
1
32
Mike Dodds
Mike Dodds@miike·
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 the AI the seL4 code + top spec, and re-synthesise the whole 1m+ line Isabelle proof
English
3
7
57
6.8K
cmr://ember
cmr://ember@ember_arlynx·
@miike love this idea! happy to collab w/anyone wanting to experiment with this (former sel4 contrib)
English
1
0
2
48
Mike Dodds
Mike Dodds@miike·
Fun exercise: predict what year an agent with sufficient scaffolding could reconstruct the entire seL4 proof. Estimates at Galois ranged from “2040” to “this year” :)
English
4
3
8
1.4K
Mike Dodds
Mike Dodds@miike·
@SMT_Solvers I guess I mean how do you trust your spec vs real libc? libc spec is deliberately under-specified and also relies on the semantics of kernel syscalls, global memory state, many hard problems
English
1
0
0
16
Chad Brewbaker
Chad Brewbaker@SMT_Solvers·
@miike Like any proof you just have to trust it up to axioms and proof kernel.
English
1
0
0
17
Mike Dodds
Mike Dodds@miike·
@SMT_Solvers csmith is an amazing tool! Another v useful project would be “csmith for everything” - quickly stand up generators for arbitrary input languages (maybe this already exists?)
English
0
1
0
226
Mike Dodds
Mike Dodds@miike·
@SMT_Solvers This would also be extremely useful & presents some interesting problems. Eg, how could you get an agent to help? How would you trust the spec afterwards?
English
1
0
1
46
Chad Brewbaker
Chad Brewbaker@SMT_Solvers·
@miike More fun excercise. Spec libc in enough detail that you can make safer C software at scale.
English
1
0
0
49
Mike Dodds retweetledi
Ilya Sergey
Ilya Sergey@ilyasergey·
New on "Proofs and Intuitions": Verifying Move Borrow Checker in Lean: an Experiment in AI-Assisted PL Metatheory. proofsandintuitions.net/2026/03/18/mov… The gist: I formalised Move's type system in Lean: 39KLOC, under a month, with Claude. Person-years in PL research are now person-weeks.
English
9
44
230
17.5K
Mike Dodds retweetledi
Arpit Gupta
Arpit Gupta@arpitrage·
Leopold Aschenbrenner predicted in June 2024 that we would get a dramatic improvement in AI capabilities around the turn of 2026 due to the switch from chatbots to agents, which he thought would unlock a new set of AI capabilities Which is basically exactly what happened?
Arpit Gupta tweet mediaArpit Gupta tweet mediaArpit Gupta tweet media
English
49
146
1.8K
139.5K
Mike Dodds retweetledi
roon
roon@tszzl·
@memeticweaver @tautologer > the USG can in general do whatever they want the founders of this great nation fought several bloody wars to make sure this is not true
English
22
38
938
51.2K
Mike Dodds retweetledi
Josh RR Jokien
Josh RR Jokien@joshcarlosjosh·
“I wish it need not have happened in my time,” said Frodo. “lmao" said Gandalf, “well it has.”
English
264
26.1K
89.8K
0
Niels Mündler
Niels Mündler@nielstron·
@miike @HarmonicMath wait they... are open now! I requested access and never got a mail that I got approved - I guess because I dont have to now.
English
1
0
2
42
Mike Dodds retweetledi
Axiom
Axiom@axiommathai·
1/ RELEASING AXLE: the Axiom Lean Engine ⚙️ We are serving our core Infrastructure for formal proving at scale. These are the same Lean metaprogramming tools that are behind AxiomProver, powering it to win Putnam and crack open research conjectures. Available to anyone today!
Axiom tweet media
English
11
66
427
110.9K
Mike Dodds
Mike Dodds@miike·
This isn’t the fully general theorem about all 760 such decompositions (what Knuth proves) - just the single construction that Claude found. If I get another sick day tomorrow I might try to prove the general result :)
English
2
0
5
378

Keşfet

@intoverflow @ember_arlynx @qd_forall @SMT_Solvers @memeticweaver @tautologer @nielstron @HarmonicMath