Add TLA+ model for deployment concurrency leases

.github/workflows/tla-plus.yaml

@@ -0,0 +1,115 @@
+name: TLA+ model check
+
+on:
+  workflow_dispatch:
+
+  pull_request:
+    paths:
+      - .github/workflows/tla-plus.yaml
+      - "formal/tla/**"
+
+  push:
+    branches:
+      - main
+    paths:
+      - .github/workflows/tla-plus.yaml
+      - "formal/tla/**"
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: ${{ github.event_name == 'pull_request' }}
+
+env:
+  TLA_TOOLS_VERSION: "1.7.4"
+  TLA_MODEL_DIR: formal/tla/deployment-concurrency
+
+jobs:
+  check-deployment-concurrency:
+    name: Deployment concurrency
+    runs-on: ubuntu-latest
+    timeout-minutes: 5
+
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          persist-credentials: false
+
+      - name: Set up Java
+        uses: actions/setup-java@v5
+        with:
+          distribution: temurin
+          java-version: "21"
+
+      - name: Download TLA+ tools
+        run: |
+          tla_tools_url="https://github.com/tlaplus/tlaplus/releases/download/"
+          tla_tools_url+="v${TLA_TOOLS_VERSION}/tla2tools.jar"
+          tla_tools_sha256="936a262061c914694dfd669a543be2457"
+          tla_tools_sha256+="3c45d5aa0ff20a8b96b23d01e050e88"
+          curl --fail --location --silent --show-error \
+            "$tla_tools_url" \
+            --output "$RUNNER_TEMP/tla2tools.jar"
+          printf '%s  %s\n' \
+            "$tla_tools_sha256" \
+            "$RUNNER_TEMP/tla2tools.jar" \
+            | sha256sum --check -
+
+      - name: Check target protocol
+        run: |
+          mkdir -p "$RUNNER_TEMP/tlc/target"
+          java -XX:+UseParallelGC \
+            -jar "$RUNNER_TEMP/tla2tools.jar" \
+            -workers 1 \
+            -metadir "$RUNNER_TEMP/tlc/target" \
+            -config "$TLA_MODEL_DIR/DeploymentConcurrency.cfg" \
+            "$TLA_MODEL_DIR/DeploymentConcurrency.tla"
+
+      - name: Check expected counterexamples
+        shell: bash
+        run: |
+          set -euo pipefail
+
+          check_counterexample() {
+            local config="$1"
+            local invariant="$2"
+            local name="${config%.cfg}"
+            local output="$RUNNER_TEMP/tlc/${name}.log"
+
+            mkdir -p "$RUNNER_TEMP/tlc/$name"
+            set +e
+            java -XX:+UseParallelGC \
+              -jar "$RUNNER_TEMP/tla2tools.jar" \
+              -workers 1 \
+              -metadir "$RUNNER_TEMP/tlc/$name" \
+              -config "$TLA_MODEL_DIR/$config" \
+              "$TLA_MODEL_DIR/DeploymentConcurrency.tla" \
+              2>&1 | tee "$output"
+            local status="${PIPESTATUS[0]}"
+            set -e
+
+            if [[ "$status" -ne 12 ]]; then
+              echo "Expected TLC exit 12 for $config, got $status" >&2
+              return 1
+            fi
+
+            if ! grep -Fq "Invariant $invariant is violated." "$output"; then
+              echo "Expected $config to violate $invariant" >&2
+              return 1
+            fi
+          }
+
+          check_counterexample \
+            CounterexampleStaleReap.cfg \
+            RenewWinsAgainstStaleScan
+          check_counterexample \
+            CounterexampleFallbackRelease.cfg \
+            NoForeignRelease
+          check_counterexample \
+            CounterexampleReadPresentRelease.cfg \
+            NoForeignRelease
+          check_counterexample \
+            CounterexampleFlowRunDeletion.cfg \
+            NoForeignRelease

AGENTS.md

@@ -20,6 +20,7 @@ prefect/
 ├── Dockerfile                       # Production container image
 ├── docs/                            # Mintlify documentation (see docs/AGENTS.md)
 ├── examples/                        # Example flows (auto-published to docs)
+├── formal/                          # Executable formal models (see formal/tla/AGENTS.md)
 ├── integration-tests/               # End-to-end integration tests (require running server)
 ├── justfile                         # Task runner (just <command>)
 ├── load_testing/                    # Load/performance testing
@@ -134,6 +135,13 @@ docker build --build-arg EXTRA_PIP_PACKAGES="prefect-aws" -t prefect .  # With e
 - Tests require deterministic behavior
 - Mock external dependencies
 
+## Formal Protocol Models
+
+- Use TLA+ selectively for bounded concurrent or distributed protocols whose correctness depends on interleavings, retries, duplication, time, or ownership. Prefer ordinary tests for local or sequential behavior.
+- Treat each `formal/tla/<protocol>/README.md` as the authority for its scope, configurations, action-to-code mapping, owner, and review triggers.
+- Before changing mapped behavior, review the model and its deterministic regressions. Update them when the abstraction changes; otherwise state in the PR why it remains valid.
+- A green model validates only its documented abstraction, not Prefect's implementation. Implementation evidence comes from mapped behavior and contract tests.
+
 ## Working on Issues
 
 - Read the GitHub issue/PR and comments (`gh issue view`, `gh pr view`) before writing code

formal/tla/AGENTS.md

