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

Merged

buger merged 27 commits intomasterfrom

reqproof-assurance-hardening

Apr 29, 2026

Commits on Apr 19, 2026

Fix 2 bugs, remove dead code, add formal verification with ReqProof

buger
and
claude
committed
Add formal verification section to README

buger
and
claude
committed
Fix reqproof.dev → reqproof.com

buger
and
claude
committed
Remove internal dogfooding notes from docs/

buger
and
claude
committed
Remove generated fixtures from repo, add tests/ to .gitignore

buger
and
claude
committed
Complete traceability: annotate all tests, add documentation links

buger
and
claude
committed
Remove internal research docs from tracked files

buger
and
claude
committed
Fix CI: disable audit until public release, update upload-artifact to v4

buger
and
claude
committed
Fix audit CI: use R2 CDN for proof download, re-enable workflow

buger
and
claude
committed
Fix audit CI: install proof via Homebrew (available on ubuntu-latest)

buger
and
claude
committed
Fix audit CI: use downloads.reqproof.com with pinned version

buger
and
claude
committed
Use probelabs/proof-action@v1 with version pin and scope=full

buger
and
claude
committed
Set fail-level to error until next proof release

buger
and
claude
committed
Use default latest version, fail-level error until next release

buger
and
claude
committed
Pin proof version until latest channel is populated

buger
and
claude
committed
Switch to latest proof with fail-level warn

buger
and
claude
committed
Proper CI setup: Go 1.25 for MC/DC, latest proof, fail-level warn

buger
and
claude
committed
Use ubuntu-24.04 for glibc 2.39 compatibility with Z3 solver

buger
and
claude
committed
Trigger CI rebuild with cache-busted proof-action

buger
and
claude
committed
Pre-download Z3 solver before audit

buger
and
claude
committed
Debug Z3 pre-download: remove output suppression

buger
and
claude
committed
Remove manual Z3 pre-download, now handled by proof-action

buger
and
claude
committed
Install Z3 via apt before audit

buger
and
claude
committed

Commits on Apr 20, 2026

Close coverage gaps: SYS-REQ-007/008/010 fuzz harness coverage to 100%

buger
and
claude
committed

Commits on Apr 23, 2026

chore: fix spec lint warnings — remove stale parent field, set review metadata

buger
and
claude
committed

Commits on Apr 24, 2026

feat: add property-based obligation classes with 24 new SYS-REQs

buger
and
claude
committed

Commits on Apr 27, 2026

Migrate review storage from reviews/ folder to per-requirement timestamps

buger
and
claude
committed