Research
Executable models and recovery
Small models make state transitions easier to explore. They can reveal a lost acknowledgement, an unsafe crash window or a handshake that never converges. They still represent a chosen subset of the implementation.
Three kinds of checks
| Check | Question | Limit |
|---|---|---|
| Randomized protocol simulations | Do sampled schedules violate send-position, recovery or suppression invariants? | Fixed seeds make runs reproducible; sampled schedules are not exhaustive model checking. |
| Session-convergence model | Can simultaneous starts and asymmetric state loss settle without unsafe replacement? | Modeled policies and environments must correspond to implemented admission, persistence and retry behavior. |
| Swift / server regression tests | Do selected concrete cases behave as expected? | Tests need suitable assertions and failing counterexamples; passing does not cover every state or platform. |
The repository contains runnable checks. This page does not claim every simulation is connected to CI or rerun on every change.
A crash-window example
A send may reserve or record a position, transmit ciphertext, then finish a full-state save later. If the completed save retires send marks created after its snapshot, a crash can restore a state that no longer remembers a transmitted position. The next send may derive that position again.
SnapshotState through position n
Send n + 1A newer durable mark is needed
Save landsMust not retire uncovered marks
The C5 simulation deliberately retains an old failing rule as a negative control and compares the corrected retirement model. Salted encryption adds a separate probabilistic defence against repeated effective key/nonce pairs. It does not turn every rollback into harmless message loss: replay, metadata, availability and retained secrets remain distinct concerns.
Simultaneous handshakes
If both endpoints initiate, each can prefer a different pending session. If one loses its state, the other may keep rejecting an apparently replayed initial while sending on state its peer no longer has. Recovery must distinguish stale traffic from a fresh authenticated replacement.
The convergence work tests bounded admission and remint policies before connecting them to Swift. The critical distinction is between obtaining enough evidence to try a replacement and committing that replacement only after authentication. A timeout alone should not create authority to replace a pinned identity.
Test the oracle too
An oracle is the rule deciding whether a run passes. A broken oracle can report success on bad behavior. Preserve a known counterexample, inject a controlled defect and require the relevant check to fail. Also test missing output, non-completion and unexpected exceptions: none should become a perfect score.
The measurement page explains two reviewed examples: the earlier healing gate that excluded unfinished trials, and the earlier media scorer that could mistake missing detector output for no dropouts. It also records the September 5 working-source corrections and their focused regression checks. These examples concern the evidence pipeline, rather than an exploit in the phone app.
From a model to a product claim
A stronger claim needs a mapping from model states to concrete code, matching cryptographic and persistence assumptions, adversarial cases outside the original schedule, and independent review of the remaining boundary. The claims ledger records which obligations remain open.
Reviewed · Review scope and versions