The formal methods community has been working on verified software for decades. Leslie Lamport’s TLA+ [1] specifies concurrent systems. Alloy [2] models structural properties. Lean [3] and Coq [4] prove theorems about programs. Dafny [5] verifies code against specifications at compile time. This is deep, serious work with a long lineage. None of these notations compete; each serves different verification needs.
One significant barrier to adoption was always the cost. Writing a formal spec for a notification scheduler or an authentication flow takes hours of skilled effort. Most teams can’t justify that investment for most features. The time required to learn and apply these techniques is time most businesses never give their engineers. The specification stays in the textbook.
We hypothesize that AI changes that. It lowers not just the cost of writing specs but the cost of learning and consistently applying them. If an AI agent can teach you the notation, draft an initial spec, and help you refine it, formal methods become approachable and practical for ordinary projects. Our Z Spec plugin is how we’re testing that hypothesis. It starts with Z, adds early support for B, and more notations will follow.
The Notation
The notation we’re using is Z, a schema language grounded in set theory and first-order predicate logic, developed at the University of Oxford and standardized as ISO 13568 [6]. Our interest in Z comes from Andrew Simpson’s Software Engineering Mathematics and State-Based Modelling courses in Oxford’s Department of Computer Science [10], where formal specification is taught as a practical engineering discipline. It is a tool for reasoning about systems before building them, not just theory.
A Z schema describes a system as a set of states, invariants that constrain those states, and operations that transition between them. When the type-checker (fuzz [7]) accepts a specification, the system description is internally consistent. When the animator (ProB [8]) explores the state space, you see every reachable configuration. That includes ones you forgot to think about.
Not Waterfall
Z Spec is not “write a spec, then generate code.” That’s waterfall with extra steps.
The plugin has three core commands that work in any direction:
model2codegenerates an implementation from a Z spec. The spec defines the acceptance criteria; Claude writes code that satisfies the schema.code2modelextracts a Z spec from existing code. Now you have a formal description of what your code actually does, which may differ from what you intended.auditcompares an existing spec against existing code, finding where implementation diverges from specification.
You can start from either end. Write a spec first and generate code from it. Or write code first and extract a spec to verify your assumptions. Or do both independently and audit the gap. The workflow is iterative, not sequential.
Case Study: Koch Trainer
Koch Trainer is an iOS Morse code app where formal specification drove the implementation iteratively. It grew not all at once but domain by domain as complexity demanded it.
The first spec modeled training sessions and learner state, covering spaced repetition scheduling, character progression, and accuracy tracking. That spec was type-checked, animated, and used to generate the core Swift implementation. Then the half-duplex radio simulation (the kind found in ham radio rigs) needed its own state model, covering transmit/receive switching, squelch behavior, and timing constraints. A second spec captured that domain. Finally, the keyer got its own spec. A keyer is a deeply complex electromechanical device with iambic squeeze logic, dit/dah memory, and precise timing ratios. Each domain was specified and implemented independently, then composed in the app. The specs are committed to the repository as both LaTeX source and compiled PDFs. Both are equally readable by the developer reviewing a pull request and the agent generating the implementation.
The audit maps every Z invariant, precondition, effect, and bound to its corresponding test. It found that the half-duplex radio model had no guard preventing keying while in receive mode. The Z spec expressed that constraint as ¬(radioMode = receiving ∧ toneActive). The session counter could theoretically report more correct answers than total attempts. The spec’s invariant correct ≤ attempts made that visible. Neither bug had been caught by existing tests because no test happened to exercise those specific state combinations.
The fix wasn’t more tests. It was domain types that make violations structurally impossible. Radio.key() throws unless radioMode = transmitting. SessionCounter.recordAttempt() always increments attempts before correctness. The spec identified the missing constraints; enforcing those constraints through the type system brought coverage from 71% to 89%.
Eric Bowman, CTO of King, used Z Spec’s audit on an iOS notification scheduler and found two bugs in the same category. The system was notifying when it shouldn’t have been. The spec’s invariants caught them structurally, not through test cases that happened to cover the right scenario. As he put it: “Z-spec skill is a real game changer… Not sure whether to sell this pick to the miners or use it to go after gold.”
Why Now
Hand-writing a Z spec for a notification scheduler was always the right approach. It just took more time to learn and apply than most teams had. When Claude produces an initial draft that fuzz can verify and you can refine, a cycle that takes minutes instead of hours, the cost collapses. What remains is the payoff: a mathematically precise definition that catches an entire class of bugs, not just the specific inputs you thought to test. The audience isn’t people who should have been doing this all along. It’s practitioners who knew the value but faced real constraints, and we believe AI can remove them.
We haven’t tested this beyond our own projects. We don’t yet know how it holds up at scale, across notations beyond Z, or in the hands of engineers who didn’t write the specs themselves. It’s a question we’re also pursuing through a masters dissertation in Oxford’s Professional Software Engineering programme.
References
- Lamport, L. “TLA+: Temporal Logic of Actions.” lamport.azurewebsites.net
- Jackson, D. “Alloy: A Language and Tool for Exploring Software Designs.” alloytools.org
- “Lean Theorem Prover.” lean-lang.org
- “The Coq Proof Assistant.” coq.inria.fr
- Microsoft Research. “Dafny.” dafny.org
- ISO. “ISO/IEC 13568: Z Formal Specification Notation.” 2002. iso.org
- Spivey, M. “fuzz: The Z Type Checker.” spivey.oriel.ox.ac.uk
- “ProB: The Animator and Model Checker.” prob.hhu.de
- Anthropic. “Claude Code.” 2024–present. docs.anthropic.com
- Simpson, A. “Software Engineering Mathematics” and “State-Based Modelling.” Department of Computer Science, University of Oxford. cs.ox.ac.uk