@@ -0,0 +1,36 @@
+# TLA+ Protocol Models
+
+Add a model only when a bounded concurrency question can change a design or
+preserve a regression that cheaper tests cannot establish.
+
+## Model contract
+
+- Label each configuration as current, target, or intentionally unsafe. Model
+  or isolate current failure behavior before a repair; a target remains a
+  proposal until mapped production tests pass.
+- Keep independently durable stores, queues, transactions, and clocks distinct
+  unless production makes them atomic. State fairness and availability
+  assumptions; never infer liveness from a safety-only run.
+- For each design-critical safety claim, include an unsafe configuration that
+  violates the exact named invariant, with bounds that admit the contested
+  trace and make critical actions reachable.
+
+Each model README records its question, owner, bounds, assumptions and
+exclusions, configuration status, invariants, commands and expected results,
+action/state-to-production mapping, and review triggers. Every production
+writer of modeled state must map to an action or be explicitly out of scope.
+
+Translate relevant counterexamples into deterministic behavior tests using
+explicit barriers, not sleeps. A target is implemented only when mapped
+contract tests pass; check database locking or serialization against
+PostgreSQL. Keep the model and its test oracle independent of production code.
+
+## CI and lifecycle
+
+- Pin JDK and TLA+ tool versions, verify downloads by checksum, run targets as
+  expected-green, and verify each unsafe configuration's exact exit and named
+  invariant. Do not commit tool JARs or TLC metadata.
+- Keep a new check advisory until its owner accepts the scope, invariants,
+  runtime, and diagnostics.
+- Remove an unowned, unmappable, or obsolete model and its dedicated CI;
+  preserve useful production regressions.

formal/tla/deployment-concurrency/CounterexampleFallbackRelease.cfg

@@ -0,0 +1,24 @@
+\* Expected to violate NoForeignRelease with the live-claim guard off.
+SPECIFICATION FallbackSpec
+
+CONSTANTS
+    Runs = {r1, r2}
+    LeaseIds = {l1, l2}
+    Limit = 1
+    MaxEpoch = 2
+    NoRun = NoRun
+    NoLease = NoLease
+    RecheckExpiryAtRevoke = TRUE
+    FallbackDecrementsAggregate = TRUE
+    RequireClaimForDecrement = FALSE
+
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    CounterBounds
+    ClaimCapacitySafety
+    OwnershipConsistent
+    NoForeignRelease
+    AccountingConsistent
+    RenewWinsAgainstStaleScan

formal/tla/deployment-concurrency/CounterexampleFlowRunDeletion.cfg

@@ -0,0 +1,24 @@
+\* Expected to violate NoForeignRelease after deletion leaves its lease live.
+SPECIFICATION DeletionSpec
+
+CONSTANTS
+    Runs = {r1, r2}
+    LeaseIds = {l1, l2}
+    Limit = 1
+    MaxEpoch = 2
+    NoRun = NoRun
+    NoLease = NoLease
+    RecheckExpiryAtRevoke = TRUE
+    FallbackDecrementsAggregate = FALSE
+    RequireClaimForDecrement = FALSE
+
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    CounterBounds
+    ClaimCapacitySafety
+    OwnershipConsistent
+    NoForeignRelease
+    AccountingConsistent
+    RenewWinsAgainstStaleScan

formal/tla/deployment-concurrency/CounterexampleReadPresentRelease.cfg

@@ -0,0 +1,24 @@
+\* Expected to violate NoForeignRelease under the current split release order.
+SPECIFICATION ReadPresentSpec
+
+CONSTANTS
+    Runs = {r1, r2}
+    LeaseIds = {l1, l2}
+    Limit = 1
+    MaxEpoch = 2
+    NoRun = NoRun
+    NoLease = NoLease
+    RecheckExpiryAtRevoke = TRUE
+    FallbackDecrementsAggregate = FALSE
+    RequireClaimForDecrement = FALSE
+
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    CounterBounds
+    ClaimCapacitySafety
+    OwnershipConsistent
+    NoForeignRelease
+    AccountingConsistent
+    RenewWinsAgainstStaleScan

formal/tla/deployment-concurrency/CounterexampleStaleReap.cfg

@@ -0,0 +1,24 @@
+\* Expected to violate RenewWinsAgainstStaleScan with the deadline guard off.
+SPECIFICATION StaleReapSpec
+
+CONSTANTS
+    Runs = {r1, r2}
+    LeaseIds = {l1, l2}
+    Limit = 1
+    MaxEpoch = 2
+    NoRun = NoRun
+    NoLease = NoLease
+    RecheckExpiryAtRevoke = FALSE
+    FallbackDecrementsAggregate = FALSE
+    RequireClaimForDecrement = TRUE
+
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    CounterBounds
+    ClaimCapacitySafety
+    OwnershipConsistent
+    RenewWinsAgainstStaleScan
+    NoForeignRelease
+    AccountingConsistent

formal/tla/deployment-concurrency/DeploymentConcurrency.cfg

@@ -0,0 +1,23 @@
+SPECIFICATION ClaimAuthoritySpec
+
+CONSTANTS
+    Runs = {r1, r2}
+    LeaseIds = {l1, l2}
+    Limit = 1
+    MaxEpoch = 2
+    NoRun = NoRun
+    NoLease = NoLease
+    RecheckExpiryAtRevoke = TRUE
+    FallbackDecrementsAggregate = FALSE
+    RequireClaimForDecrement = TRUE
+
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    CounterBounds
+    ClaimCapacitySafety
+    OwnershipConsistent
+    NoForeignRelease
+    AccountingConsistent
+    RenewWinsAgainstStaleScan