skills.rest
nrdxp
nrdxpCOMMUNITY
Explore all skills by this author →
WebsiteGitHub

spec

Formalize normative behavioral constraints and map them to executable test invariants.

10|2|Updated Jan 24, 2026
Search Tags:#specification#formal verification#invariants#alloy#behavioral contracts#bcp 14#test invariants
One-click install
npx skills add https://github.com/nrdxp/predicate --skill spec-nrdxp
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: spec
Source: https://github.com/nrdxp/predicate/tree/main/skills/spec
Command: npx skills add https://github.com/nrdxp/predicate --skill spec-nrdxp

SYSTEM DOCUMENTATION & REQUIREMENTS

What problem does it solve? Implicit behavioral assumptions and unwritten invariants cause implementation drift and costly corrective loops. This Skill turns vague expectations into explicit, verified normative specifications that deterministically constrain code generation. ## Core Features & Use Cases - Five-Step Specification Workflow: Identify, Formalize, Verify, Record, and Connect constraints using BCP 14 normative keywords (MUST, MUST NOT, SHOULD, MAY). - Tiered Formalism Selection: Scales notation from structured prose to Alloy/TLA+ to Lean/Coq proofs based on system criticality, with mandatory verification at every tier. - Test Invariant Mapping: Links every named constraint to an executable test invariant so specifications become deterministic verification targets. - Use Case: When designing a session protocol, invoke the workflow to formalize invariants like "sessions MUST NOT spawn without authentication", verify consistency, and generate the corresponding test assertions before implementation begins. ## Quick Start Invoke the spec workflow to formalize the behavioral invariants and forbidden states for my authentication module into a verified specification.

Frequently Asked Questions about spec

High-intent search queries and answers about installing and using this skill.

FAQPage Schema
How do I write a formal specification for software behavior?▼

Follow the five-step workflow: identify constraints from models and failure modes, formalize them with BCP 14 keywords and typed references, verify consistency, record the artifact in docs/specs/, and connect each constraint to a test invariant.

What is the difference between a model and a specification?▼

A model is descriptive, mapping states and transitions, while a specification is normative, declaring invariants that MUST hold. This workflow produces specifications; structural modeling belongs to the separate form workflow.

When should I use Alloy or TLA+ instead of prose specifications?▼

Use prose for simple MUST/MUST NOT constraints, Alloy or TLA+ when constraints involve state transitions, concurrency, or relational structure, and full proof assistants like Lean or Coq for cryptographic or safety-critical systems.

What do the VERIFIED tags on constraints mean?▼

Each constraint carries a verification tag: proof for formal proofs, machine for model-checked consistency, agent-check for self-verification, or UNVERIFIED with a deferral rationale. Untagged constraints are protocol violations.

Can I write a specification without an existing system model?▼

Yes. The workflow supports create mode for new domains and apply mode for extracting implicit constraints from existing systems. Inline type declarations can replace formal model references when no model exists.

Related Skills

Explore More Software Engineering Skills→
organvm-i-theoriaorganvm-i-theoria

knowledge-architecture

Design knowledge systems using ontological principles that organize entities by essential nature.

Official
Intermediate
Kevin-Liu-01Kevin-Liu-01
16

refine

Coordinate and run seven-pass quality gates over changed code.

Community
Advanced
HyperxqHyperxq
1

lefthook

Enforce Conventional Commits and run Git hooks via Lefthook.

Community
Intermediate
ssmleossmleo

govfolio-schema-contracts

Manage and verify domain schemas and OpenAPI contract boundaries for API services.

Community
Intermediate