Z Spec

Why this exists

Z notation has been around since the 1970s. Mike Spivey’s fuzz type-checker has been verifying Z specifications since 1988. The ProB animator and model-checker from HHU Düsseldorf has been exploring state spaces since 2003. The mathematics is settled. The toolchain works. The problem was never the tools — it was the distance between a working engineer and the tools.

Writing a Z specification for a session scheduler or an authentication flow takes hours of skilled effort. Learning the notation takes longer. Most teams could not justify either investment for most features, and the businesses they worked in rarely gave them the time. The specification stayed in the textbook.

We think AI changes that equation. When an AI agent can draft an initial spec from your existing code, explain the notation as you refine it, and run the type-checker and model-checker on your behalf, formal methods become practical for ordinary projects. Z Spec is how we’re testing that hypothesis inside Claude Code. Our contribution is a wrapper that shortens the path to Spivey’s and HHU Düsseldorf’s tools — not the tools themselves, and not the mathematics behind them.

This isn’t our invention. It is Oxford’s Z notation, Spivey’s type-checker, and HHU Düsseldorf’s model-checker, made accessible without the time penalty.

What you can do with it

Z Spec provides six slash commands inside Claude Code:

• /z-spec:code2model — Extract a Z specification from existing code. You get a formal description of what your code actually does, which may differ from what you intended.
• /z-spec:check — Type-check a specification with fuzz. If the checker accepts it, the system description is internally consistent.
• /z-spec:test — Animate and model-check with ProB. The tool explores the state space and shows every reachable configuration, including ones you forgot to think about.
• /z-spec:partition — Derive test cases from the specification using TTF testing tactics. Coverage comes from the spec’s structure, not from guessing inputs.
• /z-spec:audit — Compare specification against implementation. Find where the code diverges from what the spec promises.
• /z-spec:model2code — Generate an implementation from a specification. The spec defines the acceptance criteria; Claude writes code that satisfies the schema.

The workflow is not sequential. You can start from code and extract a spec, start from a spec and generate code, or maintain both independently and audit the gap.

Beyond Z

Z is our starting point, not our boundary. Z Spec also supports B-Method — Jean-Raymond Abrial’s refinement-oriented notation, which adds a discipline for progressively transforming abstract specifications into executable code. You can create, type-check, animate, and refine B machines through the same slash-command interface.

We’re experimenting with three more verification surfaces. Lean 4 proof obligations let you state properties about a specification and attempt machine-checked proofs. Runtime contracts generate executable assertions that monitor program state against spec invariants during actual operation. Property-based oracle testing uses the specification as the oracle for generative tests — the spec says what should be true, and the test framework generates thousands of cases to check it.

These are at varying stages of maturity. We’re sharing them because they’re usable, not because they’re finished.

Worked example

Koch Trainer is an iOS Morse code app where formal specification drove the implementation. The first Z spec modeled training sessions and learner state — spaced repetition scheduling, character progression, accuracy tracking. That spec was type-checked, animated with ProB, and used to generate the core Swift implementation. ProB’s state-space exploration surfaced a session-resume bug: the half-duplex radio model had no guard preventing keying while in receive mode. The Z invariant made the missing constraint visible; the fix was a domain type that makes the violation structurally impossible. Neither bug had been caught by existing tests because no test happened to exercise those state combinations. The app shipped to the App Store with specs committed alongside the source — readable by the developer reviewing a pull request and the agent generating the implementation.