punt-labs/z-spec

3 stars · Last commit 2026-04-11

Creates, validates, and animates Z specifications from source code and generates code from specifications

README preview

# Z Specification Plugin for Claude Code

> Formal Z specifications and B machines that type-check, animate, and refine --- from English to math to code.

[![License](https://img.shields.io/github/license/punt-labs/z-spec)](LICENSE)
[![CI](https://img.shields.io/github/actions/workflow/status/punt-labs/z-spec/docs.yml?label=CI)](https://github.com/punt-labs/z-spec/actions/workflows/docs.yml)
[![Working Backwards](https://img.shields.io/badge/Working_Backwards-hypothesis-lightgrey)](./prfaq.pdf)

**Platforms:** macOS, Linux

## What is Z?

[Z](https://en.wikipedia.org/wiki/Z_notation) ("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](https://www.iso.org/standard/21573.html).

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

View full repository on GitHub →