| name | bridge-formal-workflow |
| description | Use when bridge work involves Lean, Quint, proof claims, cross-layer correspondence, formal evidence, recovery, audit, or release decisions in the active bridge repository. |
Bridge Formal Workflow Locator
This namespaced plugin skill is a locator. It does not define formal policy.
The locked canonical package SHA-256 is
c6f7a0089ed252328375c2ca7c33003c91c4bf6db8dc9ba7dc6193a450e8c87d.
Run each discovery, presence check, verifier invocation, and file read as one
separate command. Do not use shell separators, pipelines, redirection, command
substitution, variables, recursive reads, or more than one path in a command.
Use literal paths.
Use only these command forms during discovery and canonical-package reading:
git rev-parse --show-topleveltest -f <one-literal-path>- the exact
/usr/bin/python3 -I -B verifier command in step 3
sed -n '1,240p' <one-literal-path>
At the locked canonical hash, the skill and every routed reference are each
fewer than 240 lines. One allowed read completes each file. Do not issue a
second sed page during this bootstrap.
Do not use nl, cat, head, tail, ls, wc, sha256sum, or any other
command during this locator bootstrap. This restriction ends after the canonical
skill and its routed references are loaded. The canonical skill and
repository-owned commands then control all later actions.
-
Set repo to the active checkout from git rev-parse --show-toplevel.
-
Require scripts/verify-formal-skill-package.py, formal/toolchain.lock,
and .agents/skills/bridge-formal-workflow/SKILL.md below that root. If any
path is absent, stop with bridge-formal-methods installation error: active checkout has no canonical bridge formal workflow.
-
Run the repository verifier below. Replace each <absolute-repo> token with
the literal absolute root from step 1; do not use a shell variable.
/usr/bin/python3 -I -B <absolute-repo>/scripts/verify-formal-skill-package.py --repository-root <absolute-repo> --expected-aggregate-sha256 c6f7a0089ed252328375c2ca7c33003c91c4bf6db8dc9ba7dc6193a450e8c87d
The verifier checks the aggregate, complete file set, entrypoint, and every
per-file hash against formal/toolchain.lock without creating build output.
If it rejects any package byte, stop with
stale formal skill snapshot: expected canonical package c6f7a0089ed252328375c2ca7c33003c91c4bf6db8dc9ba7dc6193a450e8c87d.
-
Read .agents/skills/bridge-formal-workflow/SKILL.md completely with the
allowed sed form. Follow its reference routing and instructions from the
active checkout. Read each routed reference with that same sed form.
Do not emit the capability attestation as a progress message or a marker-only
message. After successful verification, do not send a user-visible message until
the final substantive response is ready. The final substantive response must
have this exact capability attestation as its first line:
Capability: bridge-formal-methods:bridge-formal-workflow; canonical-package-sha256: c6f7a0089ed252328375c2ca7c33003c91c4bf6db8dc9ba7dc6193a450e8c87d
