audit: use tla+ to formally verify transaction graphs

.github/workflows/ci.yml

@@ -11,6 +11,7 @@ on:
     branches:
       - main
       - dev
+      - gc-v2
 
 env:
   CARGO_TERM_COLOR: always
@@ -20,8 +21,105 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
+  # Runs first and gates everything else (fmt/clippy/test all `needs: tla-plus`
+  # below) - it's the fastest job (seconds, no Rust toolchain to build) and a
+  # failure here means either a real regression the other, much slower jobs
+  # can't catch, or a stale/broken spec - either way not worth burning 30+
+  # minutes of Cargo Test/Clippy compute on before finding out.
+  #
+  # All 8 findings from audit/TLAPlus-20260630.md were fixed in commit
+  # 991faaa, so this job is expected to be GREEN. Its steps still run every
+  # bug config that reproduced the original counterexamples, but a bug
+  # config correctly still failing is no longer treated as a job failure -
+  # see the second step's own comment for why (its constants are frozen
+  # historical snapshots, not a live read of the Rust source, so they can't
+  # detect a regression by staying red; only an unexpected PASS is a real
+  # drift signal now).
+  tla-plus:
+    name: TLA+ Formal Verification
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v5
+      - uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: "21"
+      - name: Download TLA+ tools
+        run: |
+          mkdir -p ~/.local/share/tlaplus
+          curl -sL -o ~/.local/share/tlaplus/tla2tools.jar \
+            https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
+      # This audit pass proves bugs exist in CURRENT code and proves correct
+      # fix designs for them - the fixes are NOT yet applied to the Rust code
+      # (see node/README.md's "Known gap" sections). These configs model the
+      # verified fix designs (or a baseline that was never buggy) and must
+      # always pass. See root README.md's "Formal verification (TLA+)"
+      # section for what each spec covers.
+      - name: Run baseline + proposed-fix specs (must pass)
+        working-directory: node/tla
+        run: |
+          set -e
+          JAR=~/.local/share/tlaplus/tla2tools.jar
+          java -jar "$JAR" -config GraphLifecycleCoreOnly.cfg GraphLifecycle.tla
+          java -jar "$JAR" -config GraphLifecycleFixed.cfg GraphLifecycle.tla
+          java -jar "$JAR" -config GraphLifecycleFineGrainedFixed.cfg GraphLifecycleFineGrainedFixed.tla
+          java -jar "$JAR" -config InstancePresignedFixed.cfg InstancePresigned.tla
+          java -jar "$JAR" -config Take2DisproveRace.cfg Take2DisproveRace.tla
+          java -jar "$JAR" -config MultiActorRace.cfg MultiActorRace.tla
+          java -jar "$JAR" -config InstanceBridgeOutRaceFixed.cfg InstanceBridgeOutRace.tla
+          java -jar "$JAR" -config MessageStateRaceFixed.cfg MessageStateRace.tla
+          java -jar "$JAR" -config Take1ChallengeRaceFixed.cfg Take1ChallengeRace.tla
+      # This job's earlier design (while all 8 findings from this round were
+      # still genuinely unfixed) made this step - and everything gated
+      # behind it - fail for as long as any bug config still reproduced its
+      # counterexample. As of commit 991faaa, every one of those findings
+      # has actually been fixed in the shipped Rust code (see
+      # audit/TLAPlus-20260630.md) - keeping the job permanently red past
+      # that point stopped being useful: these bug configs' constants are
+      # frozen historical snapshots (e.g. Take1ChallengeRace.tla's
+      # ConnectorA), not live readings of the current Rust source, so they
+      # can never detect a real code regression by themselves - they will
+      # keep reproducing the same counterexample forever regardless of
+      # what the Rust code does. Their only genuine ongoing signal is the
+      # OPPOSITE direction: if one of them ever unexpectedly STOPS
+      # reproducing its counterexample, that means the spec itself was
+      # edited into no longer demonstrating the bug it's supposed to -
+      # that's the one case this step still treats as a hard failure.
+      # Otherwise, a bug config correctly still failing is expected and
+      # does not fail the job - it's just printed as an informational
+      # reproduction pointer.
+      - name: Confirm known-bug specs still reproduce their counterexample
+        working-directory: node/tla
+        run: |
+          JAR=~/.local/share/tlaplus/tla2tools.jar
+          {
+            echo "## TLA+ audit: historical bug-reproduction specs"
+            echo
+            echo "These model the PRE-FIX code as a permanent historical record (all"
+            echo "findings below were fixed in commit 991faaa - see"
+            echo "\`audit/TLAPlus-20260630.md\`). Still correctly reproducing their"
+            echo "original counterexample below is expected and does not fail this job."
+            echo
+          } >> "$GITHUB_STEP_SUMMARY"
+          while IFS='|' read -r cfg tla finding; do
+            [ -z "$cfg" ] && continue
+            if java -jar "$JAR" -config "$cfg" "$tla" | grep -q "Model checking completed. No error has been found."; then
+              echo "::error::$tla / $cfg was expected to keep reproducing its historical counterexample but passed instead - the spec itself was likely edited into no longer demonstrating the bug it's supposed to. If the underlying Rust fix was somehow reverted, this is also how you'd find out - either way, investigate before trusting this spec again."
+              exit 1
+            fi
+            repro="cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config $cfg $tla"
+            echo "- **$finding** - reproduce: \`$repro\`" >> "$GITHUB_STEP_SUMMARY"
+          done <<'BUGS'
+          GraphLifecycle.cfg|GraphLifecycle.tla|Finding 1: Graph.status race
+          GraphLifecycleFineGrained.cfg|GraphLifecycleFineGrained.tla|Finding 1b: naive guard still unsafe
+          InstancePresignedBug.cfg|InstancePresigned.tla|Finding 2: Instance.status regression past Presigned
+          InstanceBridgeOutRace.cfg|InstanceBridgeOutRace.tla|Finding 6: InstanceBridgeOutStatus resurrection
+          MessageStateRace.cfg|MessageStateRace.tla|Finding 7: MessageState resurrection
+          Take1ChallengeRace.cfg|Take1ChallengeRace.tla|Finding 9: connector_a has no margin check
+          BUGS
   fmt:
     name: Rustfmt
