hive/.github/workflows/formal-verify.yml at v5 · hivecommons/hive · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
name: Formal Verify

# Exhaustively re-verifies the Spin models of the escalation + reviewer-lane
# lifecycle (src/formal/escalation/) and contributor lease/reconnect protocol
# (src/formal/contribute-lease/) whenever the modeled Go code or the models
# themselves change. Reporting-only: this check is intentionally NOT required.
# The run fails when a property that must hold is violated, or when a
# documented counterexample (known design gap) can no longer be reproduced —
# both mean the model and the code have drifted apart and a human should look.
on:
  pull_request:
    paths:
      - 'src/pkg/escalation/**'
      - 'src/pkg/scheduler/reviewer_lane*'
      - 'src/pkg/dashboard/contribute_ws.go'
      - 'src/pkg/dashboard/contribute_leases.go'
      - 'src/pkg/dashboard/contribute_select.go'
      - 'bin/contributor-relay.js'
      - 'src/formal/**'
      - '.github/workflows/formal-verify.yml'
  workflow_dispatch:


concurrency:
  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: ${{ github.event_name == 'pull_request' }}

permissions:
  contents: read

jobs:
  escalation:
    name: formal-verify (escalation)
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1

      - name: Install Spin
        run: |
          sudo apt-get update
          sudo apt-get install -y spin

      - name: Verify escalation lifecycle model
        run: bash src/formal/escalation/run.sh

      - name: Verify contributor lease/reconnect model
        run: bash src/formal/contribute-lease/run.sh