test: add formal verification of the leaderless signaling protocol

.github/workflows/protocol.yml

@@ -0,0 +1,65 @@
+name: Protocol verification
+
+on:
+  pull_request:
+    paths:
+      - 'protocol/**'
+      - 'components/mesh-conn/**'
+      - 'components/admission-broker/**'
+      - 'components/admission-client/**'
+      - '.github/workflows/protocol.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'protocol/**'
+      - 'components/mesh-conn/**'
+      - 'components/admission-broker/**'
+      - 'components/admission-client/**'
+      - '.github/workflows/protocol.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  tlc:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: '17'
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+      - name: Check models, witnesses, and expected counterexamples
+        run: python3 protocol/check.py
+      - name: Save TLC evidence
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: protocol-model-checks
+          path: .local/protocol-checks/
+          include-hidden-files: true
+          if-no-files-found: warn
+
+  lean:
+    runs-on: ubuntu-latest
+    timeout-minutes: 12
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+      - name: Check unbounded signaling proof and all axiom dependencies
+        run: python3 protocol/proof/check.py
+      - name: Save Lean evidence
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: protocol-lean-proof
+          path: .local/protocol-proof/
+          include-hidden-files: true
+          if-no-files-found: warn

.gitignore

@@ -4,7 +4,7 @@
 
 # Local run artifacts
 .local/
-snapshots/
+/snapshots/
 .env
 
 # Compiled Go binaries
@@ -28,3 +28,8 @@ clusters/*/*.bak
 
 # Legacy local state after moving the demo cluster to clusters/patroni-demo.
 cluster-example/
+
+# Formal verification caches; protocol/snapshots contains checked-in models.
+protocol/**/__pycache__/
+protocol/**/*.olean
+protocol/**/states/

CHANGELOG.md

@@ -60,6 +60,13 @@ This changelog tracks `service-mesh` releases.
 
 ### Documentation
 
+- Added kernel-checked Lean proofs of unbounded signaling-state convergence
+  and candidate dissemination, with explicit failure/timing premises and
+  executable NAT-expiry counterexamples.
+
+- Added runnable TLA+ protocol models, bounded verification results, and
+  counterexample checks for signaling, handshake coordination, attempt ownership,
+  candidate replay, and admission, plus initial composed recovery safety checks.
 - Added this changelog and changelog maintenance instructions.
 - Added the starter architecture SVG and updated the HA Postgres SVG.
 - Updated attestation and publishing docs for deterministic compose

README.md

@@ -584,9 +584,21 @@ service design.
 - `workloads`: demo workload images used by the HA Postgres demo.
 - `support`: helper services for bootstrap or local operation.
 - `docs`: architecture, operations, and design notes.
+- `protocol`: unbounded Lean signaling proofs, finite TLA+ checks, and counterexamples.
 
 ## Development
 
+Run the unbounded signaling proof (Linux x86-64, Python 3.11+, `curl`, `tar`, and
+`zstd`) and finite model checks (Python 3.10+, Java, and `curl`):
+
+```bash
+python3 protocol/proof/check.py
+python3 protocol/check.py
+```
+
+See [`protocol/README.md`](protocol/README.md) for model bounds, assumptions,
+and verification status.
+
 With the unreleased local provider selected, run the coordinator module's
 mock-provider tests (no Cloud resources are created):
 

protocol/.gitignore

@@ -0,0 +1,2 @@
+__pycache__/
+**/states/

protocol/admission/Admission.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = TRUE
+  RequiredChecks = {"evidence", "reportData", "kms", "osImage", "workload"}
+INVARIANTS TypeOK AtMostOneConsumption AtMostOneGrant AllChecksRequired GrantRequiresConsumption
+CHECK_DEADLOCK FALSE

protocol/admission/Admission.tla

