There's been a lot of chatter recently on HN and LW about how...
Max von Hippel@maxvonhippel
25 views
Dec 28, 2025
~2 min read
Advertisement
1
There's been a lot of chatter recently on HN and LW about how formal verification is the obvious use-case for AI. While I broadly agree, I think much of the discourse is kinda wrong because it incorrectly presumes formal = slopless. 🧵
2
I spent 5 years doing a PhD in formal methods / security, working with both model checkers and interactive theorem provers. I have written my fair share of both good and bad formal code. Formal code can be buggy and shitty in a lot of ways! It can ...
3
* prove something other than what you think it proves. For example, it's very common that you mis-define some concept such that the proof is accidentally trivial.
* model something in a way that makes proofs unnecessarily hard. For example, it's pretty common that inducting ..
* model something in a way that makes proofs unnecessarily hard. For example, it's pretty common that inducting ..
4
.. in one direction (say, car) on a list will be easy for a prover but the other direction (say cdr) will be difficult. (This is a necessary evil if you want the prover to not enter infinite rewrite loops.)
* Prove something about a model of code, where the model != the code.
* Prove something about a model of code, where the model != the code.
5
This is really common and an easy failure case for AI. "The code you wanted me to verify was too complex, so I rewrote it to be simpler and proved the simpler thing correct." Well, yeah, but the bugs I wanted you to find were in the complexity. lol.
6
* Another thing you may run into are vulns/0-days in the prover itself. There are many known instances of bugs in provers like Coq/LEAN allowing for proofs of false. Why wouldn't a sophistocated AI with goal-misalignment find and exploit such bugs? Especially in an RL context.
7
(The above point should be especially salient to folks interested in doing RL on formal math, such as @AnthropicAI and @HarmonicMath and @axiommathai )
8
@AnthropicAI @HarmonicMath @axiommathai * The AI might also introduce axioms that conflict with your priors/goals/whatever. It can do so in surprising ways, like it might inform you that boy, Cubical Type Theory would really help with this thm, and you might not know that CTT is an axiomatic shift. The prover will tell
9
@AnthropicAI @HarmonicMath @axiommathai you but you need to be prepared for this and know how to parse the error msg.
10
@AnthropicAI @HarmonicMath @axiommathai I might expand this to a real blog post in the near future but for now thought some folks on the TL might find this useful. If you're an ML person trying RL on FM tasks and want some upfront advice feel free to hit me up :).
