audit: use tla+ to formally verify transaction graphs #1024
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
| name: Cargo Build & Test | |
| on: | |
| push: | |
| branches: | |
| - main | |
| - dev | |
| tags: | |
| - v[0-9]+.* | |
| pull_request: | |
| branches: | |
| - main | |
| - dev | |
| - gc-v2 | |
| env: | |
| CARGO_TERM_COLOR: always | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} | |
| 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. | |
| # | |
| # THIS JOB IS EXPECTED TO BE RED ON THIS BRANCH RIGHT NOW. Its second step | |
| # deliberately fails for as long as any of the 6 TLC-proven, unfixed bugs | |
| # from audit/TLAPlus-20260630.md remain unfixed in the Rust code - that is | |
| # not a broken pipeline, it's the point: a clean-looking CI would hide | |
| # that this branch has known, proven, un-remediated findings. Every job | |
| # gated behind it (fmt/clippy/test) stays red along with it until real | |
| # fixes land. See that step's own comment and the audit report's | |
| # Recommendations section for the verified fix design for each finding. | |
| 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 | |
| # These model the CURRENT, unfixed code and are expected to keep | |
| # failing until the corresponding fix design above is actually applied | |
| # to the Rust source - that failure is a real, live issue, not a | |
| # historical artifact. If one of these starts passing without a | |
| # matching code change, either the bug config or the spec itself | |
| # silently changed meaning and no longer demonstrates the bug it's | |
| # supposed to. | |
| # This step is DESIGNED to keep this job red for as long as any of | |
| # these findings remain unfixed in the Rust code - it is not a drift | |
| # check anymore, it's a blocking "you have open, proven bugs" gate. | |
| # Each bug config is expected to keep failing (TLC finds the real | |
| # counterexample) until its fix design is actually applied; that | |
| # expected failure is itself what fails THIS step, on purpose, so the | |
| # whole tla-plus job - and everything gated behind it (fmt/clippy/ | |
| # test) - stays red as a constant, impossible-to-miss signal instead | |
| # of a clean-looking CI on a branch with proven, un-remediated | |
| # findings. | |
| # | |
| # The one case this step treats as MORE severe than "still open" is a | |
| # bug config unexpectedly PASSING - that means either the fix landed | |
| # without this workflow being updated (great - update the lists) or | |
| # the spec itself silently stopped demonstrating the bug (bad - the | |
| # spec needs to be fixed). Either way it exits immediately rather | |
| # than being folded into the generic open-bug count below. | |
| # | |
| # Deliberately generic: this step prints how to REPRODUCE each open | |
| # finding (the exact TLC command), not how to fix it. The verified fix | |
| # design for each finding lives in audit/TLAPlus-20260630.md - kept in | |
| # one place instead of duplicated here, where it would drift. | |
| - name: Fail while documented bugs remain unfixed (blocking, by design) | |
| working-directory: node/tla | |
| run: | | |
| JAR=~/.local/share/tlaplus/tla2tools.jar | |
| open_bugs=0 | |
| { | |
| echo "## TLA+ audit: open, unfixed findings" | |
| echo | |
| echo "This branch has TLC-proven bugs still present in the shipped Rust code." | |
| echo "Full detail and the verified fix design for each: \`audit/TLAPlus-20260630.md\`." | |
| echo "This job fails by design until each one below is fixed." | |
| 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 failing (bug not yet fixed in code) but passed - either the fix was applied (move it to the must-pass step and drop it from this list) or the spec no longer demonstrates the bug" | |
| exit 1 | |
| fi | |
| repro="cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config $cfg $tla" | |
| echo "::warning::$finding ($tla / $cfg) confirmed still present and unfixed - reproduce: $repro" | |
| echo "- **$finding** - reproduce: \`$repro\`" >> "$GITHUB_STEP_SUMMARY" | |
| open_bugs=$((open_bugs + 1)) | |
| 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 | |
| if [ "$open_bugs" -gt 0 ]; then | |
| echo "::error::$open_bugs documented, TLC-proven bug(s) remain unfixed in the Rust code. See audit/TLAPlus-20260630.md for the verified fix design for each one; reproduction commands are in the warnings above and the step summary." | |
| exit 1 | |
| fi | |
| fmt: | |
| name: Rustfmt | |
| needs: tla-plus | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions-rs/toolchain@v1 | |
| timeout-minutes: 30 | |
| with: | |
| profile: minimal | |
| toolchain: stable | |
| override: true | |
| - run: rustup component add rustfmt | |
| - uses: actions-rs/cargo@v1 | |
| with: | |
| command: fmt | |
| args: --all -- --check | |
| clippy: | |
| name: Clippy | |
| needs: tla-plus | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - uses: actions-rs/toolchain@v1 | |
| timeout-minutes: 30 | |
| with: | |
| profile: minimal | |
| toolchain: nightly-2025-12-11 | |
| override: true | |
| components: clippy | |
| - run: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/ProjectZKM/toolchain/refs/heads/main/setup.sh | sh | |
| - name: Install Dependencies | |
| run: sudo apt update && sudo apt install protobuf-compiler | |
| - run: | | |
| source ~/.zkm-toolchain/env | |
| cargo clippy --all-targets -- -D warnings | |
| test: | |
| name: Cargo Test | |
| needs: tla-plus | |
| runs-on: ubuntu-latest | |
| strategy: | |
| matrix: | |
| toolchain: | |
| - nightly-2025-12-11 | |
| steps: | |
| - uses: actions/checkout@v5 | |
| - name: Install Ziren toolchain | |
| run: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/ProjectZKM/toolchain/refs/heads/main/setup.sh | sh | |
| - name: Install Dependencies | |
| run: sudo apt update && sudo apt install protobuf-compiler | |
| - name: Launch the Regtest | |
| run: cd scripts && docker compose up -d | |
| - name: Run all unit tests | |
| run: | | |
| set -e | |
| source ~/.zkm-toolchain/env | |
| cargo test -r --all --all-targets |