Repository navigation

🐛 [v6] contribute: a role-delegated task's guidance carries the assigned repo's AGENTS.md and the issue's relevant knowledge #692

	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