Skip to content

tla: model-check verifier-challenge gaps (#429 fail-open, #431 scan coverage) #454

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
eigmax wants to merge 4 commits into
base: dev
Choose a base branch
from
Open

tla: model-check verifier-challenge gaps (#429 fail-open, #431 scan coverage) #454

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9daaf6e
tla: model-check verifier-challenge gaps for issues #429 and #431
eigmax Aug 27, 2026
68832fb
ci: run TLA+ check on every PR; add issue #429/#431 specs to the gate
eigmax Aug 27, 2026
6df2766
ci: generic tier-based TLA+ gate (pass / historical / live)
eigmax Aug 27, 2026
0582be3
ci: run every TLA+ spec and report results dynamically; ungate the jobs
eigmax Aug 27, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
177 changes: 96 additions & 81 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,9 @@ on:
- dev
tags:
- v[0-9]+.*
# Run on every pull request regardless of base branch, so the TLA+ formal-
# verification gate (and the rest of CI behind it) runs on ANY PR.
pull_request:
branches:
- main
- dev
- gc-v2

env:
CARGO_TERM_COLOR: always
Expand All @@ -21,20 +19,12 @@ 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).
# Runs independently and in parallel with fmt/clippy/test (no `needs:` gating)
# so EVERY check runs on every PR regardless of the others' outcome. It is a
# first-class check: it fails (and blocks merge, if branch protection requires
# it) whenever a `live` bug spec still reproduces its counterexample. See the
# step below - it runs every spec, prints each one's actual TLC result in the
# job summary, and routes by tier (pass / historical / live).
tla-plus:
name: TLA+ Formal Verification
runs-on: ubuntu-latest
Expand All @@ -49,77 +39,104 @@ jobs:
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
# One declarative spec table + a generic router. Each spec carries a
# `tier`:
# pass - a fix/baseline design; MUST verify clean (else a fix
# design regressed).
# historical - a bug already fixed in the code; the frozen spec MUST
# still reproduce its counterexample. An unexpected PASS
# means the spec drifted (no longer demonstrates the bug)
# or a landed fix was reverted -> hard fail.
# live - a known-unfixed bug; while its spec still reproduces the
# counterexample it is an OPEN finding that BLOCKS merge.
# To clear it: fix the code, then change its tier to
# `historical` here (the spec is frozen and cannot detect
# the code fix on its own).
# Adding any future finding is one row; that is the whole maintenance
# surface. No per-issue logic lives in the script below.
- name: TLA+ formal verification (verify fixes, reproduce fixed bugs, block live ones)
working-directory: node/tla
run: |
set -u
JAR=~/.local/share/tlaplus/tla2tools.jar
hard_fail=0
live_open=0
{
echo "## TLA+ audit: historical bug-reproduction specs"
echo "## TLA+ formal verification"
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 "Every spec is run and its live TLC result reported below. Tiers:"
echo "**pass** must verify; **historical** (fixed bug) must still reproduce"
echo "its counterexample; **live** (unfixed bug) blocks merge while it does."
echo
echo "| Spec | Tier | TLC result | Status |"
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
# true iff TLC reports the spec holds (no violation found)
verifies() { java -jar "$JAR" -config "$1" "$2" 2>/dev/null | grep -q "Model checking completed. No error has been found."; }
while IFS='|' read -r tier cfg tla desc; do
tier="$(echo "$tier" | tr -d '[:space:]')"
cfg="$(echo "$cfg" | tr -d '[:space:]')"
tla="$(echo "$tla" | tr -d '[:space:]')"
desc="$(echo "$desc" | sed 's/^ *//; s/ *$//')"
[ -z "$tier" ] && continue
case "$tier" in \#*) continue ;; esac
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
# run the check - never short-circuit; record the real outcome
if verifies "$cfg" "$tla"; then tlc="verified (no violation)"; ok=1; else tlc="counterexample found"; ok=0; fi
case "$tier" in
pass)
if [ "$ok" = 1 ]; then status="OK"; else
status="REGRESSED - fix/baseline no longer verifies"; hard_fail=$((hard_fail+1))
echo "::error::[pass] $cfg / $tla did NOT verify ($desc). Repro: $repro"
fi ;;
historical)
if [ "$ok" = 0 ]; then status="OK - reproduces (regression record)"; else
status="DRIFT - no longer reproduces (spec edited or fix reverted)"; hard_fail=$((hard_fail+1))
echo "::error::[historical] $cfg / $tla unexpectedly verified ($desc) - investigate drift/revert. Repro: $repro"
fi ;;
live)
if [ "$ok" = 0 ]; then
status="OPEN - blocks merge"; live_open=$((live_open+1)); hard_fail=$((hard_fail+1))
echo "::error::OPEN BUG (blocks merge): $desc. Repro: $repro"
else
status="review - no longer reproduces; if fixed, move tier to historical"
echo "::warning::[live] $cfg / $tla no longer reproduces ($desc) - move its tier to 'historical' if the code is fixed. Repro: $repro"
fi ;;
*) status="UNKNOWN TIER"; hard_fail=$((hard_fail+1)); echo "::error::unknown tier '$tier' for $cfg (use pass|historical|live)" ;;
esac
echo "| \`$tla\` (\`$cfg\`) | $tier | $tlc | $status - $desc |" >> "$GITHUB_STEP_SUMMARY"
done <<'SPECS'
pass | GraphLifecycleCoreOnly.cfg | GraphLifecycle.tla | baseline chain-scan state machine is sound
pass | GraphLifecycleFixed.cfg | GraphLifecycle.tla | Finding 1 fix - atomic guard closes Graph.status race
pass | GraphLifecycleFineGrainedFixed.cfg | GraphLifecycleFineGrainedFixed.tla | Finding 1b fix - single-statement atomic CAS
pass | InstancePresignedFixed.cfg | InstancePresigned.tla | Finding 2 fix - Instance.status regression guarded
pass | Take2DisproveRace.cfg | Take2DisproveRace.tla | Finding 4 - Take2 vs Disprove margin holds (real shipped values)
pass | MultiActorRace.cfg | MultiActorRace.tla | Finding 5/10 - 1-of-N watchtower/verifier + operator_commit margin
pass | InstanceBridgeOutRaceFixed.cfg | InstanceBridgeOutRace.tla | Finding 6 fix - terminal-status guard closes resurrection
pass | MessageStateRaceFixed.cfg | MessageStateRace.tla | Finding 7 fix - terminal-guarded resurrect
pass | Take1ChallengeRaceFixed.cfg | Take1ChallengeRace.tla | Finding 9 fix - connector_a margin check added
pass | VerifierKickoffFailOpenFixed.cfg | VerifierKickoffFailOpen.tla | Issue #429 fix design - defer/retry mirrors committee
pass | KickoffScanCoverageFixed.cfg | KickoffScanCoverage.tla | Issue #431 fix - scan_kickoff_chain with adequate depth
historical | GraphLifecycle.cfg | GraphLifecycle.tla | Finding 1: Graph.status race (fixed 991faaa)
historical | GraphLifecycleFineGrained.cfg | GraphLifecycleFineGrained.tla | Finding 1b: naive guard still unsafe (fixed 991faaa)
historical | InstancePresignedBug.cfg | InstancePresigned.tla | Finding 2: Instance.status regression past Presigned (fixed 991faaa)
historical | InstanceBridgeOutRace.cfg | InstanceBridgeOutRace.tla | Finding 6: InstanceBridgeOutStatus resurrection (fixed 991faaa)
historical | MessageStateRace.cfg | MessageStateRace.tla | Finding 7: MessageState resurrection (fixed 991faaa)
historical | Take1ChallengeRace.cfg | Take1ChallengeRace.tla | Finding 9: connector_a has no margin check (fixed 991faaa)
historical | KickoffScanCoverage.cfg | KickoffScanCoverage.tla | Issue #431: detect_kickoff one-per-operator coverage gap (fixed by #451)
live | VerifierKickoffFailOpen.cfg | VerifierKickoffFailOpen.tla | Issue #429: verifier KickoffSent fail-open (SPV lag skips Challenge, never retried)
live | KickoffScanCoverageResidual.cfg | KickoffScanCoverage.tla | Issue #431 residual: MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 depth cap leaves deeper decoy chains uncovered
SPECS
{
echo
echo "**Result: $hard_fail check(s) failing, $live_open live bug(s) open.**"
} >> "$GITHUB_STEP_SUMMARY"
if [ "$hard_fail" -gt 0 ]; then
echo "::error::$hard_fail TLA+ check(s) failed ($live_open live bug(s) block merge). See the result table in the job summary."
exit 1
fi
fmt:
name: Rustfmt
needs: tla-plus
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v5
Expand All @@ -136,7 +153,6 @@ jobs:
args: --all -- --check
clippy:
name: Clippy
needs: tla-plus
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v5
Expand All @@ -155,7 +171,6 @@ jobs:
cargo clippy --all-targets -- -D warnings
test:
name: Cargo Test
needs: tla-plus
runs-on: ubuntu-latest
strategy:
matrix:
Expand Down
7 changes: 7 additions & 0 deletions node/tla/KickoffScanCoverage.cfg
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
\* ORIGINAL #431 @ f2f0285e: detect_kickoff watches only the lowest-nonce
\* graph per operator (no chain walk). ScanDepth=0. Operator has 3 graphs.
\* Expected to FAIL: kicking nonce 1 or 2 escapes coverage.
CONSTANTS NumGraphs = 3 ScanDepth = 0
SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT KickoffAlwaysCovered
80 changes: 80 additions & 0 deletions node/tla/KickoffScanCoverage.tla
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
---- MODULE KickoffScanCoverage ----
(***************************************************************************)
(* Model of GOATNetwork/bitvm-node issue #431: *)
(* "detect_kickoff watches only the lowest-nonce graph per operator, so *)
(* a kickoff on a later graph is never Challenged (unauthorized Take1)". *)
(* *)
(* THE ORIGINAL BUG (gc-v2 @ f2f0285e): detect_kickoff sourced its graphs *)
(* from fetch_on_turn_graph_by_status, which keeps ONE row per *)
(* operator_pubkey - the lowest kickoff_index still at OperatorDataPushed *)
(* (SQL: ORDER BY operator_pubkey, kickoff_index; Rust keeps the first per *)
(* operator). An operator with two posted graphs leaves nonce 0 idle and *)
(* kicks nonce >= 1; the kicked graph is never in the watched set, so no *)
(* KickoffSent / Challenge is ever created for it, and after the ConnectorA *)
(* CSV the operator Take1s with pegBTC never burned. Distinct from #429 *)
(* (there the message exists but the verifier skips it on SPV lag). *)
(* *)
(* THE FIX (commit 2bce25d, "Fix graph maintenance logic" #451, on current *)
(* dev): detect_kickoff now runs scan_kickoff_chain from each root, which *)
(* walks confirmed_prekickoff_successor forward - following each graph's *)
(* on-chain-confirmed next_prekickoff to the successor (validated *)
(* kickoff_index == prev+1) - so the idle lowest-nonce decoy no longer *)
(* hides a kicked successor. This closes the filed 2-graph attack. *)
(* *)
(* THE RESIDUAL: the walk is capped at MAX_PREKICKOFF_SUCCESSORS_PER_SCAN *)
(* = 32 (graph_maintenance_tasks.rs). The perpetually-idle root (never *)
(* kicked, so never advancing out of OperatorDataPushed) means the scan *)
(* window never slides; a chain of > 32 idle decoys with the kicked graph *)
(* beyond depth 32 is never reached on any tick. Expensive (33+ confirmed *)
(* on-chain prekickoffs, capital-locked) but structurally open. *)
(* *)
(* This spec is a COVERAGE abstraction (same static-Init idiom as *)
(* Take2DisproveRace.tla): the operator kicks graph `kicked`, keeping the *)
(* root idle; detect_kickoff covers exactly the confirmed chain reachable *)
(* from the root within ScanDepth. Property: the kicked graph is covered *)
(* (hence Challenged). ScanDepth=0 models the original no-walk selection; *)
(* ScanDepth>=NumGraphs-1 models the fix with an adequate depth budget; *)
(* 0<ScanDepth<NumGraphs-1 models the depth-limit residual. *)
(***************************************************************************)
EXTENDS Naturals

CONSTANTS
NumGraphs, \* graphs this operator has posted (all OperatorDataPushed, nonce 0..NumGraphs-1)
ScanDepth \* how many confirmed prekickoff successors detect_kickoff walks from the root
\* 0 = original bug (watch the root only, no chain walk)
\* >= NumGraphs-1 = shipped fix with adequate budget (real MAX = 32)
\* 0 < d < NumGraphs-1 = depth-limit residual

Graphs == 0 .. (NumGraphs - 1)

\* The operator keeps the lowest-nonce graph idle as the decoy; it is the
\* single root detect_kickoff selects per operator (fetch_first_graph_per_
\* operator_by_status). Because it is never kicked it never leaves
\* OperatorDataPushed, so the scan window never advances past it.
Root == 0

VARIABLE kicked \* the graph whose kickoff the operator broadcasts (no L2 initWithdraw)
vars == <<kicked>>

TypeOK == kicked \in Graphs

\* To broadcast graph `kicked`'s kickoff the operator must have confirmed the
\* prekickoff chain Root..kicked on Bitcoin (each successor's prekickoff spends
\* the prior next_prekickoff). scan_kickoff_chain therefore CAN follow that
\* confirmed chain from Root - but only up to ScanDepth successors deep. A
\* graph g is covered (its kickoff observed -> KickoffSent -> Challenge) iff
\* the walk reaches it: it lies on the confirmed chain (g <= kicked) and within
\* the depth budget (g <= ScanDepth).
WalkedSet == { g \in Graphs : g <= kicked /\ g <= ScanDepth }

Init == kicked \in Graphs
Next == UNCHANGED vars \* exhaustive over the Init choice of `kicked`
Spec == Init /\ [][Next]_vars

--------------------------------------------------------------------------
\* Safety: every unauthorized kickoff is covered by detect_kickoff (so a
\* Challenge can fire before the operator's uncontested Take1).
\* kicked \in WalkedSet <=> kicked <= ScanDepth.
KickoffAlwaysCovered == kicked \in WalkedSet

====
Loading
Loading