The proof maintenance problem

Earlier this week, Turso, the team building a modern rewrite of SQLite in Rust and one of our design partners, merged a PR that closed a bug issue that Aretta had filed as part of verification work we have written about before. However, the aretta-ci bot reopened the issue, flagging it as "do not close". There was no human involvement, either on Turso's or our side. Why did this happen?

The gap that regression tests cannot fill#

The fix was correct for the reported bug; however, it broke a neighboring, unreported durability specification. Detecting the second break is beyond the scope of an ordinary regression test suite.

An ordinary regression test would have been enough for the reported bug. After this fix, Turso's suite would gain a test that reproduces the checkpoint bug, the fix would make that test pass, and the test would stay in the suite to detect the same behavior if it ever returned. The limit is coverage. A regression test covers exactly the property it was written for, and a suite built this way has tests only for bugs that have already been found. So after a fix that repairs the known bug but breaks something else, every existing test still passes: there is no test for the property that broke.

How Aristo caught it#

Aristo starts from the guarantee instead of from the bug history. In the first post about this engagement we showed how that works. The top-level promise is decomposed into a conjunction of smaller specifications, S ⟺ A1 ∧ A2 ∧ …, and those into smaller ones, until every leaf is something you can check against the code. A bug, in this setting, is a leaf specification found to be false.

Instantiated for Turso's write-ahead-log subsystem (the symbols are schematic, so these leaves differ from the first post's tree), the top-level promise S is that a crash never corrupts or loses committed data, and two of its leaves are:

• A1: checkpointing is crash-atomic. A crash during a checkpoint never results in a torn database file. The reported bug (issue #7952) was a failure of this specification.
• A2: a COMMIT under PRAGMA synchronous=FULL does not return until its WAL frames are fsync-durable, so an acknowledged commit survives a crash. This one had passed every check so far.

Sibling specifications like A2 are the point: nobody wrote all the leaf specifications in anticipation of a particular failure; they exist because the proof of the top-level guarantee needs them, so the model already has coverage wherever a fix might have side effects.

Re-checking the model at the fix commit#

When the PR merged, we re-checked the whole model, not only the reproduction for the reported bug. At the fix commit, the check of A1 passed for the first time: the reported bug was gone. But the check of A2, which had passed at every revision before, now failed. Hence S still did not hold. That automated result is what the bot posted when it reopened the issue. The failure of A2 comes down to one observable requirement: under synchronous=FULL, COMMIT must fsync the WAL before it returns. The table below shows that requirement checked on both revisions, with and without a checkpoint immediately before the COMMIT:

Revision	Setup: wal_checkpoint(TRUNCATE) before the COMMIT?	Observed: COMMIT fsyncs the WAL, as A2 requires?
parent	yes	yes
parent	no	yes
fix	yes	no
fix	no	yes

Under PRAGMA synchronous=FULL, a COMMIT that follows a WAL-resetting checkpoint does not fsync the WAL. The frames are written and COMMIT returns success, but nothing forces them to disk. Without the preceding checkpoint the fsync happens correctly, which is why this is easy to miss in review and in ordinary test suites. In fact, this regression was more severe than the original bug: a torn file is corruption a checker can detect, while this one means an acknowledged commit is silently lost, with PRAGMA integrity_check still reporting "ok". None of it reached production; the failure was demonstrated in a crash simulator during verification.

Resolution#

Subsequently, Pekka Enberg at Turso confirmed the mechanism and implemented the full fix in a PR, including the regression test recommended in our reopening comment. Turso closed #7952 again, this time citing the fix commit. Less than a day passed between our reopening of the issue and the merged upstream fix. Enberg also described the episode on X, noting that "in hindsight I should have just run the verification step on the original fix to catch this earlier."

Both A1 and A2 remain in the model, and each new revision of Turso is re-checked against them as part of the standing report we maintain. That is the proof maintenance problem in the title, and the last leg of the verification loop we described earlier: re-running the proof whenever the code changes. A fix is a code change like any other, which is why re-running the whole proof, and not just the reported bug's test, is what caught the regression.

Work with us#

Aristo, the SDK our verification service is built on, is free and open source. Deeper verification as described here is what we run with design partners, and we are onboarding 2 to 3 more. If the hardest guarantees in your system are on the crash path, apply to join, or reach us at hello@aretta.ai.