Formal methods use mathematical models and machine-checked reasoning to answer questions that testing alone cannot exhaust. They can show that every behavior in a bounded model satisfies an invariant, or that a theorem follows from stated assumptions.

They do not provide unconditional “mathematical certainty.” A result is only as strong as the model, assumptions, abstraction boundary, tool configuration, and relationship between model and implementation.

That qualification makes formal methods more useful, not less. It turns “verified” from a marketing label into a reviewable claim.

What can be verified?

Separate four artifacts:

  1. requirements: the behavior stakeholders actually need;
  2. specification: a precise mathematical model of relevant behavior;
  3. properties: safety or liveness statements about the model;
  4. implementation: the Rust/C++/hardware system that runs.

A model checker can establish that a finite explored model satisfies a property. A proof assistant can check a proof about a mathematical definition. Neither automatically proves that production code refines the model or that the requirements were correct.

The strongest projects maintain an explicit refinement story: which implementation states correspond to model states, which environment assumptions are relied on, and how tests, types, code review, or further proof connect the two.

Safety and liveness

Safety says that something bad never happens:

  • two leaders are never active in one term;
  • an object under a legal hold is never deleted;
  • a committed log entry is never replaced;
  • a balance never becomes negative.

Liveness says that something good eventually happens:

  • an eligible delete request eventually completes;
  • a submitted command eventually receives a response;
  • a lock request eventually enters the critical section.

Liveness always needs environmental assumptions. A request cannot complete if a worker is never scheduled, the network drops every message forever, or a legal hold remains forever. Fairness and failure assumptions belong in the specification.

Model checking, theorem proving, and static analysis

These techniques answer different questions.

Model checking

A model checker enumerates or symbolically explores states within a configured model. It is excellent at finding counterexamples involving concurrency, retries, reordering, and failure. A counterexample is an execution trace from an initial state to a property violation.

Finite model checking does not prove behavior for every possible cluster size or integer unless a cutoff or separate proof justifies that generalization. Its strength is exhaustive exploration of the chosen scope.

Theorem proving

A proof assistant checks a sequence of logical deductions. Proofs can quantify over unbounded domains, but building definitions and proofs requires more effort. The trusted base includes the proof assistant’s kernel and the formalization of the system.

Abstract interpretation and static analysis

Static analyzers approximate program behavior to prove properties such as absence of certain arithmetic errors, null dereferences, or data races. They trade precision for automation and scalability. A warning-free run means only that properties implemented by that analyzer hold under its model.

Types, tests, and runtime checks

Rust’s ownership system proves important memory and aliasing properties for safe code. It does not prove distributed consensus, business authorization, or that a delete API is called against the intended object.

Property tests sample many inputs; deterministic simulation explores scheduled executions; runtime assertions detect violations in deployed states. These complement formal models but are not interchangeable with proof.

Case study: an object-deletion controller

Consider a controller that accepts delete requests but must never delete an object while a legal hold is active. The hard case is a race:

  1. a delete request is queued;
  2. a legal hold is added;
  3. a worker reads stale state;
  4. deletion proceeds.

Start with a small state machine before discussing code.

A compact TLA+ model

---- MODULE DeleteAgent ----
EXTENDS FiniteSets, Sequences

CONSTANT Objects

VARIABLES live, held, requested, deleted, audit

vars == <<live, held, requested, deleted, audit>>

TypeOK ==
    /\ live \subseteq Objects
    /\ held \subseteq Objects
    /\ requested \subseteq Objects
    /\ deleted \subseteq Objects
    /\ audit \in Seq(Objects)

Init ==
    /\ live = Objects
    /\ held = {}
    /\ requested = {}
    /\ deleted = {}
    /\ audit = <<>>

Request(o) ==
    /\ o \in live
    /\ requested' = requested \cup {o}
    /\ UNCHANGED <<live, held, deleted, audit>>

AddHold(o) ==
    /\ o \in live
    /\ held' = held \cup {o}
    /\ UNCHANGED <<live, requested, deleted, audit>>

RemoveHold(o) ==
    /\ o \in held
    /\ held' = held \ {o}
    /\ UNCHANGED <<live, requested, deleted, audit>>

Delete(o) ==
    /\ o \in requested
    /\ o \in live
    /\ o \notin held
    /\ live' = live \ {o}
    /\ requested' = requested \ {o}
    /\ deleted' = deleted \cup {o}
    /\ audit' = Append(audit, o)
    /\ UNCHANGED held

Next ==
    \E o \in Objects:
        Request(o) \/ AddHold(o) \/ RemoveHold(o) \/ Delete(o)

Spec == Init /\ [][Next]_vars

NoHeldObjectDeleted == held \cap deleted = {}

EveryDeletionAudited ==
    \A o \in deleted: \E i \in 1..Len(audit): audit[i] = o

====

NoHeldObjectDeleted is not actually strong enough for every interpretation. After an object is deleted, this model prevents AddHold because the object is no longer live, so the invariant holds. But the requirement may instead say “an object that was held at the instant authorization was decided can never be deleted without a later observed release.” That requires modeling versions or authorization tokens, not just current set membership.