@@ -0,0 +1,61 @@
+----------------------------- MODULE Admission -----------------------------
+EXTENDS Naturals, FiniteSets
+
+(* One fresh nonce at one broker, concurrent attest requests, immutable pinned
+   policy. A check result abstracts the real verifier/hash/policy predicate.
+   Consume is atomic and occurs BEFORE the slow external verifier call.
+   Expiry does not cancel requests which have already consumed the nonce. *)
+CONSTANTS Requests, AtomicConsume, RequiredChecks
+Checks == {"evidence", "reportData", "kms", "osImage", "workload"}
+ASSUME /\ Requests # {} /\ AtomicConsume \in BOOLEAN
+       /\ RequiredChecks \subseteq Checks
+
+VARIABLES live, stage, results, granted, consumed
+vars == <<live, stage, results, granted, consumed>>
+
+Init == /\ live = TRUE
+        /\ stage = [r \in Requests |-> "new"]
+        /\ results \in [Requests -> SUBSET Checks]
+        /\ granted = {} /\ consumed = {}
+
+Consume(r) ==
+    /\ stage[r] = "new" /\ live
+    /\ stage' = [stage EXCEPT ![r] = "consumed"]
+    /\ live' = IF AtomicConsume THEN FALSE ELSE live
+    /\ consumed' = consumed \cup {r}
+    /\ UNCHANGED <<results, granted>>
+
+Verify(r) ==
+    /\ stage[r] = "consumed"
+    /\ stage' = [stage EXCEPT ![r] =
+         IF RequiredChecks \subseteq results[r] THEN "verified" ELSE "rejected"]
+    /\ UNCHANGED <<live, results, granted, consumed>>
+
+Issue(r) == /\ stage[r] = "verified"
+            /\ stage' = [stage EXCEPT ![r] = "issued"]
+            /\ granted' = granted \cup {r}
+            /\ UNCHANGED <<live, results, consumed>>
+
+(* An external verifier/issuer error consumes the nonce but grants nothing. *)
+ExternalFailure(r) ==
+    /\ stage[r] \in {"consumed", "verified"}
+    /\ stage' = [stage EXCEPT ![r] = "rejected"]
+    /\ UNCHANGED <<live, results, granted, consumed>>
+
+ExpireOrRestart == /\ live' = FALSE
+                   /\ UNCHANGED <<stage, results, granted, consumed>>
+
+Next == \/ \E r \in Requests : Consume(r) \/ Verify(r) \/ Issue(r) \/ ExternalFailure(r)
+        \/ ExpireOrRestart
+Spec == Init /\ [][Next]_vars
+TypeOK == /\ live \in BOOLEAN
+          /\ stage \in [Requests -> {"new", "consumed", "verified", "rejected", "issued"}]
+          /\ results \in [Requests -> SUBSET Checks]
+          /\ granted \subseteq Requests /\ consumed \subseteq Requests
+AtMostOneConsumption == Cardinality(consumed) <= 1
+AtMostOneGrant == Cardinality(granted) <= 1
+AllChecksRequired == \A r \in granted : Checks \subseteq results[r]
+GrantRequiresConsumption == granted \subseteq consumed
+(* Expected to fail: authorized evidence must be capable of obtaining a token. *)
+NoGrants == granted = {}
+=============================================================================

protocol/admission/MissingEvidence.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = TRUE
+  RequiredChecks = {"reportData", "kms", "osImage", "workload"}
+INVARIANT AllChecksRequired
+CHECK_DEADLOCK FALSE

protocol/admission/MissingKMS.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = TRUE
+  RequiredChecks = {"evidence", "reportData", "osImage", "workload"}
+INVARIANT AllChecksRequired
+CHECK_DEADLOCK FALSE

protocol/admission/MissingOSImage.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = TRUE
+  RequiredChecks = {"evidence", "reportData", "kms", "workload"}
+INVARIANT AllChecksRequired
+CHECK_DEADLOCK FALSE

protocol/admission/MissingReportData.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = TRUE
+  RequiredChecks = {"evidence", "kms", "osImage", "workload"}
+INVARIANT AllChecksRequired
+CHECK_DEADLOCK FALSE

protocol/admission/MissingWorkload.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = TRUE
+  RequiredChecks = {"evidence", "reportData", "kms", "osImage"}
+INVARIANT AllChecksRequired
+CHECK_DEADLOCK FALSE

protocol/admission/Reachable.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = TRUE
+  RequiredChecks = {"evidence", "reportData", "kms", "osImage", "workload"}
+INVARIANT NoGrants
+CHECK_DEADLOCK FALSE

protocol/admission/Replay.cfg

@@ -0,0 +1,7 @@
+SPECIFICATION Spec
+CONSTANTS
+  Requests = {r1, r2}
+  AtomicConsume = FALSE
+  RequiredChecks = {"evidence", "reportData", "kms", "osImage", "workload"}
+INVARIANT AtMostOneGrant
+CHECK_DEADLOCK FALSE

protocol/attempts/AttemptOwnership.cfg

@@ -0,0 +1,6 @@
+SPECIFICATION Spec
+CONSTANTS
+  GuardTimer = TRUE
+  GuardICECallback = TRUE
+INVARIANTS TypeOK AttemptIsolation
+CHECK_DEADLOCK FALSE

protocol/attempts/AttemptOwnership.tla

