formal-verify

name	formal-verify
description	Continuous formal verification of architectural constraints and code quality. Use when asked to verify, audit, or validate codebase integrity. Runs automatically via hooks on every edit (structural) and pre-commit (full). Catches ownership violations, boundary crossings, state machine bugs, and code smells that grep ratchets miss. Triggers: "verify", "formal verify", "check architecture", "audit code quality", "run verification", "/verify", "/verify --bootstrap", "/verify --grade".
license	MIT
metadata	{"author":"petekp","version":"0.1.0"}

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.