Repository navigation
fix(ci): repair the permissions block indentation (invalid YAML) #139
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # 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@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - 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 "cc4803dce2a8ffaf0f5920a9dc39df4b5ee34ab4cb53fb58ac557277a7e516b3 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." |