Fix 2 bugs, remove 7 dead code blocks, add formal verification #21

	name: ReqProof Audit
	on:
	push:
	branches: [main]
	pull_request:

	jobs:
	audit:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v4
	with:
	fetch-depth: 0

	# Go 1.25+ required for code-level MC/DC instrumentation.
	# jsonparser library itself supports Go 1.13+ but the verification
	# tooling needs modern Go for source-to-source rewriting.
	- name: Set up Go
	uses: actions/setup-go@v5
	with:
	go-version: '1.25'

	- name: Cache ReqProof solvers
	uses: actions/cache@v4
	with:
	path: ~/.proof/solvers
	key: proof-solvers-${{ runner.os }}

	- name: Cache ReqProof index
	uses: actions/cache@v4
	with:
	path: \|
	.proof/index.db
	.proof/index.db-shm
	.proof/index.db-wal
	key: proof-index-${{ runner.os }}-${{ hashFiles('specs/*/.req.yaml') }}
	restore-keys: \|
	proof-index-${{ runner.os }}-

	# Pre-download Z3 solver so audit checks can use it.
	# proof auto-downloads during verify but audit checks need it upfront.
	- name: Pre-download Z3 solver
	run: proof verify-properties specs/system parser --timeout 30 \|\| echo "Z3 pre-download completed (verification may have partial results)"

	- uses: probelabs/proof-action@v1
	with:
	fail-level: warn
	scope: full
	format: markdown

Navigation Menu