bridge-formal-workflow

name	bridge-formal-workflow
description	Use when bridge work involves formalization, Lean or Quint selection, proof claims, obligation status, cross-layer correspondence, formal-session recovery, or formal evidence review for candidate, audit, or release.

Bridge Formal Workflow

Classify the claim before choosing a tool. Repository definitions and validators own the workflow; this skill never owns obligation status or release authority.

Self-contained decisions

When the request supplies the facts for an assurance or status decision, answer in the same response. Begin with decision, then state evidence classification, authority boundary, missing evidence or limits, and next safe check. This response contract completes a text-only review: do not announce repository inspection or defer the verdict. If repository access is unavailable, decide from the stated facts, disclose that limitation, and keep unavailable authority checks blocked.

Required order

For work on repository artifacts or executable checks, use this order:

1. Locate the repository root and read its AGENTS.md.
2. Validate the active OpenSpec change and bind the source snapshot.
3. Select model, candidate, or audit/release mode.
4. Classify the claim before selecting Lean or Quint.
5. Use Quint for transition-system behavior and bounded counterexample search.
6. Use Lean for theorem statements with every proof assumption explicit.
7. For any claim that crosses layers, require an executable correspondence contract; shared names, identifiers, or sample agreement are insufficient.
8. Run repository-owned commands and publish immutable receipts only through the repository mechanism.
9. Reduce receipts as evidence classifications only. A receipt, reducer, or model review cannot grant GateRoster, work-package, or release authority.
10. On recovery, recompute repository, worktree, snapshot, input, and tool fingerprints before resuming. Never replay an external effect from memory.

Mode selection

Mode	Purpose	Claim boundary
model	Explore or edit the abstract design	No release evidence
candidate	Reproducible local checks	Candidate evidence only
audit/release	Run every locked release prerequisite	Fail closed on any unavailable or stale check

Capability profiles change discovery, never release criteria:

Profile	Available surface
plugin_full	Repository, canonical skill, thin plugin, and tools
skill_only	Repository, canonical skill, and tools
policy_only	Repository policy and available tools

All profiles use the same repository validators and fail-closed audit/release requirements. A plugin is only a locator; a missing capability is a blocker, not permission to weaken or relabel a check.

References

• Read authority and evidence for claim, status, receipt, GateRoster, review, or release decisions.
• Read Lean and Quint boundary before tool selection or any cross-layer claim.
• Read session recovery whenever work resumes from saved state or a prior approval.
• Read commands before running or recommending checks.