A lot has changed in formal verification this year, and it has two sides. Proofs got much cheaper. And expensive proofs were how we found bad specifications.

Most of what is written about it is only about the first side. This post is about the second. As an example I take my own project.

What changed

In April I wrote about how I let LLMs do proofs. The setup is an agent that reads the Rocq proof state, tries a tactic and knows at once whether it works. Back then it managed arithmetic on its own. With VST tactics it was still bad.

Four months later both work (kind of). For me that is around 22,000 lines of Rocq in libshrincs: a VST proof for a C implementation and an SSProve security proof, most of it written by LLMs. Goals that used to take a day now close on their own.

That is not only down to my setup. Everyone in formal methods seems to be doing something like this right now. Baudart et al. used the same kind of setup to prove 10 of 12 Putnam problems from 2025 in Rocq. That is much harder than anything I do.

The upside

Grinding tactics was always the slow part of formal methods. And a big reason why so little gets verified.

The effort is much smaller now. Before I complain: this is great. Work few could afford before is now within reach. Still not cheap. The two of us verifying a C implementation and a security proof against one shared model, that just did not work on the old budget. I would not have tried.

The proofs are from LLMs. The model, the bridges, the public contracts and the game statements are not, those are by hand.

The grind is not completely gone either. Proofs break, and then I have to understand one I never wrote. That takes time too. That is what the proof style is for, which I force on everything the LLMs produce: what comes back should have a shape I can read and debug.

And the line I have just drawn is cleaner in theory than in practice. With the helper lemmas I catch myself generating the statement too, because there it matters less anyway. How well I can judge where that is true, I do not know myself.

Nothing checks a specification

A proof that does not work is harmless. The tool notices it, you lose time. Dangerous is a proof that goes through for the wrong statement. No proof assistant has ever caught that one. The kernel checks whether your proof shows your theorem. Whether your theorem says what you mean is not its job.

Until now the grind found it. If you sit on a proof for a week, you read your own definitions for a week. And somewhere on the third day you notice: what you wrote down is not what you mean. Slow, late and by accident. But nothing else was checking.

Now Qed comes back and nothing complains. A wrong statement goes through just as fast as a right one.

And it gets worse. Projects get bigger, because you now take on things that were too expensive before. The statements grow with them. Bigger statements are more easily wrong, there are more of them, and almost nobody reads each single one any more.

The part I miss

A week of grinding and Qed at the end, that felt really good. Almost ecstatic. I was proud of those proofs, of the current ones I am not.

More than once the missing step came to me in the morning, in the half hour between sleeping and waking. I got up and it worked. Your head keeps working even when you are not sitting at it, and delivers the answer when you are not asking.

That does not happen any more. Nothing stays in the head long enough.

Who can check them

Some people wonder whether a model can review the specification. I do not trust the result. LLMs agree with you far too quickly. They will just as happily explain to you why your definition makes sense as tell you that it is wrong. I cannot tell the two answers apart.

That can get better. But it is a different kind of error than a made-up tactic, because here nothing checks the answer.

So people are left, and there is the catch. Writing a big theorem correctly is a skill of its own, and you learn it by writing proofs. Which we now do less and less.

The path is still open. It starts as always: with natural numbers and lists, where the theorems are small enough that being stuck costs nothing and the lesson still lands. What is new is that you have to decide actively, against an LLM that takes the exercise off your hands the moment you ask. It is like studying with the solutions open next to you. You read them every time. Everything makes sense. Then the exam comes. I speak from experience. Whoever skips the path ends up writing statements nobody can understand. Yourself included.

Fewer and smaller statements

If nothing checks the specification, you can only do one thing: have fewer and smaller ones, and put them where somebody really looks. That is exactly why libshrincs is built the way it is. An example, not a solution:

• One definition that both proofs point at. The two proofs agree because they share one file of 366 lines. Nobody has to compare two documents by hand.
• A few bridge files, where a reviewer checks whether the two halves describe the same thing. Four of them, against 22,000 lines of proof.
• One allowlist with all the assumptions, mine and the ones the libraries bring along, and a build step that compares what the proofs really assume. If a new one shows up, the build breaks.

That does not make the statements right. They only become few and small enough that somebody could check them. More than that is not possible here.

What I want

We have to notice that we lost a detector, and replace it on purpose. The time we save now should go into reviews.

The other thing: teaching has to change. The courses I learned with, in more than one proof assistant, are all built on closing goals. Here is a lemma, write the tactics. That was right as long as the tactics were the expensive part and the statement fell out along the way.

The expensive part is somewhere else now. Two things you have to practise today: writing the statement down correctly, and building the proof far enough that something else finishes it: the induction, the case split, the place where the invariant has to get stronger. Finishing it, a model can do well. Deciding what has to be shown at all, and in what form, it does badly.

How such a course looks, I do not know. But these are new exercises, not the old ones with hidden solutions.