Z Specification Plugin for Claude Code
Formal Z specifications and B machines that type-check, animate, and refine --- from English to math to code.
Platforms: macOS, Linux
What is Z?
Z ("zed") is a formal specification language based on set theory and first-order predicate logic. It was developed at the University of Oxford in the late 1970s and is standardized as ISO 13568.
A Z specification describes a system as:
- States --- the data a system holds (e.g., a set of users, a counter, a mode flag)
- Invariants --- constraints that must always be true (e.g.,
correct ≤ attempts, level ≥ 1)
- Operations --- transitions between states, with preconditions and effects
The specification says what a system does, not how. When a type-checker (fuzz) accepts a spec, the description is internally consistent. When an animator (ProB) explores the state space, you see every reachable configuration --- including ones you forgot to think about.
Z's sibling, the B-Method, extends the same mathematical foundations with a substitution language and a deterministic refinement chain from spec to code. This plugin supports both --- see B-Method below.
Why use formal specs?
Formal specs catch entire classes of bugs mathematically, not just the specific inputs you happened to test. A spec invariant like ¬(radioMode = receiving ∧ toneActive) makes it structurally impossible to miss the case where keying occurs during receive mode --- no matter how many test cases you write, the invariant covers all of them.
Formal specifications have always caught these bugs. They were too expensive to write by hand --- hours of skilled effort per schema. An LLM drafts the spec; fuzz type-checks it. The methods are the same; the time cost is not.
Key references
Dependencies
Z Spec orchestrates two established tools that do the mathematical heavy lifting:
- fuzz --- Mike Spivey's Z type-checker, developed at Oxford. Verifies that a specification is internally consistent: every schema is well-typed, every reference resolves, every invariant is expressible. Also provides
fuzz.sty for LaTeX rendering.
- ProB --- an animator and model-checker from Heinrich Heine University Düsseldorf. Explores the state space of a specification: finds reachable states, checks invariants hold across all transitions, and discovers counter-examples when they don't.
Both are installed automatically by /z-spec:setup all. fuzz is compiled from source; ProB is downloaded as a pre-built binary for your platform.
Quick Start
curl -fsSL https://raw.githubusercontent.com/punt-labs/z-spec/5b18f6d/install.sh | sh
Manual install (if you already have uv)
uv tool install punt-z-spec
claude plugin marketplace add punt-labs/claude-plugins
claude plugin install z-spec@punt-labs
z-spec doctor
Verify before running
curl -fsSL https://raw.githubusercontent.com/punt-labs/z-spec/5b18f6d/install.sh -o install.sh
shasum -a 256 install.sh
cat install.sh
sh install.sh
Inside Claude Code:
/z-spec:setup all # Install fuzz and probcli
/z-spec:code2model the user authentication system # Generate your first spec
/z-spec:check docs/auth.tex # Type-check it
/z-spec:test docs/auth.tex # Animate and model-check
What /z-spec:setup installs
