Claude Tools / MCP Servers / z-spec-dev

MCP Servers · punt-labs/z-spec

z-spec-dev

Create, validate, and test formal Z specifications for stateful systems using fuzz and probcli

CLEARED_STATICmcp-portablev0.18.0

Pipeline results

Coverage

CLEARED_STATIC

Tests run

7 / 8

Portability

MCP-portable

Type

MCP Servers

Tests & results

What the pipeline checked

TestStateResult or reason

eligibilityranall eligibility checks passed

dedupranunique -- no near-duplicate found

clocran43810 code lines / 296 files

secretsranno secret patterns matched

egressran4 lexical match(es) — FLAG-INFO (C-01: semantic analysis deferred to v2)

injectionranno patterns matched (confidence: STANDARD)

required-fieldsranrequired fields present: name, version, description

behaviouraldeferredbehavioural assessment deferred (v1): Python with non-stdlib imports (committed-only policy): [('tests/test_gate.py', '__future__'), ('tests/test_gate.py', 'punt_zspec')]

What's inside

Components found

commands/audit-dev.md

componentlow

commands/audit.md

componentlow

commands/b-animate-dev.md

componentlow

commands/b-animate.md

componentlow

commands/b-check-dev.md

componentlow

commands/b-check.md

componentlow

commands/b-create-dev.md

componentmedium

commands/b-create.md

componentmedium

commands/b-refine-dev.md

componentlow

commands/b-refine.md

componentlow

commands/check-dev.md

componentlow

commands/check.md

componentlow

commands/cleanup-dev.md

componentlow

commands/cleanup.md

componentlow

commands/code2model-dev.md

componentlow

commands/code2model.md

componentlow

commands/contracts-dev.md

componentmedium

commands/contracts.md

componentmedium

commands/disable-dev.md

componentlow

commands/disable.md

componentlow

Coverage

Not assessed

behavioural execution not run
egress patterns logged (FLAG-INFO): 4 lexical match(es)

README

From the repository

# 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

The specification says *what* a system does, not *how*. When …

← Back to MCP Servers