Repository navigation

Add test for get_player_matches all lifecycle states #640

	name: Formal Verification Gate

	on:
	pull_request:
	push:
	branches:
	- main
	- develop
	- formal-verification

	jobs:
	check-artifacts:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5

	- name: Check formal_spec.json exists
	run: \|
	test -f contracts/escrow/formal_spec.json
	echo "✅ formal_spec.json found"

	- name: Validate JSON
	run: \|
	apt-get update && apt-get install -y jq
	jq empty contracts/escrow/formal_spec.json
	echo "✅ JSON valid"

	- name: Check kani_harness exists
	run: \|
	test -f contracts/escrow/src/kani_harness.rs
	echo "✅ kani_harness.rs found"

	- name: Check TLA+ specification exists
	run: \|
	test -f specs/tla/MatchStateMachine.tla
	test -f specs/tla/MatchStateMachine.cfg
	test -f docs/formal-spec.md
	echo "✅ TLA+ specification found"

	- name: Success
	run: echo "✅ All formal verification artifacts present"

	# Exhaustively model-check the match state machine. Both models complete in
	# well under a minute, so this runs on every PR rather than on a schedule.
	tla-model-check:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v5

	- name: Set up Java
	uses: actions/setup-java@v4
	with:
	distribution: temurin
	java-version: '17'

	- name: Cache tla2tools.jar
	uses: actions/cache@v5
	with:
	path: specs/tla/.tools
	key: tla2tools-v1.7.4

	- name: Run TLC
	run: scripts/check_tla.sh