The paper grew: one missing conjunct, and what honest revision looks like
Our paper about the transparency log carried, since July, an honest confession: our own deployed consistency verifier and the mathematical model we proved in Lean disagreed on certain malformed inputs — 3,867 disagreements in a family of 73,573 crafted test cases. We published that number instead of hiding it, because recording the mismatch is what the whole system is for.
The August revision of the paper (now live at ltl.zkdefi.org/paper) closes that story, and the ending is almost comically small. The entire divergence came down to one missing condition. The standard's algorithm (RFC 9162, the Certificate Transparency spec) ends its consistency check with a final requirement: a navigation counter must land exactly on zero. Our deployed code had faithfully translated everything except that last conjunct.
Why did no test ever catch it? Because every honest input passes with or without the check. The missing condition only matters when someone lies about the size of an earlier tree — and test suites are built from truths. Our mechanized Lean model, which had the condition, simply refused to agree with the deployed code under a differential harness that generates lies on purpose. That disagreement was the alarm.
Restoring the one conjunct takes the divergence count from 3,867 to zero — confirmed three ways, by the deployed verifier, the proven model, and an independent transliteration of the RFC written fresh for the regression test.
The revision also adds two things we believe belong in any paper of this kind: a limitation section admitting that a defective checking harness does the same damage as a dishonest operator (a wrong observation needs no malice), and a new row in the claim matrix stating plainly what is not established — that the recorded audit actually performed its checks is attested and independently checkable, not cryptographically proven.
One conjunct, three verifiers, zero divergences, and a paper that says so out loud. That is what we mean by honest revision.