[Copilot]

Extend GH-AW’s formal-methods guidance with executable F* verification alongside TLA+/TLC and Z3, including reproducible tooling and agent-assisted proof repair.

• Tooling: Add checksum-pinned F* 2026.10.25 and bundled Z3 5.3.0 through shared setup hooks, with version checks and smoke verification.
• Agent guidance: Integrate pinned Proof Copilot skills, document optional MCP support, and define the Specify → Implement → Verify → Diagnose → Repair → Reverify loop.
• Verification discipline: Preserve acceptance contracts, reject proof bypasses, retain reproducible evidence, and distinguish verified models from production implementations.
• Runnable examples: Pair an F* counter contract and failing-proof repair with complementary TLC safety/progress checks. Add independent read-only Actions verification and an agentic repair workflow.
• TLA+ compatibility: Refresh the replaced upstream TLC asset’s checksum and affected locks; retain existing work-queue version pins.

"$FSTAR_BIN" --smt "$FSTAR_Z3" --z3version 5.3.0 \
  --cache_off --z3rlimit 50 specs/formal-methods/Counter.fst

[pelikhan]

@copilot don't be this specific, the agent should resolve the sha on its own and pass the sha as a arg to install.sh

[Copilot]

Updated the guidance to require independently resolving the release asset SHA and passing it to the installer; the installer and workflow call sites now enforce that interface. Committed as 877fb48.

[Copilot]

Simplified the guidance to say to resolve the archive SHA-256 and pass it to the installer. Commit: 83f74d8.

[pelikhan]

@copilot run pr-finisher skill

[pelikhan]

@copilot keep it minimal

[Copilot]

@copilot run pr-finisher skill

Completed one PR-finisher pass. The PR is still draft; current-HEAD completed checks show no failures, with scans still running.

@copilot keep it minimal

Kept this pass minimal: no code changes or empty commit.

[pelikhan]

@copilot simplify these changes to a minimalistic update. shared/fsahrp.md must be self contained, not scripts

[pelikhan]

@copilot use env vars for f* version/sha

[Copilot]

@copilot simplify these changes to a minimalistic update. shared/fsahrp.md must be self contained, not scripts

Made the shared F* hook self-contained and removed the separate installer script, updating the standalone verifier and tests accordingly. This is in local commit e71c305; the remote rejected the push, so it is not yet on the PR.

@copilot use env vars for f* version/sha

FSTAR_VERSION and FSTAR_SHA256 are now environment pins in the shared hook and independent verifier. This is in local commit e71c305; the remote rejected the push, so it is not yet on the PR.

[pelikhan]

@copilot do not pollute instructions with how to use f*, focus on installation and how to run f*. the model knows how to use f*. same for other tools.