create-formal-verification-skill

• SKILL.mdcore · 7,187 bytes

# create-formal-verification-skill

An example-based test exercises only the cases someone wrote down. A formal check exhausts a stated scope, which may be all interleavings of a model, all inputs below a size bound, or the entire input space. Apply one where that gap matters, then leave a skill that later agents rerun each time they edit the covered code.

Assume the user cannot read TLA+ or any proof language. Report everything using the names and concepts of the code itself, so they can judge the outcome and decide what to do without learning the tool.

Good targets: concurrency, retries, state machines, parsers, permission checks, and unsafe memory access, anywhere tests feel thin. If the area already has a generated verify skill, use the `maintain-formal-verification-skill` skill ([../maintain-formal-verification-skill/SKILL.md](../maintain-formal-verification-skill/SKILL.md)) instead.

## 1. Choose what to verify

Read the code first, and put questions to the user only where the code leaves a gap. When the user pointed at a particular area or defect, begin with it.

The best candidate is a guarantee the code makes, whose failure hurts users, and whose failing case tests rarely reach. Pick the highest-value candidate in the codebase, not the easiest to formalize. Security guarantees often rank highest: "a revoked token is never accepted after revocation commits", "a payout is never sent twice for one invoice", "a path from user input never resolves outside the upload root".