Experimenting with ACL2 and Claude Code
Published:
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
Posts by Tags
ai
formal-methods
Experimenting with ACL2 and Claude Code
Published:
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
galois
Claude Can (Sometimes) Prove It
Published:
Galois blog post: Link
Specifications Don’t Exist
Published:
Galois blog post: Link
What Works (and Doesn’t) Selling Formal Methods
Published:
Galois blog post: Link
o3, Frontier Math, and the Future of Mathematics (Galois blog)
Published:
Galois blog post: Link
Function Argument Nullability Using an LLM (Galois blog)
Published:
Galois blog post: Link
Generative AI for Specifications (Galois blog)
Published:
Galois blog post: Link
Galois / Twisp: Avoiding Foolishness in Distributed Systems (Galois blog)
Published:
Galois blog post: Link
The Impact of Provable Security: AWS and Supranational (Galois blog)
Published:
Galois blog post: Link
Building a Concurrency Verifier Using Crucible (Galois blog)
Published:
Galois blog post: Link
Who is verifying their cryptographic protocols? (Galois blog)
Published:
Galois blog post: Link
QUIC Testing, a Quick Replication (Galois blog)
Published:
Galois blog post: Link
Proofs Should Repair Themselves (Galois blog)
Published:
Galois blog post: Link
interactive-theorem-proving
Experimenting with ACL2 and Claude Code
Published:
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