+    needs: tla-plus
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v5
@@ -38,6 +136,7 @@ jobs:
           args: --all -- --check
   clippy:
     name: Clippy
+    needs: tla-plus
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v5
@@ -56,6 +155,7 @@ jobs:
           cargo clippy --all-targets -- -D warnings
   test:
     name: Cargo Test
+    needs: tla-plus
     runs-on: ubuntu-latest
     strategy:
       matrix:
@@ -72,5 +172,5 @@ jobs:
       - name: Run all unit tests
         run: |
           set -e
-          source ~/.zkm-toolchain/env 
+          source ~/.zkm-toolchain/env
           cargo test -r --all --all-targets

.gitignore

@@ -34,4 +34,5 @@ circuits/*/*/*.bin.in
 
 **/*.out
 **/*/output.data*
-proof-builder-rpc/*.ckpt
+proof-builder-rpc/*.ckpt
+node/tla/states/

README.md

@@ -11,6 +11,76 @@ GOAT Network's BitVM2 bridge implementation. See [GOAT BitVM2 Whitepaper](https:
 - `deployment`: Deployment scripts and documentation
 
 
+## Formal verification (TLA+)
+
+`node/tla/` contains TLA+ specs that formally verify the graph/instance status
+state machines and the peg-out timelock configuration against real races and
+boundary conditions found in the Rust implementation. This started as an
+**audit pass**: the specs proved several real bugs existed and proved a
+correct fix design for each. **As of commit
+[`991faaa`](https://github.com/GOATNetwork/bitvm2-node/commit/991faaabdb56c747103e8f1c6d6477c638ccfc4c),
+all 8 of those findings have been fixed and verified in the shipped Rust
+code** - see `audit/TLAPlus-20260630.md` for the full report, including what
+each real applied fix looks like.
+
+**CI's `tla-plus` job is expected to be GREEN.** Each bug config (e.g.
+`GraphLifecycle.cfg`) is kept as a **permanent historical record**,
+deliberately still modeling the pre-fix code, and correctly reproducing its
+original counterexample - but that expected failure is only printed as an
+informational reproduction pointer in the job summary, it does not fail the
+job. The only thing that *does* fail the job is a bug config **unexpectedly
+passing**, since that would mean either the spec silently stopped
+demonstrating the bug it's supposed to, or (more alarmingly) the fix's guard
+got removed again. See that job's own comments in
+`.github/workflows/ci.yml` for the full reasoning.
+
+Concretely: for each bug found, there is a **pair** of configs - one modeling
+the pre-fix code (still models it as buggy on purpose - **expected to
+fail**, a permanent historical record, not a live issue, and does not fail
+CI) and one modeling the fix design (**expected to pass**, and does fail CI
+if it doesn't - for every finding below, that design has since actually been
+applied to the shipped Rust code, not just proven sound in the abstract).
+
+**Setup** (once): install a JRE (11+) and download the official TLA+ tools jar:
+
+```bash
+sudo apt-get install -y openjdk-21-jre-headless   # or any JRE 11+
+mkdir -p ~/.local/share/tlaplus
+curl -sL -o ~/.local/share/tlaplus/tla2tools.jar \
+  https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
+```
+
+**Run a spec**:
+
+```bash
+cd node/tla
+java -jar ~/.local/share/tlaplus/tla2tools.jar -config <Spec>.cfg <Spec>.tla
+```
+
+| Spec | Config | Models | Result |
+|---|---|---|---|
+| `GraphLifecycle.tla` | `GraphLifecycleCoreOnly.cfg` | code baseline | pass - chain-scan state machine alone is sound |
+| `GraphLifecycle.tla` | `GraphLifecycle.cfg` | **pre-fix code (historical)** | **fails, by design**: unguarded race between the Bitcoin-chain-scan and GoatChain-event writers of `Graph.status` - fixed in `991faaa`, kept failing as a permanent regression check |
+| `GraphLifecycle.tla` | `GraphLifecycleFixed.cfg` | fix design (**applied in `991faaa`**) | pass - atomic guard design closes the race |
+| `GraphLifecycleFineGrained.tla` | `GraphLifecycleFineGrained.cfg` | pre-fix code (historical) | **fails, by design**: the read/write gap a naive (non-atomic) guard would still have - fixed in `991faaa` |
+| `GraphLifecycleFineGrainedFixed.tla` | `GraphLifecycleFineGrainedFixed.cfg` | fix design (**applied in `991faaa`**) | pass - single-statement atomic CAS design closes the gap |
+| `InstancePresigned.tla` | `InstancePresignedBug.cfg` | **pre-fix code (historical)** | **fails, by design**: `Instance.status` can regress past `Presigned` - fixed in `991faaa` |
+| `InstancePresigned.tla` | `InstancePresignedFixed.cfg` | fix design (**applied in `991faaa`**) | pass - guard design closes the regression |
+| `Take2DisproveRace.tla` | `Take2DisproveRace.cfg` | fix design (**applied in `991faaa`**, values updated to match) | pass - Take2 vs. Disprove UTXO race has strict margin on all networks with the real shipped `crates/bitvm-gc/src/timelocks.rs` values (Testnet4 `connector_d` now 40, shipped with more margin than originally proposed); the pre-fix shipped value (34) did **not** have this margin - that boundary case is how this spec found the bug in the first place |
+| `MultiActorRace.tla` | `MultiActorRace.cfg` | fix design (**applied in `991faaa`**, values updated to match) | pass - the 1-of-N watchtower/verifier security property holds under the real shipped timelock values, checked against 2 independent actors per role rather than 1 |
+| `InstanceBridgeOutRace.tla` | `InstanceBridgeOutRace.cfg` | **pre-fix code (historical)** | **fails, by design**: `InstanceBridgeOutStatus` can be resurrected to `Initialize` after reaching `Claim`/`Timeout`/`Refund` by a stale RPC upsert or maintenance-task write - fixed in `991faaa` |
+| `InstanceBridgeOutRace.tla` | `InstanceBridgeOutRaceFixed.cfg` | fix design (**applied in `991faaa`**) | pass - atomic guard design (write only if not already terminal) closes the resurrection |
+| `MessageStateRace.tla` | `MessageStateRace.cfg` | **pre-fix code (historical)** | **fails, by design**: `MessageState::Cancelled` could be resurrected to `Pending` by `upsert_message`'s unconditional `ON CONFLICT DO UPDATE` - fixed in `991faaa` |
+| `MessageStateRace.tla` | `MessageStateRaceFixed.cfg` | fix design (**applied in `991faaa`**) | pass - guarding the resurrect-to-Pending write against terminal status closes the race |
+| `Take1ChallengeRace.tla` | `Take1ChallengeRace.cfg` | **pre-fix code (historical)** | **fails, by design**: `connector_a` (Take1 vs. Challenge) had *no* margin check anywhere in `validate_timelock_config`; on Regtest the pre-fix shipped value gave a challenger exactly zero reaction margin - fixed in `991faaa` |
+| `Take1ChallengeRace.tla` | `Take1ChallengeRaceFixed.cfg` | fix design (**applied in `991faaa`**) | pass - the missing margin check (mirroring Finding 4's floor) was added, closing the gap |
+| `MultiActorRace.tla` | `MultiActorRace.cfg` | verification (no bug; still holds under real shipped values) | pass - also confirms `operator_commit`'s margin against the shared `ConnectorF` UTXO (the `OperatorCommitTimeoutTransaction` path, `ConnectorF` leaf 1's second spender) holds, closing a gap where only a scalar Rust check existed |
+
+Additional standalone tools available in the jar if needed: SANY (parser/type-checker)
+via `java -cp tla2tools.jar tla2sany.SANY <Spec>.tla`, and the PlusCal translator
+(used to generate `GraphLifecycleFineGrained*.tla`'s TLA+ body from its PlusCal
+algorithm block) via `java -cp tla2tools.jar pcal.trans <Spec>.tla`.
+
 ## Contributing
 
 Contributions are welcome! Please open an issue or submit a pull request for any improvements or bug fixes.