@@ -0,0 +1,62 @@
+------------------------- MODULE AttemptOwnership -------------------------
+EXTENDS Naturals
+
+(* time.AfterFunc can start a callback before Stop(), then block waiting for
+   sess.mu. Stop does not wait for a callback which has already started.
+   The serial retry loop may install the next abortAttempt before it runs.
+   Current Go callbacks all use peerSession.abortAgent(agent), which checks
+   sess.agent == agent under the session lock. Negative configurations remove
+   ownership checks to preserve the regression counterexamples. *)
+CONSTANT GuardTimer, GuardICECallback
+ASSUME /\ GuardTimer \in BOOLEAN /\ GuardICECallback \in BOOLEAN
+
+Attempts == 1..2
+VARIABLES current, running, finished, timer, iceCallbacks, staleCancellation
+vars == <<current, running, finished, timer, iceCallbacks, staleCancellation>>
+
+Init == /\ current = 1 /\ running = TRUE /\ finished = FALSE
+        /\ timer = [a \in Attempts |-> IF a = 1 THEN "armed" ELSE "absent"]
+        /\ iceCallbacks = {} /\ staleCancellation = FALSE
+
+TimerStarts(a) ==
+    /\ timer[a] = "armed"
+    /\ timer' = [timer EXCEPT ![a] = "started"]
+    /\ UNCHANGED <<current, running, finished, iceCallbacks, staleCancellation>>
+
+Finish ==
+    /\ current = 1 /\ ~finished
+    /\ running' = FALSE /\ finished' = TRUE
+    /\ timer' = [timer EXCEPT ![current] = IF @ = "armed" THEN "stopped" ELSE @]
+    /\ iceCallbacks' = iceCallbacks \cup {current}
+    /\ UNCHANGED <<current, staleCancellation>>
+
+BeginNext ==
+    /\ current = 1 /\ finished
+    /\ current' = 2 /\ running' = TRUE /\ finished' = FALSE
+    /\ timer' = [timer EXCEPT ![2] = "armed"]
+    /\ UNCHANGED <<iceCallbacks, staleCancellation>>
+
+TimerRuns(a) ==
+    /\ timer[a] = "started"
+    /\ LET cancels == running /\ (~GuardTimer \/ a = current)
+       IN /\ running' = IF cancels THEN FALSE ELSE running
+          /\ staleCancellation' = (staleCancellation \/ (cancels /\ a # current))
+    /\ timer' = [timer EXCEPT ![a] = "done"]
+    /\ UNCHANGED <<current, finished, iceCallbacks>>
+
+ICECallbackRuns(a) ==
+    /\ a \in iceCallbacks
+    /\ LET cancels == running /\ (~GuardICECallback \/ a = current)
+       IN /\ running' = IF cancels THEN FALSE ELSE running
+          /\ staleCancellation' = (staleCancellation \/ (cancels /\ a # current))
+    /\ iceCallbacks' = iceCallbacks \ {a}
+    /\ UNCHANGED <<current, finished, timer>>
+
+Next == \/ Finish \/ BeginNext
+        \/ \E a \in Attempts : TimerStarts(a) \/ TimerRuns(a) \/ ICECallbackRuns(a)
+Spec == Init /\ [][Next]_vars
+TypeOK == /\ current \in Attempts /\ running \in BOOLEAN /\ finished \in BOOLEAN
+          /\ timer \in [Attempts -> {"absent", "armed", "started", "stopped", "done"}]
+          /\ iceCallbacks \subseteq Attempts /\ staleCancellation \in BOOLEAN
+AttemptIsolation == ~staleCancellation
+=============================================================================

protocol/attempts/UnguardedICE.cfg

@@ -0,0 +1,6 @@
+SPECIFICATION Spec
+CONSTANTS
+  GuardTimer = TRUE
+  GuardICECallback = FALSE
+INVARIANTS TypeOK AttemptIsolation
+CHECK_DEADLOCK FALSE

protocol/attempts/UnguardedTimer.cfg

@@ -0,0 +1,7 @@
+\* Negative control: the current implementation DOES guard timer ownership.
+SPECIFICATION Spec
+CONSTANTS
+  GuardTimer = FALSE
+  GuardICECallback = TRUE
+INVARIANTS TypeOK AttemptIsolation
+CHECK_DEADLOCK FALSE

protocol/candidates/CandidateReplay.cfg

@@ -0,0 +1,8 @@
+SPECIFICATION Spec
+CONSTANTS
+  GuardLocalAuth = TRUE
+  CaptureAgent = TRUE
+  ReplayCandidates = TRUE
+INVARIANTS TypeOK LocalAuthIsolation CapturedAgentIsolation ReplayCoverage
+PROPERTY EventuallyReplayed
+CHECK_DEADLOCK FALSE