formal-verify
Use this skill when architectural intent matters more than "it compiles."
This skill runs a three-layer verification loop:
- Layer 1: structural verification over extracted AST facts and declarative rules
- Layer 2: behavioral verification over Z3Py protocol specs and TLA+/Apalache state-machine specs
- 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:
- Install dependencies and create
.verifier/
- Discover architectural rules from docs and code shape
- Interview the user in plain English about ambiguities
- 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 ruleselegance.yaml stores thresholds and grade policyspecs/ stores Z3Py and TLA+ behavioral specsfacts/ caches extracted AST factsreports/ 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.
1---2name: formal-verify3description: 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".4license: MIT5---6
7# formal-verify
8
9Use this skill when architectural intent matters more than "it compiles."
10
11This skill runs a three-layer verification loop:
12
131. Layer 1: structural verification over extracted AST facts and declarative rules
142. Layer 2: behavioral verification over Z3Py protocol specs and TLA+/Apalache state-machine specs
153. Layer 3: elegance auditing over complexity, consistency, and craft heuristics
16
17The layers are intentionally tiered:
18
19- every edit: Layer 1 only, fast enough for continuous feedback
20- slice checkpoint: Layers 1 and 2
21- pre-commit and manual `/verify`: all three layers
22
23## Quick Start
24
25Bootstrap a target project with:
26
27```bash
28/verify --bootstrap
29```
30
31Bootstrap runs four phases:
32
331. Install dependencies and create `.verifier/`
342. Discover architectural rules from docs and code shape
353. Interview the user in plain English about ambiguities
364. Validate the initial rules against the current codebase
37
38## Commands
39
40- `/verify`
41 Runs all layers in verbose mode and prints a unified report.
42- `/verify --bootstrap`
43 Installs dependencies, creates `.verifier/`, and scaffolds the first rule set.
44- `/verify --evolve`
45 Checks for drift between architectural docs and existing verification specs.
46- `/verify --grade`
47 Runs Layer 3 only and reports the current elegance grade.
48
49## How Verification Runs
50
51### Layer 1: Structural
52
53The runner extracts facts from Rust and Swift source files, then checks
54`structural.yaml` rules such as:
55
56- only module X may cross boundary Y
57- modules matching pattern Z must implement interface W
58- all modules must not reference legacy identifiers
59
60Structural checks are the default PostToolUse hook because they are the fastest.
61
62### Layer 2: Behavioral
63
64Behavioral verification covers state transitions and protocol contracts:
65
66- TLA+/Apalache for temporal properties, liveness, and interleavings
67- Z3Py spec files for contracts, invariants, and cross-boundary data guarantees
68
69Use this layer at slice checkpoints, before risky merges, and whenever a change
70touches coordination logic or cross-language contracts.
71
72### Layer 3: Elegance
73
74Elegance auditing scores code for:
75
76- complexity
77- consistency
78- craft
79
80It produces a grade and line-level deductions so the agent can clean up code,
81not just make it technically correct.
82
83## Violation Handling
84
85When a violation is found, tailor the output to the audience:
86
87- agent output: counterexample, diagnosis, concrete fix suggestion
88- human output: counterexample and diagnosis only
89
90If the agent fails to resolve the same violation three times, stop the fix loop
91and escalate with:
92
93- the original rule
94- the counterexample
95- the three attempted fixes
96- what still appears to block a correct repair
97
98## Project Structure Created In The Target Repo
99
100Bootstrap creates and maintains:
101
102```text
103.verifier/
104├── structural.yaml
105├── elegance.yaml
106├── specs/
107├── facts/
108└── reports/
109```
110
111- `structural.yaml` stores declarative Layer 1 rules
112- `elegance.yaml` stores thresholds and grade policy
113- `specs/` stores Z3Py and TLA+ behavioral specs
114- `facts/` caches extracted AST facts
115- `reports/` stores the most recent verification outputs
116
117`facts/` and `reports/` should be gitignored in the target project.
118
119## Operating Guidance
120
121- Run `/verify` before claiming a migration is complete.
122- Run `/verify --grade` when the code is correct but still feels rough.
123- Prefer updating rules and specs over weakening them when the architecture
124 evolves intentionally.
125- Keep `SKILL.md` focused on orchestration; pull detailed mechanics from the
126 references below.
127
128## References
129
130- `@references/layer1-structural.md`
131 Fact extraction, Z3 encoding, reachability, and incremental invalidation.
132- `@references/layer2-behavioral.md`
133 When to use TLA+/Apalache versus Z3Py, plus spec execution contracts.
134- `@references/layer3-elegance.md`
135 Metric families, grading, thresholds, and the Layer 3 sub-module layout.
136- `@references/constraint-yaml-spec.md`
137 Structural rule schema, selectors, assertions, and fact pattern operators.
138- `@references/bootstrap-process.md`
139 The install, discover, interview, validate bootstrap workflow.
140- `@references/agent-feedback-loop.md`
141 Hook integration, violation injection, retries, and escalation policy.
142- `@references/spec-authoring-guide.md`
143 Translating plain-English architectural intent into formal specs.
petekp