Agent-Skills.md

Agent Skills: formal-verify

>

UncategorizedID: petekp/agent-skills/formal-verify

Repository

petekp/agent-skills
petekp
31

Install this agent skill to your local

pnpm dlx add-skill https://github.com/petekp/agent-skills/tree/HEAD/skills/formal-verify

Skill Files

Browse the full folder contents for formal-verify.

Download Skill

Loading file tree…

skills/formal-verify/SKILL.md

Skill Metadata

Name
formal-verify
Description
>

formal-verify

Use this skill when architectural intent matters more than "it compiles."

This skill runs a three-layer verification loop:

  1. Layer 1: structural verification over extracted AST facts and declarative rules
  2. Layer 2: behavioral verification over Z3Py protocol specs and TLA+/Apalache state-machine specs
  3. Layer 3: elegance auditing over complexity, consistency, and craft heuristics

The layers are intentionally tiered:

  • every edit: Layer 1 only, fast enough for continuous feedback
  • slice checkpoint: Layers 1 and 2
  • pre-commit and manual /verify: all three layers

Quick Start

Bootstrap a target project with:

/verify --bootstrap

Bootstrap runs four phases:

  1. Install dependencies and create .verifier/
  2. Discover architectural rules from docs and code shape
  3. Interview the user in plain English about ambiguities
  4. Validate the initial rules against the current codebase

Commands

  • /verify Runs all layers in verbose mode and prints a unified report.
  • /verify --bootstrap Installs dependencies, creates .verifier/, and scaffolds the first rule set.
  • /verify --evolve Checks for drift between architectural docs and existing verification specs.
  • /verify --grade Runs Layer 3 only and reports the current elegance grade.

How Verification Runs

Layer 1: Structural

The runner extracts facts from Rust and Swift source files, then checks structural.yaml rules such as:

  • only module X may cross boundary Y
  • modules matching pattern Z must implement interface W
  • all modules must not reference legacy identifiers

Structural checks are the default PostToolUse hook because they are the fastest.

Layer 2: Behavioral

Behavioral verification covers state transitions and protocol contracts:

  • TLA+/Apalache for temporal properties, liveness, and interleavings
  • Z3Py spec files for contracts, invariants, and cross-boundary data guarantees

Use this layer at slice checkpoints, before risky merges, and whenever a change touches coordination logic or cross-language contracts.

Layer 3: Elegance

Elegance auditing scores code for:

  • complexity
  • consistency
  • craft

It produces a grade and line-level deductions so the agent can clean up code, not just make it technically correct.

Violation Handling

When a violation is found, tailor the output to the audience:

  • agent output: counterexample, diagnosis, concrete fix suggestion
  • human output: counterexample and diagnosis only

If the agent fails to resolve the same violation three times, stop the fix loop and escalate with:

  • the original rule
  • the counterexample
  • the three attempted fixes
  • what still appears to block a correct repair

Project Structure Created In The Target Repo

Bootstrap creates and maintains:

.verifier/
├── structural.yaml
├── elegance.yaml
├── specs/
├── facts/
└── reports/
  • structural.yaml stores declarative Layer 1 rules
  • elegance.yaml stores thresholds and grade policy
  • specs/ stores Z3Py and TLA+ behavioral specs
  • facts/ caches extracted AST facts
  • reports/ stores the most recent verification outputs

facts/ and reports/ should be gitignored in the target project.

Operating Guidance

  • Run /verify before claiming a migration is complete.
  • Run /verify --grade when the code is correct but still feels rough.
  • Prefer updating rules and specs over weakening them when the architecture evolves intentionally.
  • Keep SKILL.md focused on orchestration; pull detailed mechanics from the references below.

References

  • @references/layer1-structural.md Fact extraction, Z3 encoding, reachability, and incremental invalidation.
  • @references/layer2-behavioral.md When to use TLA+/Apalache versus Z3Py, plus spec execution contracts.
  • @references/layer3-elegance.md Metric families, grading, thresholds, and the Layer 3 sub-module layout.
  • @references/constraint-yaml-spec.md Structural rule schema, selectors, assertions, and fact pattern operators.
  • @references/bootstrap-process.md The install, discover, interview, validate bootstrap workflow.
  • @references/agent-feedback-loop.md Hook integration, violation injection, retries, and escalation policy.
  • @references/spec-authoring-guide.md Translating plain-English architectural intent into formal specs.