A Claude Code plugin that converts prose instructions in specification files (CLAUDE.md, SKILL.md, AGENTS.md) to formal verification-inspired notation that LLMs follow more reliably.
Research shows structured constraint formats reduce ambiguity and improve LLM compliance:
| Study | Finding |
|---|---|
| HoarePrompt (2025) | Hoare-style {P} C {Q} triples improved correctness reasoning 62-93% over prose |
| FASTRIC (2025) | Explicit state machines improved compliance by 3-4 points |
| LogicGuard (2025) | LTL temporal constraints achieved 100% task completion where free-form agents failed |
LLMs can't mechanically verify specs, but structured formats are less ambiguous than prose, so they get followed more reliably.
| Rule type | Formalism | Example |
|---|---|---|
| Behavioral constraints | LTL temporal invariants | G(edit(f) → f ∈ files_read) |
| Action specifications | Hoare triples | {bug_reported} fix {regression_test_exists} |
| Output constraints | Refinement types | CommitMsg : {s | len(s) < 80 ∧ lowercase(s)} |
| Permission tiers | Three-tier boundaries | ALWAYS / ASK_FIRST / NEVER |
| Workflows | State machines | Mermaid stateDiagram-v2 |
Before (prose):
Practice TDD where possible: Write tests first, run to confirm they fail,
implement minimum code, refactor while keeping tests passing.
After (Hoare triple):
{feature_requested} implement {tests_pass ∧ diff_minimal}
ORDERING: write_tests → verify_fail → implement → verify_pass
/plugin install formalize-spec
Or add the marketplace URL manually and install from there.
Trigger naturally:
- "formalize this CLAUDE.md"
- "convert these rules to predicates"
- "make this spec more precise"
Or invoke directly: /formalize-spec path/to/SKILL.md
MIT