An Anecdote Against Slop Artifacts

Aug 14, 2026

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 ?

b0.10 ?

b0.110 ?

b0.1100 ?

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 and false if P/2^Q . 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 ?

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...

An Anecdote Against Slop Artifacts

Related Articles

(no title)

Scientists reverse brain aging, with a nasal spray

NHS apologises and admits Palantir have access to identifiable patient data

AI has torched the market for junior programmers

Al Vigier: Canada's AI strategy shouldn't include secret Palantir bills