From 70a6f0eadc6ce9942243b01ab9d410b8e669ff2a Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 12:21:16 +0000 Subject: [PATCH] proof(consensus): fix + model-check the BFT consensus spec; wire TLC into CI The TLA+ consensus spec had never been model-checked and was invalid: * TypeOK violated -- Commit logs a vote snapshot incl "NONE" (commits fire once the approval threshold is met, before all agents vote), but the log type only allowed APPROVE/REJECT. * Agreement mis-stated -- it asserted all committed actions are globally DISTINCT (violated by a legitimate re-commit), not the consensus property. * ByzantineSafety vacuous -- a constant-level formula (no state vars), so TLC asserted nothing about the protocol. Rewritten as a genuine single-round Byzantine quorum model (design decision 2026-06-14): per-agent commit views, an equivocating proposer (honest agents may receive different values) + Byzantine voters. Safety now rests on QUORUM INTERSECTION: * Agreement -- no two honest agents commit different values for a round; * Validity -- an honest commit is backed by a Threshold-quorum; * ByzantineSafety -- a committed value cannot be forged by the Byzantine minority alone (>= Threshold-|Byzantine| honest senders; Threshold > F). Verified with TLC (N=4, F=1, Threshold=2F+1=3): positive run -- no error; NEGATIVE run (Threshold=2 < 2F+1) -- Agreement violated, proving the quorum threshold is load-bearing (invariants are not vacuous). Adds .github/workflows/tla-consensus.yml: downloads tla2tools v1.8.0 (sha256-pinned), runs the positive gate + asserts the negative test fails. https://claude.ai/code/session_01DQACj3RFmAPZaBPgR9SAaS --- .github/workflows/tla-consensus.yml | 56 ++++++ formal/.gitignore | 6 + formal/PhronesisConsensus.cfg | 26 +-- formal/PhronesisConsensus.tla | 268 ++++++++++------------------ formal/PhronesisConsensus_neg.cfg | 22 +++ 5 files changed, 186 insertions(+), 192 deletions(-) create mode 100644 .github/workflows/tla-consensus.yml create mode 100644 formal/.gitignore create mode 100644 formal/PhronesisConsensus_neg.cfg diff --git a/.github/workflows/tla-consensus.yml b/.github/workflows/tla-consensus.yml new file mode 100644 index 0000000..4486881 --- /dev/null +++ b/.github/workflows/tla-consensus.yml @@ -0,0 +1,56 @@ +# SPDX-License-Identifier: MPL-2.0 +# tla-consensus.yml — model-check the Byzantine consensus spec with TLC. +# +# Validates formal/PhronesisConsensus.tla (per-agent commit views, equivocating +# proposer + Byzantine voters). Two gates: +# * positive — at Threshold = 2F+1 all safety invariants hold (TypeOK, +# Agreement, Validity, ByzantineSafety); +# * negative — below the quorum bound (Threshold = 2) TLC MUST report an +# Agreement violation, proving the quorum threshold is load-bearing. +name: TLA+ Consensus + +on: + push: + branches: [main, master] + pull_request: + workflow_dispatch: + +# Estate guardrail: cancel superseded runs (read-only check, safe to cancel). +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + tlc: + name: TLC model-check (BFT safety) + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - name: Checkout + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + + - name: Fetch tla2tools (pinned version + sha256-verified) + run: | + curl -fsSL -o tla2tools.jar \ + https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar + echo "237332bdcc79a35c7d26efa7b82c77c85c2744591c5598673a8a45085ff2a4fb tla2tools.jar" \ + | sha256sum -c - + + - name: TLC positive — all safety invariants hold at Threshold = 2F+1 + working-directory: formal + run: | + java -XX:+UseParallelGC -cp "${GITHUB_WORKSPACE}/tla2tools.jar" \ + tlc2.TLC -config PhronesisConsensus.cfg PhronesisConsensus.tla + + - name: TLC negative — Agreement must fail below the quorum bound + working-directory: formal + run: | + if java -cp "${GITHUB_WORKSPACE}/tla2tools.jar" \ + tlc2.TLC -config PhronesisConsensus_neg.cfg PhronesisConsensus.tla; then + echo "::error::Agreement held at Threshold < 2F+1 — the quorum bound is not load-bearing (invariant vacuous)." + exit 1 + fi + echo "Negative test OK: Agreement correctly violated below the quorum bound." diff --git a/formal/.gitignore b/formal/.gitignore new file mode 100644 index 0000000..59e265e --- /dev/null +++ b/formal/.gitignore @@ -0,0 +1,6 @@ +# TLC model-checker artifacts +*_TTrace_*.tla +*_TTrace_*.bin +states/ +*.st +MC_*.out diff --git a/formal/PhronesisConsensus.cfg b/formal/PhronesisConsensus.cfg index e023ea2..37a1af9 100644 --- a/formal/PhronesisConsensus.cfg +++ b/formal/PhronesisConsensus.cfg @@ -1,34 +1,20 @@ -\* TLC Configuration for PhronesisConsensus +\* SPDX-License-Identifier: MPL-2.0 +\* TLC configuration for PhronesisConsensus (Byzantine quorum model). +\* N = 4 agents, F = 1 Byzantine (a4), Threshold = 2F+1 = 3, N >= 3F+1. \* Run with: tlc PhronesisConsensus.tla -config PhronesisConsensus.cfg CONSTANTS - \* 4 agents (N=4, tolerates F=1 Byzantine agent) Agents = {a1, a2, a3, a4} - - \* Two possible actions for model checking Actions = {act1, act2} - - \* Bound rounds for finite state space - MaxRounds = 3 - - \* Threshold for consensus (2F+1 = 3 for N=4, F=1) + MaxRounds = 1 Threshold = 3 - - \* Null constant + Byzantine = {a4} NULL = NULL -SPECIFICATION - Spec +SPECIFICATION Spec INVARIANTS TypeOK - Safety Agreement Validity - NonRepudiation ByzantineSafety - -PROPERTIES - \* Enable for liveness checking (requires fairness) - \* EventualDecision - \* Progress diff --git a/formal/PhronesisConsensus.tla b/formal/PhronesisConsensus.tla index 5d0b50f..873561c 100644 --- a/formal/PhronesisConsensus.tla +++ b/formal/PhronesisConsensus.tla @@ -1,203 +1,127 @@ -------------------------------- MODULE PhronesisConsensus -------------------------------- (* - * TLA+ Specification for Phronesis Consensus Protocol + * SPDX-License-Identifier: MPL-2.0 + * Copyright (c) Jonathan D.A. Jewell * - * This module specifies the consensus mechanism used for action execution - * in the Phronesis policy language. It models a simplified PBFT-style - * protocol with the following properties: + * TLA+ specification of the Phronesis action-commit consensus, modelled as a + * single-round Byzantine quorum protocol (PBFT-style core). * - * Safety: - * - Agreement: All honest agents agree on committed actions - * - Validity: Only valid actions (passing policy checks) can commit - * - Non-repudiation: All commits are logged immutably + * KEY MODELLING CHOICES (design decision 2026-06-14): + * - Agents have INDIVIDUAL commit views (committed[agent][round]), so + * "Agreement" is the genuine BFT property: no two HONEST agents commit + * different values for the same round. + * - The adversary is strong: a subset `Byzantine` may EQUIVOCATE (vote for + * several conflicting values), AND honest agents may receive different + * values for the same round (modelling a faulty/equivocating PROPOSER) — + * each honest agent still votes at most ONCE per round. * - * Liveness: - * - Termination: Every proposed action eventually commits or aborts + * Safety then rests on QUORUM INTERSECTION (not on a trusted proposer): with + * N = |Agents|, F = |Byzantine|, N >= 3F+1 and Threshold = 2F+1, any two + * Threshold-quorums share >= F+1 agents, hence >= 1 honest agent; since an + * honest agent votes at most once per round, two conflicting values cannot + * both reach a quorum. The threshold is LOAD-BEARING: lowering it below 2F+1 + * makes TLC report an Agreement violation (see the negative test in CI). * - * Model Parameters: - * - N: Total number of agents - * - F: Maximum number of Byzantine (faulty) agents - * - Constraint: N >= 3*F + 1 + * Run: tlc PhronesisConsensus.tla -config PhronesisConsensus.cfg *) - -EXTENDS Integers, Sequences, FiniteSets, TLC +EXTENDS Integers, FiniteSets, TLC CONSTANTS - Agents, \* Set of all agents - Actions, \* Set of possible actions - MaxRounds, \* Bound for model checking - Threshold \* Voting threshold (typically 2/3 + 1) + Agents, \* set of all agents (N = Cardinality(Agents)) + Actions, \* set of proposable actions + MaxRounds, \* number of consensus rounds modelled (rounds are independent) + Threshold, \* quorum size (intended 2F+1) + Byzantine, \* subset of Agents that may equivocate (|Byzantine| <= F) + NULL \* "no value" marker + +ASSUME ByzantineSubsetOfAgents == Byzantine \subseteq Agents + +Honest == Agents \ Byzantine +Rounds == 1..MaxRounds VARIABLES - proposed, \* The currently proposed action (or NULL) - votes, \* Function: Agent -> {APPROVE, REJECT, NONE} - committed, \* Sequence of committed actions - round, \* Current consensus round - agentState, \* Function: Agent -> {IDLE, VOTING, COMMITTED} - log \* Immutable consensus log - -\* Type invariant -TypeOK == - /\ proposed \in Actions \cup {NULL} - /\ votes \in [Agents -> {"APPROVE", "REJECT", "NONE"}] - /\ committed \in Seq(Actions) - /\ round \in Nat - /\ agentState \in [Agents -> {"IDLE", "VOTING", "COMMITTED"}] - /\ log \in Seq([action: Actions, votes: [Agents -> {"APPROVE", "REJECT"}], timestamp: Nat]) - -\* Initial state -Init == - /\ proposed = NULL - /\ votes = [a \in Agents |-> "NONE"] - /\ committed = <<>> - /\ round = 0 - /\ agentState = [a \in Agents |-> "IDLE"] - /\ log = <<>> + msgs, \* [Rounds -> SUBSET (Agents \X Actions)] : vote messages cast + committed \* [Agents -> [Rounds -> Actions \cup {NULL}]] : per-agent commit view -\* Helper: Count approvals -ApprovalCount == Cardinality({a \in Agents : votes[a] = "APPROVE"}) +vars == <> -\* Helper: Count rejections -RejectionCount == Cardinality({a \in Agents : votes[a] = "REJECT"}) +\* Distinct senders who voted for action v in round r. +Senders(r, v) == { a \in Agents : <> \in msgs[r] } -\* Helper: All votes cast -AllVotesCast == \A a \in Agents : votes[a] # "NONE" +\* Has honest agent a already voted in round r? +HonestVoted(a, r) == \E v \in Actions : <> \in msgs[r] -\* Helper: Consensus reached -ConsensusReached == ApprovalCount >= Threshold +------------------------------------------------------------------------------ +TypeOK == + /\ msgs \in [Rounds -> SUBSET (Agents \X Actions)] + /\ committed \in [Agents -> [Rounds -> Actions \cup {NULL}]] -\* Helper: Consensus failed -ConsensusFailed == RejectionCount > Cardinality(Agents) - Threshold +Init == + /\ msgs = [r \in Rounds |-> {}] + /\ committed = [a \in Agents |-> [r \in Rounds |-> NULL]] ------------------------------------------------------------------------------ +------------------------------------------------------------------------------ \* Actions -\* Leader proposes an action -Propose(action) == - /\ proposed = NULL - /\ round < MaxRounds - /\ proposed' = action - /\ agentState' = [a \in Agents |-> "VOTING"] - /\ round' = round + 1 - /\ UNCHANGED <> - -\* Agent casts a vote -Vote(agent, vote) == - /\ proposed # NULL - /\ agentState[agent] = "VOTING" - /\ votes[agent] = "NONE" - /\ vote \in {"APPROVE", "REJECT"} - /\ votes' = [votes EXCEPT ![agent] = vote] - /\ UNCHANGED <> - -\* Commit action if consensus reached -Commit == - /\ proposed # NULL - /\ ConsensusReached - /\ committed' = Append(committed, proposed) - /\ log' = Append(log, [ - action |-> proposed, - votes |-> [a \in Agents |-> votes[a]], - timestamp |-> round - ]) - /\ proposed' = NULL - /\ votes' = [a \in Agents |-> "NONE"] - /\ agentState' = [a \in Agents |-> "IDLE"] - /\ UNCHANGED round - -\* Abort action if consensus failed -Abort == - /\ proposed # NULL - /\ ConsensusFailed - /\ proposed' = NULL - /\ votes' = [a \in Agents |-> "NONE"] - /\ agentState' = [a \in Agents |-> "IDLE"] - /\ UNCHANGED <> - -\* Timeout (all votes cast but no decision) -Timeout == - /\ proposed # NULL - /\ AllVotesCast - /\ ~ConsensusReached - /\ ~ConsensusFailed - /\ proposed' = NULL - /\ votes' = [a \in Agents |-> "NONE"] - /\ agentState' = [a \in Agents |-> "IDLE"] - /\ UNCHANGED <> - ------------------------------------------------------------------------------ -\* Specification +\* An HONEST agent votes ONCE per round, for the value it was delivered. The +\* delivered value is chosen over all Actions to model a faulty/equivocating +\* proposer that may split the vote across honest agents. +HonestVote(a, r, v) == + /\ a \in Honest + /\ v \in Actions + /\ ~HonestVoted(a, r) + /\ msgs' = [msgs EXCEPT ![r] = @ \cup {<>}] + /\ UNCHANGED committed + +\* A BYZANTINE agent may vote for ANY action (equivocation: possibly several). +ByzVote(a, r, v) == + /\ a \in Byzantine + /\ v \in Actions + /\ msgs' = [msgs EXCEPT ![r] = @ \cup {<>}] + /\ UNCHANGED committed + +\* An honest agent commits v for round r once it observes a Threshold-quorum. +Commit(a, r, v) == + /\ a \in Honest + /\ committed[a][r] = NULL + /\ Cardinality(Senders(r, v)) >= Threshold + /\ committed' = [committed EXCEPT ![a][r] = v] + /\ UNCHANGED msgs Next == - \/ \E action \in Actions : Propose(action) - \/ \E agent \in Agents, vote \in {"APPROVE", "REJECT"} : Vote(agent, vote) - \/ Commit - \/ Abort - \/ Timeout + \/ \E a \in Agents, r \in Rounds, v \in Actions : HonestVote(a, r, v) + \/ \E a \in Agents, r \in Rounds, v \in Actions : ByzVote(a, r, v) + \/ \E a \in Agents, r \in Rounds, v \in Actions : Commit(a, r, v) -Spec == Init /\ [][Next]_<> +Spec == Init /\ [][Next]_vars ------------------------------------------------------------------------------ -\* Safety Properties +------------------------------------------------------------------------------ +\* Safety properties -\* Agreement: No conflicting commits +\* AGREEMENT (the genuine BFT property): no two honest agents commit different +\* values for the same round. Holds by quorum intersection iff Threshold >= 2F+1. Agreement == - \A i, j \in 1..Len(committed) : - i = j \/ committed[i] # committed[j] + \A a, b \in Honest, r \in Rounds : + (committed[a][r] # NULL /\ committed[b][r] # NULL) + => committed[a][r] = committed[b][r] -\* Validity: Only properly voted actions commit +\* VALIDITY: an honest agent only commits a value backed by a Threshold-quorum. Validity == - \A i \in 1..Len(log) : - Cardinality({a \in Agents : log[i].votes[a] = "APPROVE"}) >= Threshold - -\* Non-repudiation: Every committed action is in the log -NonRepudiation == - \A i \in 1..Len(committed) : - \E j \in 1..Len(log) : log[j].action = committed[i] - -\* Log is append-only (no modifications) -LogAppendOnly == - [][Len(log') >= Len(log)]_log - -\* Combined safety property -Safety == Agreement /\ Validity /\ NonRepudiation - ------------------------------------------------------------------------------ -\* Liveness Properties (under fairness) - -\* Every proposal eventually commits or aborts -EventualDecision == - proposed # NULL ~> (proposed = NULL) - -\* The system makes progress -Progress == - <>(Len(committed) > 0) - ------------------------------------------------------------------------------ -\* Byzantine Fault Tolerance - -\* Assuming F Byzantine agents (modeled as arbitrary voters) -\* With N >= 3F + 1 and Threshold = 2F + 1: -\* - Byzantine agents cannot commit invalid actions alone -\* - Honest agents (>= 2F + 1) can always reach consensus + \A a \in Honest, r \in Rounds : + committed[a][r] # NULL => + Cardinality(Senders(r, committed[a][r])) >= Threshold +\* BYZANTINE SAFETY (state-level): a committed value cannot be forged by the +\* Byzantine minority alone. Every honest commit is backed by at least +\* (Threshold - |Byzantine|) HONEST senders, provided Threshold > |Byzantine|. ByzantineSafety == - \* Even if F agents vote arbitrarily, safety holds - \A subset \in SUBSET Agents : - Cardinality(subset) <= (Cardinality(Agents) - 1) \div 3 => - \* These agents cannot force a commit without honest majority - Cardinality(subset) < Threshold - ------------------------------------------------------------------------------ -\* Model Checking Configuration - -\* For TLC model checker, use these constants: -\* Agents = {a1, a2, a3, a4} (N = 4) -\* Actions = {act1, act2} -\* MaxRounds = 3 -\* Threshold = 3 (for N=4, F=1, need 2F+1 = 3) - -\* Check: Safety, Validity, NonRepudiation -\* Check with fairness: EventualDecision, Progress + /\ Threshold > Cardinality(Byzantine) + /\ \A a \in Honest, r \in Rounds : + committed[a][r] # NULL => + Cardinality(Senders(r, committed[a][r]) \cap Honest) + >= Threshold - Cardinality(Byzantine) + +\* Combined safety. +Safety == TypeOK /\ Agreement /\ Validity /\ ByzantineSafety ============================================================================= diff --git a/formal/PhronesisConsensus_neg.cfg b/formal/PhronesisConsensus_neg.cfg new file mode 100644 index 0000000..bda9a73 --- /dev/null +++ b/formal/PhronesisConsensus_neg.cfg @@ -0,0 +1,22 @@ +\* SPDX-License-Identifier: MPL-2.0 +\* NEGATIVE test config for PhronesisConsensus. +\* Threshold = 2 is BELOW the BFT quorum bound 2F+1 = 3 (for N=4, F=1). +\* TLC MUST report an Agreement violation here — this proves the quorum +\* threshold is load-bearing and the safety invariants are not vacuous. +\* (The CI step asserts TLC exits non-zero on this config.) + +CONSTANTS + Agents = {a1, a2, a3, a4} + Actions = {act1, act2} + MaxRounds = 1 + Threshold = 2 + Byzantine = {a4} + NULL = NULL + +SPECIFICATION Spec + +INVARIANTS + TypeOK + Agreement + Validity + ByzantineSafety