This is a cautionary tale.

Act I

My latest paper “Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic” involved quite a lot of proof work. In that paper we showed how you can use program logic techniques to prove stuff about a particular implementation of real numbers (lazy bitstreams), and we formally verified it using the Iris framework in Rocq.

The core “program logic” nugget at the heart of this paper is really simple and elegant; of course, this is because Joe went “wolf mode” and cooked this part of the project over a single weekend. My main contribution to the paper was exploring how far this trick could get us, in the end scaling all the way up to verified implementations of cool and counterintuitive sampling algorithms.

In particular, I spent a couple months hacking on this idea, and of course, going completely insane in the process. Through tears I verified the existence of, and absolute convergence of, and commutation of, ten thousand different Riemann integrals in Rocq, working around the scant and inconsistent support for them in our analysis libraries. I was not a heavy user of AI at the time–this mental torture was sourced organically. As an effect (aside from forgetting the feeling of joy) but I knew pretty much every line of this repository inside and out.

Act II

Because of our weird representation of real numbers our adequacy theorem, the main metatheorem relevant for correctness of program logics, had to be stated in a somewhat nonstandard way. The statement is more or less as follows:

Theorem Adequacy.

• Let e be a program, and mu be a proper distribution over R.
• Let P/2^Q be any dyadic rational number.
• Suppose you prove HasDistribution(e, mu) (the main “judgment” of our logic).
• Suppose that IsLessThanDyadic(e, P/2^Q) terminates with probability 1.

Then, the probability that IsLessThanDyadic(e, P/2^Q) returns true is equal to cfd(mu)(P/2^Q)

All of the weirdness has to do with IsLessThanDyadic, a necessary layer for simulating real numbers in a language that doesn’t have them. The program IsLessThanDyadic works by iteratively comparing approximations of the real number returned by e against approximations of P/2^Q. For example, if P/2^Q is the dyadic binary number b0.110111..., the program will iteratively compare increasingly finer approximations of e against it, until the first comparison that decides which side that e lands on:

• b0.0 < e < b0.1?
• b0.10 < e < b0.11?
• b0.110 < e < b0.111?
• b0.1100 < e < b0.1101?
• and on and on

Of course, when e is randomly sampled from a sufficiently nice probability distribution like the Gaussian, the chance that it exactly equals P/2^Q is zero, so a simple inductive argument justifies that the obvious implementation of IsLessThanDyadic really will terminate with probability 1 as required. And it’s easy to justify to yourself (and inside our logic) that this process will output true if e < P/2^Q and false if P/2^Q < e. By appealing to some elementary measure theory, the fact that we know IsLessThanDyadic(e, P/2^Q) for every dyadic number P/2^Q is enough to characterize the cumulative density function of e over the entire real line, and so the proofs we carry out inside our logic are the real stuff.

Our final artifact includes random sampling algorithms for the real-valued, honest-to-god Gaussian and Laplace distributions, and a library of verified arithmetic complete enough to fill an unverified hole in prior work. At the time we submitted I was super proud of this result, especially given how much work I’d put in to making every little detail of the math come together.

The reviewers agreed it was cool, and it was accepted. Yay!

Act III

While our adequacy theorem is nice, that fourth bullet point is sort of weird, and we highlighted in our paper that a separate tool such as Total Eris would have no issue demonstrating that IsLessThanDyadic(e, P/2^Q) terminates with probability 1 in Rocq. Come rebuttal time we decided to actually sit down and do it, at least for the uniform sampler over [0,1]. So there I was, sitting in a hotel room in Providence, hacking away on a Total Eris proof when I realized

Act FUckfuckfuckfuckfuckfu

Our implementation of IsLessThanDyadic was NOT comparing increasingly more precise approximations of P/2^Q. Due to a sign error in our code, it was checking the outcome of e against increasingly coarser approximations of our dyadic:

• 0 < e < 1?
• 0 < e < 2?
• 0 < e < 4?
• 0 < e < 8?
• And on and on forever, haha, uh oh, I’m in danger

Worse than just being unprovable, the program actually just plain did not terminate!

Why did the proof checker still accept this? Well, Eris is a partial correctness logic, so it trivially accepts anything about nonterminating programs (indeed, partial correctness is necessary for the logic’s main trick to work). Loeb induction, the principle we use to verify properties about IsLessThanDyadic in Iris, simply assumes that your program is in a terminating trace, causing the termination assumption to bubble all the way up to the adequacy theorem–the point where we waved it away. When you’re in the muck of a Loeb induction proof, a correct proof and a proof that is vacuous due to nontermination look just about the same.

You can prove anything about nonterminating programs using Loeb induction, but it will not be possible to close off that final termination hypothesis in your adequacy theorem. This is exactly the situation I was in, that horrible night in Providence.

The paper could simply not be published in this state, and I was mentally preparing myself to retract our submission.

Act V

I freaked out for a little bit, but then I stopped freaking out and corrected the sign error, and surprisingly the adequacy theorem still compiled. Then I was able to sit back down finish the Total Eris proof, closing the last hypothesis.

Act… what the hell?

I thought the same thing.

While the proof I’d written was vacuous, I’d actually still written a correct proof, just in a vacuous context. With the sign errors corrected, nothing needed to be modified about my partial correctness arguments, but my termination statement switched from being false to being true (a good change to make, generally speaking).

The main reason this did not become a tragedy was because I did not “adversarially exploit” the Loeb induction hypothesis. In fact, the final proof still went through by Loeb induction, and parts of it genuinely rely on the fact that we can avoid traces that don’t terminate (such as the zero probability case that e samples any dyadic rational number P/2^Q exactly).

It can be hard to decide what is an exploit versus a correct proof, but it’s important for proof engineering that you know the difference. This mistake was not a big deal but it very easily could have been. The months I spent mentally torturing myself with the details of these arguments meant I understood them completely, and I knew that even if not correct, they were fixable. So that’s exactly what I did.

A couple hours later, we submitted the rebuttal confidently asserting that yes, we also verified the obvious hypothesis too.

Close one, cowboy.

Conclusion

This is a cautionary tale. Now that AI is readily available, and generally pretty good, some people believe that you can simply slop out a proof and submit it for the extra badges on your cover page. I’m not sure I would have noticed an AI that decided to avail itself of my nonterminating program. I’m quite sure I would not have been able to fix it so quickly–the time alone to regenerate a correct version from scratch would probably have even been too long.

You have to be careful with these things. Formal methods is still hard, and you need an expert to interpret the results. And when your slopped out artifact doesn’t exactly match the text of your paper, I’ve got to say, the once-bitten part of me just doesn’t buy it.