The exercise exposes the ambiguity before code cements it.

Small formal models should be executable as written. Pseudocode decorated with TLA+ symbols creates false confidence if TLC never parses it.

Strengthen the model with versions

A production object service normally exposes versions, generations, or conditional requests. Model an authorization decision as a token containing:

(object_id, observed_version, hold_version, policy_version)

The delete transition succeeds only if the storage system atomically confirms those versions still match. If a hold was added after authorization, the hold version changes and the conditional delete fails.

This turns a vague “check then delete” into an atomic precondition. Without a conditional storage operation or transaction, no amount of local Rust type safety closes the time-of-check/time-of-use race.

A Rust state machine is not automatically verified

Rust can mirror model states and make invalid local combinations harder to construct:

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
struct Version(u64);

#[derive(Debug, Clone, PartialEq, Eq)]
struct DeletePermit {
    object_id: String,
    object_version: Version,
    hold_version: Version,
}

trait ObjectStore {
    type Error;

    fn delete_if_versions_match(
        &self,
        permit: &DeletePermit,
    ) -> Result<bool, Self::Error>;
}

The permit bundles the observations needed for a conditional operation. The store method returns false if state changed.

This design is informed by the model, but the Rust implementation is not “formally verified” merely because it has types or comments such as #[requires(...)]. Such attributes only have meaning when a specific verification tool interprets them and its proof obligations are discharged.

Connecting model and code

Several levels of assurance are possible.

Model-derived tests

Export model traces or hand-encode transition sequences as integration tests. Verify that races found by the model produce safe implementation outcomes.

This is valuable but tests only selected traces.

Conformance checking

Record implementation events, project them into model actions, and check that each trace is allowed by the specification. This can detect divergence in tests or production. It still observes only executed traces.

Refinement mapping

Define a mathematical mapping from concrete implementation state to abstract model state and prove every concrete step preserves the abstract specification. This provides a much stronger connection but requires a formal semantics or verification framework for the implementation.

Verified core plus unverified shell

Prove a small state-transition core and wrap it in ordinary I/O code. Runtime validation ensures external inputs satisfy the core’s assumptions. This often provides better return on effort than verifying an entire service stack.

A disciplined TLC workflow

For a TLA+ model:

  1. define a tiny finite set such as two or three objects;
  2. check TypeOK first;
  3. check safety invariants;
  4. inspect distinct states and deadlocks;
  5. add concurrency, retries, crashes, and stale reads one mechanism at a time;
  6. add fairness only when liveness requirements justify it;
  7. use symmetry sets or model constraints carefully and document what they exclude;
  8. preserve the .cfg/model configuration in version control and CI.

A green TLC run without the exact constants, invariants, and properties is not reproducible evidence.

Common modeling mistakes

Modeling the intended algorithm instead of the deployed one

If production performs “read hold, enqueue, later delete” through separate APIs, a model with one atomic Delete action hides the race. Split actions at real atomic boundaries.

Assuming reliable clocks

Timeouts and leases require bounded clock drift and message delay assumptions. State those bounds or model timeout as nondeterministic.

Proving a weak invariant

“No held object is in the deleted set” may miss a history-sensitive rule. Add ghost/history variables in the model when the property refers to what was previously observed.

Ignoring failures

Model partial writes, duplicate delivery, retry after success, process restart, and stale leadership. Happy-path models rarely justify formal-methods effort.

Claiming liveness without fairness

If Delete(o) remains enabled but the scheduler can always choose another action, eventual deletion does not follow. Add a justified weak/strong fairness condition or weaken the requirement.

Choosing the right method

Use lightweight modeling when:

  • a protocol has concurrency or reordering;
  • a requirement is hard to state precisely;
  • a bug would involve a rare sequence of ordinary events;
  • the design is still cheap to change.

Use theorem proving when:

  • the property must quantify beyond a finite model;
  • a reusable algorithmic core justifies the cost;
  • proof artifacts are part of certification or assurance.

Use static analysis and types when:

  • the property maps closely to program data/control flow;
  • automation and continuous feedback are more valuable than a bespoke proof.

Most critical systems need a portfolio: a protocol model, safe language, structured testing, deterministic fault injection, runtime invariants, and operational controls.

What a rigorous verification claim contains

Instead of “the delete agent is formally verified,” write:

TLC explored all reachable states of model DeleteAgent for three objects and two workers under the recorded configuration. It found no violation of invariants X and Y. The production implementation uses conditional version checks corresponding to transition Z; conformance tests cover the published counterexample suite. Storage atomicity and identity-provider correctness remain assumptions.

That statement is narrower, but it tells reviewers exactly what evidence exists and where risk remains.

Conclusion

Formal methods are most valuable before they prove anything: writing a model forces atomicity, failure, consistency, and progress assumptions into the open. Model checking then searches combinations humans are poor at enumerating; proofs can extend assurance beyond finite scopes.

The goal is not to replace testing or attach “verified” to Rust code. It is to build a chain of evidence from requirement to model, property, tool result, implementation mechanism, and operational assumption.

Sources and further reading