Formal verification in Rocq missed non-terminating logic due to sign error in real-number approximation

The paper originally presented a formally verified exact sampler for continuous distributions, implemented in Rocq using the Iris framework. The core logic was proven correct, and the artifact included verified sampling algorithms for Gaussian and Laplace distributions. However, the verification relied on a key assumption: that the `IsLessThanDyadic` function, which approximates real-number comparisons, would terminate with probability 1. This assumption was not mechanically enforced in the proof system used (Eris), which only guarantees partial correctness.

The error in `IsLessThanDyadic` was a sign mistake that inverted the direction of approximation. Instead of refining the comparison bounds (e.g., `0.1 < e < 0.11`, `0.110 < e < 0.111`), the function expanded them (e.g., `0 < e < 1`, `0 < e < 2`). This caused the function to diverge rather than terminate, violating the paper’s adequacy theorem. The proof checker accepted the incorrect implementation because Eris, as a partial-correctness logic, trivially validates any claim about non-terminating programs.

The bug was uncovered only when the authors attempted to prove termination separately using Total Eris, a tool designed for total correctness. This revealed the discrepancy between the assumed and actual behavior of `IsLessThanDyadic`. The incident underscores the fragility of assumptions in formal verification, particularly when termination is not explicitly enforced. It also demonstrates the value of complementary tools (like Total Eris) for catching errors that partial-correctness logics cannot.

For engineers, the takeaway is twofold. First, formal verification does not eliminate the need for rigorous testing or complementary proof techniques. Second, the choice of proof system matters: partial-correctness logics may silently accept incorrect claims about non-terminating code, while total-correctness tools can expose such flaws. The error also highlights the risks of manual proof work, even in highly scrutinized projects.