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
Mike Dodds
Latest posts
Claude Can (Sometimes) Prove It
Galois blog post: Link
Specifications Don’t Exist
Galois blog post: Link
What Works (and Doesn’t) Selling Formal Methods
Galois blog post: Link
o3, Frontier Math, and the Future of Mathematics (Galois blog)
Galois blog post: Link
Function Argument Nullability Using an LLM (Galois blog)
Galois blog post: Link
Generative AI for Specifications (Galois blog)
Galois blog post: Link
Galois / Twisp: Avoiding Foolishness in Distributed Systems (Galois blog)
Galois blog post: Link
The Impact of Provable Security: AWS and Supranational (Galois blog)
Galois blog post: Link
Building a Concurrency Verifier Using Crucible (Galois blog)
Galois blog post: Link