“Formally verified” is a strong claim. A model checker can show that a finite model has no counterexample within the explored state space. A proof assistant can establish a theorem from stated assumptions. Neither result automatically proves that a production binary, cloud API, operator procedure, and deployment configuration match the model.
The practical value of formal methods is still substantial: they force us to write down states, transitions, assumptions, and safety properties before rare interleavings reach production.
This case study considers a workflow that permanently deletes a specific version of an object only when that version is not protected. The target resembles versioned object storage with retention and legal-hold semantics, but the method applies to any critical deletion service.
Start with the claim
The safety claim is:
A version protected for the duration of the modeled workflow is never permanently deleted.
That sentence already establishes boundaries. It is about a specific version, not merely a bucket and key. It says “permanently deleted,” not “hidden by a delete marker.” It treats protection as stable during the small first model. A richer model must include adding, removing, and expiring protection.
We also want operational properties:
- every accepted request is either rejected or sent to the storage service;
- duplicate delivery does not create a second logical deletion;
- every outcome has an audit record;
- a stale protection read cannot override the storage service's authoritative enforcement.
Safety answers “nothing forbidden happens.” Eventual completion is a liveness property and requires scheduling and availability assumptions that should be stated separately.
A small TLA+ model
The following TLA+ module models a finite set of versions and a fixed protected subset. present tracks versions still stored; queued tracks deletion requests; deleted and rejected retain outcomes.
---- MODULE VersionDeletion ----
EXTENDS Naturals, FiniteSets
CONSTANTS Versions, Protected
ASSUME /\ Versions # {}
/\ Protected \subseteq Versions
VARIABLES present, queued, deleted, rejected
vars == <<present, queued, deleted, rejected>>
Init ==
/\ present = Versions
/\ queued = {}
/\ deleted = {}
/\ rejected = {}
Request(v) ==
/\ v \in present
/\ v \notin queued
/\ queued' = queued \cup {v}
/\ UNCHANGED <<present, deleted, rejected>>
Delete(v) ==
/\ v \in queued
/\ v \notin Protected
/\ present' = present \ {v}
/\ queued' = queued \ {v}
/\ deleted' = deleted \cup {v}
/\ UNCHANGED rejected
RejectProtected(v) ==
/\ v \in queued
/\ v \in Protected
/\ queued' = queued \ {v}
/\ rejected' = rejected \cup {v}
/\ UNCHANGED <<present, deleted>>
Next ==
\E v \in Versions :
Request(v) \/ Delete(v) \/ RejectProtected(v)
Spec == Init /\ [][Next]_vars
TypeOK ==
/\ present \subseteq Versions
/\ queued \subseteq Versions
/\ deleted \subseteq Versions
/\ rejected \subseteq Versions
NoProtectedDeletion ==
deleted \cap Protected = {}
====
The model is intentionally small. That is an advantage for the first iteration: we can understand every state variable and transition before adding realistic failure modes.
What the invariant means
NoProtectedDeletion says:
deleted ∩ Protected = ∅
If TLC explores the configured finite state space and finds no counterexample, we have evidence that this model preserves that invariant for the explored values and transitions.
That does not prove:
- the Rust implementation matches the model;
- the object-storage service implements the assumed semantics;
- the production access policy is correct;
- an operator cannot bypass the workflow;
- protection can never change concurrently;
- every request eventually completes.
Writing down those exclusions is part of doing formal methods responsibly.
The first model has a strong assumption
Protected is constant.
That means the model does not cover a workflow where protection can change while deletion is in flight:
request deletion
|
read object as unprotected
|
another actor adds protection
|
delete executes
If the real system allows that race, the first model is insufficient.
A richer model can make protection a variable and add transitions such as:
Protect(v)
Unprotect(v)
ExpireRetention(v)
Then the safety property must say exactly which protection states are authoritative and at what point deletion becomes irrevocable.
The model should grow only when the production contract requires it. Extra state is not rigor by itself; relevant state is.
Authoritative enforcement belongs at the destructive boundary
A common implementation pattern is:
- read metadata to see whether an object appears protected;
- reject early if it is protected;
- otherwise issue the permanent-delete operation.
The metadata check is useful for user experience and auditing, but it should not be the only safety barrier if the storage system itself can enforce retention or legal-hold rules.
Why? Because the read can become stale between steps 1 and 3.
metadata read: unprotected
|
| protection changes
v
delete request
The destructive API should still reject the delete if authoritative protection now applies.
This gives the service two layers:
application pre-check
-> clearer policy response, audit context
storage enforcement
-> final authority at destructive operation
The model should treat the second layer as an assumption only if the real storage API actually provides it under the configured mode.
Version identity must be explicit
With versioned object storage, deleting “the key” is ambiguous.
A request should carry a stable identity such as:
bucket
key
version_id
Otherwise a retry or delayed worker can act on a different version from the one that was reviewed.
The model's v corresponds to that immutable version identity, not a mutable logical path.
This is one of the most useful outcomes of modeling: a vague business operation such as “delete this object” becomes a precise state transition over a specific version.
Model duplicate delivery
Production queues retry. Clients retry. Workers crash after side effects but before acknowledgements.
So a deletion workflow should expect the same logical request more than once.
A simple extension introduces request IDs:
request_id -> target version -> outcome
The safety property is not necessarily “the storage API is invoked once.” An idempotent deletion API may tolerate repeated calls. The more useful property is:
One logical request has one durable outcome, and retries cannot redirect it to another target version.
The workflow can persist states such as:
Accepted
RejectedProtected
DeleteRequested
Deleted
AlreadyAbsent
Failed
A retry reads the existing state instead of inventing a new logical operation.
Auditing is state, not a side effect after the fact
For critical destructive workflows, an audit event that is written only after success can be lost if the process crashes between deletion and logging.
A safer design treats auditability as part of the workflow state machine.
Conceptually:
accepted request
|
v
persist request identity + target
|
v
policy decision
|
v
perform destructive operation
|
v
persist terminal outcome
If the audit sink is external, the service can use an outbox or durable event record so publication can be retried independently from the destructive operation.
The model can then express an invariant such as:
Deleted ⊆ RequestsWithDurableIdentity
and a liveness property, under fair delivery assumptions, that terminal outcomes are eventually exported to the audit system.
Safety and liveness are different questions
The first model focuses on safety:
A protected version is never deleted.
A liveness claim might be:
Every queued unprotected deletion eventually reaches a terminal outcome.
That is impossible to prove without assumptions. If the worker is never scheduled or the storage service remains unavailable forever, completion is not guaranteed.
A realistic liveness statement therefore needs conditions such as:
- workers are scheduled fairly;
- retries continue;
- the storage API eventually responds;
- required dependencies eventually become available.
Formal specifications are useful precisely because they force those hidden assumptions into the open.
Add failures explicitly
Once the basic invariant holds, model the failure points that matter to the implementation:
before persistence
before storage call
after storage success but before local acknowledgement
after terminal state but before audit publication
Then ask whether every retry path preserves target identity and protection safety.
A useful pattern is to model external operations as nondeterministic outcomes rather than assuming success:
DeleteCall(v) -> Success | Protected | NotFound | TransientFailure
This lets the checker explore retry interleavings that are hard to reproduce in ordinary tests.
Refine the model toward a Rust state machine
The specification becomes most useful when its states map cleanly into code.
A Rust domain model might start like:
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
struct ObjectVersion {
bucket: String,
key: String,
version_id: String,
}
#[derive(Clone, Debug, PartialEq, Eq)]
enum DeleteState {
Accepted,
RejectedProtected,
DeleteRequested,
Deleted,
AlreadyAbsent,
FailedRetryable,
}
#[derive(Clone, Debug)]
struct DeleteRequest {
request_id: String,
target: ObjectVersion,
state: DeleteState,
}
The code should not copy the TLA+ syntax. It should preserve the same distinctions:
- immutable target version;
- explicit request identity;
- explicit terminal states;
- no hidden transition that changes the target;
- authoritative protection failure cannot be converted into success.
From there, tests can assert that every command handler implements only allowed transitions.
Model checking complements implementation testing
Different tools answer different questions.
Unit tests
Good for deterministic transition behavior:
Accepted + protected -> RejectedProtected
Accepted + unprotected -> DeleteRequested
Property-based tests
Good for many generated inputs and state sequences.
Fault-injection tests
Good for verifying persistence and retry behavior around real dependencies.
TLA+ / model checking
Good for exploring many interleavings of a deliberately abstract state machine and checking invariants across the explored state space.
None replaces the others.
A model can be correct while the implementation is wrong. An implementation test can pass while missing an interleaving the model would expose.
Traceability is the bridge
The most important engineering practice after writing the model is maintaining a mapping between specification and implementation.
For example:
| Specification concept | Implementation concept |
| --- | --- |
| v | ObjectVersion |
| queued | durable accepted requests |
| deleted | terminal Deleted state |
| rejected | RejectedProtected |
| Delete(v) | storage client permanent-delete call |
| NoProtectedDeletion | storage enforcement + transition tests |
When code changes, review whether the mapping is still true. If a new “force delete” path appears, the model may need another transition—or the implementation may have violated the intended design.
State what was proved
After TLC checks the small model successfully, a responsible result statement is something like:
For the configured finite sets of versions and a fixed protected subset, TLC found no execution of
Request,Delete, andRejectProtectedthat violatesdeleted ∩ Protected = {}.
That is narrower than “the deletion system is formally verified.” It is also much more useful because another engineer can understand the exact evidence.
If a richer model later adds changing protection, duplicate request IDs, retries, and audit publication, state the newly checked properties just as precisely.
The practical value
The most valuable result of this exercise is not the TLA+ syntax. It is the sequence of questions the model forces us to answer:
- What exactly is being deleted?
- Which state is authoritative for protection?
- Can protection change concurrently?
- What does a duplicate request mean?
- Which outcomes are terminal?
- What must be durable before the destructive call?
- What must be auditable after it?
- Which failures are retryable?
- What assumptions are required for eventual completion?
Those questions turn a dangerous API call into an explicit protocol.
Formal methods are strongest when used this way: not as a badge that replaces testing, but as a tool for finding the assumptions and interleavings that ordinary code review tends to leave implicit.