Begin with one conversation

The agent sends Propose(action, generation). The approval service returns Approve(action_hash, generation) or Reject. The executor admits the action only when approval identity matches. The executor spends one capacity credit, runs the tool, publishes one receipt, and returns the credit.

This conversation resembles Communicating Sequential Processes: named participants exchange events through channels, and their legal conversations form the protocol. CSP vocabulary helps identify messages, sequencing, choice, and deadlock. TLA+ can then encode those events as actions without requiring a CSP tool in the first model.

Route each question by shape

The admission proof remains a runnable anchor for the capstone:

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct Request {
    generation: u8,
    action_hash: u8,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct Approval {
    generation: u8,
    action_hash: u8,
}

fn accepts(request: Request, approval: Approval) -> bool {
    request.generation == approval.generation && request.action_hash == approval.action_hash
}

#[cfg(kani)]
mod proofs {
    use super::{accepts, Approval, Request};

    #[kani::proof]
    pub fn accepted_receipt_matches_request() {
        let request = Request {
            generation: kani::any(),
            action_hash: kani::any(),
        };
        let approval = Approval {
            generation: kani::any(),
            action_hash: kani::any(),
        };

        if accepts(request, approval) {
            assert_eq!(request.generation, approval.generation);
            assert_eq!(request.action_hash, approval.action_hash);
        }
    }
}

kani admission.rs

Normalize the trace vocabulary

Use the same nouns across tools: generation, action_hash, approval, credit, completion, and receipt. A TLC action named Cancel(g) should map to a Stateright action and a Loom synchronization point with the same meaning. A Kani counterexample should print the same fields that an approval receipt stores.

Shared words do not make the claims identical. Shared words make it possible to replay one checker witness through another layer. For example, a TLC trace can become a deterministic reducer test. A Loom schedule can reveal that the production adapter violates the atomic step assumed by the TLA+ model.

Write the final report

A useful report has six short parts:

1. The claim names one observation and one forbidden behavior.
2. The model names its state, actions, and refusal boundary.
3. The checker result names version, command, bounds, and verdict.
4. The negative control names the injected defect and the expected witness.
5. The refinement note maps production events and values to model terms.
6. The residual-risk note names every important behavior still outside the evidence.

Do not collapse the report to “formally verified.” That phrase hides the property, model, bound, and code connection. Say what the evidence established.

Practice

Design a model for this failure: an agent proposes Delete(file-A). A person approves the proposal. Before execution, the agent changes the argument to file-B while retaining the approval token.

Write the state fields, action sequence, safety property, and first checker. Then name one Kani harness and one Loom race that remain after the temporal model passes.

Worked answer

The state contains proposal bytes or their canonical hash, generation, approval identity, execution status, and receipt. The actions are propose, approve, replace proposal, execute, and record. The safety property says that every executed action has the exact canonical identity and generation named by its approval. TLA+ with TLC is a good first checker because the failure depends on an event sequence.

The Kani harness checks that the admission function accepts only equal generation and action identity values. The Loom model checks whether proposal replacement and execution can observe fields from different snapshots. A passing temporal model still needs the refinement argument that production reads one coherent record.

Lessons

• Choose a checker from the formal shape of the question.
• CSP vocabulary can clarify conversations before a behavioral model is written.
• Shared state and action names make counterexamples replayable across layers.
• Each result retains its own assumptions, bounds, and refinement gap.
• Negative controls show that the evidence can detect the failure it claims to exclude.

References

1. C. A. R. Hoare. “Communicating Sequential Processes.” Communications of the ACM, 1978. — processes, communication, and guarded choice.
2. Leslie Lamport. “A High-Level View of TLA+.” — behavior-level specification and implementation relations.
3. Kani Project. “Kani Documentation.” — Rust proof harnesses and bounded verification.