formalize-enforce

Mechanically enforce formal invariants on Claude Code agents using Quint specs and Claude Code hooks.

What It Does

Quint specs define state machines with preconditions. This plugin evaluates those preconditions on every tool call:

• PreToolUse: Check if the action's precondition holds. If not, block the tool call (exit 2).
• PostToolUse: Apply the action and persist updated state for future checks.

No prompt compliance required. The Quint evaluator runs directly in bun — same spec language used for design-time verification, now enforced at runtime.

Default Rules

The built-in spec enforces three invariants:

Invariant	Formal	Effect
Read before edit	G(edit(f) -> f in files_read)	Blocks Edit on files not yet Read
Green before commit	G(commit -> tests_pass /\ ~tests_stale)	Blocks git commit unless tests pass
Bun only	G(pkg_cmd -> is_bun)	Blocks npm/yarn/pnpm, allows bun

Install

claude plugin add bjnewman/formalize-enforce

Or clone and install manually:

git clone https://github.com/bjnewman/formalize-enforce.git
cd formalize-enforce
bun install

Custom Specs

1. Write a Quint spec (see specs/agent_rules.qnt for an example)
2. Write a mapping file (see specs/mapping.json)
3. Place both in your project's .claude/ directory:
   • .claude/enforce-mapping.json (mapping)
   • Spec path is relative to the mapping file

The plugin checks for .claude/enforce-mapping.json first, then falls back to the built-in spec.

Architecture

Quint spec (.qnt)  ──(design-time)──>  quint verify / quint run
        |
        └──(runtime)──>  Quint Evaluator (imported directly into bun)
                              |
              PreToolUse hook ─┤─> check precondition ─> allow/block
             PostToolUse hook ─┘─> apply state transition ─> persist

The Quint npm package is imported directly — no subprocess, no CLI wrapper, no translation to a different DSL.

Companion Plugin

formalize-spec — converts prose instructions to formal verification-inspired notation that LLMs follow more reliably.

License

MIT