Your Formal Model Passed. Did You Verify the Software?¶

A model checker can finish successfully while the login page keeps sending a verified user back to “Verify your email.” There is no contradiction. The model and the page may be doing different things.

The awkward part of formal verification in an application is often the connection between a checked design and the code serving requests. We make that connection explicit in SigID with model traces that are replayed against implementation boundaries. One small example shows both what this buys us and where the evidence stops.

The cache remembers the wrong success¶

Consider a hosted form for setting up an authenticator. The user needs to verify their email before continuing. They submit the form, see the verification page, complete email verification, and submit the same form again.

The second submission ought to progress. Its bytes may be identical to the first submission, but a prerequisite has changed.

Now put an idempotency layer in front of the handler. This layer remembers a completed response so a repeated request can receive the same result without performing the operation twice. That's useful after a double-click or a lost response. It's also a problem if the layer mistakes a prerequisite page for the completed operation.

The verification page can be a perfectly valid HTTP 200 response. It rendered successfully. The requested authenticator setup has not happened yet. Caching the page as the operation's completed response confuses those two facts.

After the user verifies their email, the next submission finds the old response in the cache. The handler never gets a chance to observe the new proof. The user is told to verify again.

Four actions are enough¶

SigID has a small TLA+ model for this boundary. It tracks whether the email is verified, the cached response, the response being returned, and the current phase. Its action sequence is short enough to read in full:

require_email → verify_email → create_totp → replay_totp

Here, totp names the authenticator-setup result; the model does not implement the one-time-password algorithm.

The model checks three invariants:

VerificationNeverCached == cached # "verify_email"
SetupRequiresProof == response = "totp" => verified
VerifiedRetryProgresses == phase >= 3 => response = "totp"

An invariant describes a condition that must hold in the states under consideration. The last one says that, once the modeled retry has executed, the response must be setup. It is a state property; it does not assert that a user will eventually submit the form or that a network will eventually deliver it. That distinction between state properties and claims about execution matters when interpreting a checker result. The Apalache documentation on invariants explains the different kinds of properties.

This is a deliberately small, fixed sequence with a terminal self-loop. It doesn't enumerate arbitrary browsers, parallel requests, or every authentication flow. Small enough to inspect is an advantage here: the assumption about what can enter the cache is visible.

Put the bad behavior back¶

For this article, we ran TLC on the current model and checked that its terminal action trace matches the committed replay fixture. The model passed its three invariants.

Then we changed a temporary copy so the first action stored "verify_email" in the completed-response slot. We asked TLC to check only VerifiedRetryProgresses, allowing the sequence to get past the earlier cache invariant and reach the user-visible failure.

The retry returned "verify_email" after proof had become true. TLC reported that VerifiedRetryProgresses was violated.

This experiment establishes something useful and quite specific: the modeled property detects the cached-prerequisite behavior. It doesn't establish that the running service follows the corrected model. For that, we need to cross another boundary.

Make the implementation take the same steps¶

The corresponding Rust regression test reads the committed action trace. It then drives requests through SigID's actual idempotency middleware and actual HTML renderer for the verification-required page.

The fixture deliberately holds the browser cookie, form body, and clock fixed. The repeated request therefore reuses the original cache key. Generating a different key after verification would let the test pass without testing the behavior we care about.

For the proof step, the fixture changes a boolean. On the next form submission, the test expects the setup response and no replay marker. It submits once more and expects the same setup response, this time with the replay marker present. The handler must have run exactly twice: once for the prerequisite page and once for setup. This focused Rust replay passed when we ran it for this article.

That last assertion matters. Disabling caching altogether would let the verified user proceed, but it would discard the duplicate-request behavior the middleware is there to provide. The test checks both sides of the contract.

The production renderer marks the prerequisite response so the middleware abandons its pending slot instead of finalizing a completed response. The regression exercises that connection. A separate trace check compares the fixture with the model's terminal trace, so changing one without the other is detectable.

Be precise about the test doubles¶

This replay uses an in-memory idempotency store. Email verification is the controlled boolean, and successful setup is a stub response. The test does not send an email, persist an authenticator, run PostgreSQL, or automate a browser.

Those choices keep the regression focused on the renderer-to-middleware contract. They also put a clear limit on its result. A passing replay here provides no evidence that an email provider is reachable or that a database adapter implements its own concurrency contract correctly. Those require different tests.

Elsewhere in SigID, traces are replayed through application services and PostgreSQL when persistence is the boundary under examination. The principle is to exercise the code that owns the property, and to name every substitute that changes what the test can establish.

Why keep the model when a regression test would catch this?¶

A handwritten regression could catch this exact bug. For a defect this small, writing that test alone would be a reasonable engineering choice. Formal modeling has a maintenance cost, and a four-action example isn't evidence that every form needs a model checker.

We keep the model because it records the contract independently of the HTTP test: a prerequisite may change outside the submitted form, proof must be required, a retry must observe it, and completed setup must remain replayable. The mutation gives us a direct check that a stated property rejects the bad behavior. The implementation replay then asks whether real middleware follows the same sequence.

That still leaves work for reviewers. A model can omit the troublesome state. A replay can call a helper that bypasses the code it claims to test. A checker can be run with bounds that leave the interesting execution unexplored. None of these disappear because a report uses the word “verified.”

When evaluating an identity system, ask for one property followed all the way through: its assumptions, the execution that would violate it, the check that detects that execution, and the production code exercised by the regression. Our security model describes the broader boundaries. This cache example is the level of detail we think an assurance claim should survive.