Getting Started
Go from zero to an agent with VDMJ syntax/type checks and runtime contract enforcement in under 5 minutes. This guide covers installation, prerequisites, and your first end-to-end workflow.
Prerequisites
The plugin runs inside Claude Code. You will also need the following tools for full functionality:
VDMJ
RequiredThe VDM-SL toolchain for syntax checking, type checking, and proof obligation generation.
- Java 11 or later
- Download from VDMJ Releases VDMJ Releases
- Unzip vdmj-suite-*-distribution.zip and add the vdmj.sh launcher to your PATH — or fetch the standalone jar from Maven Central to ~/.vdmj/vdmj.jar
Z3 Solver
OptionalSMT solver for automated proof of proof obligations. Only needed for the smt-verify skill.
pip install z3-solver
Node.js + Vitest/Jest
OptionalNeeded to run the contract tests produced by the generate-tests skill.
Installation
formal-agent-contracts is listed in Claude's official community directory. Install it from Discover in the /plugin menu, or with these commands:
/plugin marketplace add anthropics/claude-plugins-community /plugin install formal-agent-contracts@claude-community
To get the newest release right away, add the repository directly as a marketplace (the official directory can lag a release behind):
/plugin marketplace add kotaroyamame/formal-agent-contracts /plugin install formal-agent-contracts@formal-agent-contracts
Your First Contract in 5 Minutes
Let's define a simple agent contract, check its syntax and types, and generate working code — all through conversation with Claude.
Define the contract
Tell Claude what your agent does in plain language:
"Define a user registration agent. It takes a username and email, validates that the email contains @, and returns a user ID. The username must be 3-20 characters."
Claude generates a VDM-SL specification with types, pre-conditions, post-conditions, and invariants — plus Phase 2 design documents (PROTOCOL.md, API-SIGNATURES.md) covering message types, state transitions, and API signatures. It will ask clarifying questions if your requirements are ambiguous.
Verify the specification
Ask Claude to check your spec:
"Verify this specification"
VDMJ runs syntax and type checking, then generates proof obligations, and the design documents are checked for completeness and consistency with the spec. This is not proof completion; it identifies the obligations that can be proved later with tools such as Z3. Claude explains each PO in plain English.
Generate code
Ask Claude to generate an implementation:
"Generate TypeScript code from this spec"
Claude produces TypeScript (or Python) with every pre-condition, post-condition, and invariant compiled into runtime checks. If a contract is violated at runtime, you get a clear ContractError with the exact rule that was broken. Say "Generate contract tests" next and the generate-tests skill derives Jest/Vitest tests (type invariants, pre/post-conditions, state transitions, boundaries) from the spec and design documents.
Shortcut: Say "Run the full workflow for a registration agent" and Claude will execute each phase in order: Define → Syntax/type check → Prove where needed → Generate → Test.
Key Concepts
You don't need to know formal methods to use this plugin, but understanding three concepts will help you get the most out of it:
Pre-condition
preA rule that must be true before an operation runs. Example: "The task ID must exist in the board." If violated, the caller made an invalid request.
Post-condition
postA guarantee that is true after an operation completes. Example: "After deletion, the task ID is no longer in the board." If violated, the implementation has a bug.
Invariant
invA rule that must always be true. Example: "Task title length ≤ 100 characters." Checked every time a record is constructed.
Prompt Templates
Ready-made prompts to get started quickly. Replace {...} placeholders with your own domain.
Template 1: Simple (Single Agent)
Start minimal and let Claude ask follow-up questions to refine the spec.
Define a {AgentName} agent. [Data] - {Entity} has {Field1}, {Field2}, {Field3} - {If enums: Status is {Value1}/{Value2}/{Value3}} [Operations] - {Operation 1 description} - {Operation 2 description} [Rules] - {Business rule 1} - {Business rule 2}
Example: Inventory Management Agent
Define an inventory management agent. [Data] - Product has ProductID, Name, Stock, Category - Category is Food / Daily Goods / Electronics [Operations] - Receive stock (add specified quantity) - Ship stock (subtract specified quantity) - Query stock (return current stock by product ID) [Rules] - Stock must not go below 0 - Ship quantity must not exceed current stock - Product name must not be empty
Template 2: Multi-Agent
For systems where multiple agents collaborate. Explicitly state inter-agent dependencies.
Define contracts for the following multi-agent system. [System Overview] {What the system does — 1-2 sentences} [Agent Configuration] 1. {Agent A} — {Role} 2. {Agent B} — {Role} [Inter-Agent Dependencies] - After {Agent A}'s {OperationX}, {Agent B}'s {OperationY} is called [Shared Data Types] - {TypeName}: {Description} [Key Rules per Agent] - {Agent A}: {Constraint} - {Agent B}: {Constraint}
Example: EC Order Processing
Define contracts for the following multi-agent system. [System Overview] EC site order processing. Three agents coordinate: Order → Inventory → Payment. [Agent Configuration] 1. OrderAgent — Order acceptance and management 2. InventoryAgent — Stock reservation and release 3. PaymentAgent — Payment processing [Inter-Agent Dependencies] - After OrderAgent's ConfirmOrder, InventoryAgent's ReserveStock is called - After ReserveStock succeeds, PaymentAgent's Charge is called - If Charge fails, InventoryAgent's ReleaseStock restores stock [Key Rules per Agent] - OrderAgent: Paid orders cannot be cancelled - InventoryAgent: Stock must not go below 0 - PaymentAgent: Cannot capture payment without prior authorization
Template 3: Integrated Workflow (End-to-End)
Run the full pipeline — define, syntax/type check, prove where needed, generate, test — in one shot.
Run the integrated workflow for {SystemName}. [Domain] {What the system is for} [Data] - {Entity and its fields} [Operations] - {OperationName}: {What it does} ({Precondition if any}) [Absolute Rules] - {Invariant / business rule} [Target Language] {TypeScript / Python}
Example: Meeting Room Reservation
Run the integrated workflow for a reservation management system. [Domain] Meeting room reservations. Prevent double-booking at the specification level. [Data] - Room: RoomID, Name, Capacity - Reservation: ReservationID, RoomID, StartTime, EndTime, BookedBy [Operations] - CreateReservation: Create a new reservation (no time overlap in same room) - CancelReservation: Cancel a reservation (reservation must exist) [Absolute Rules] - No overlapping reservations for the same room - StartTime < EndTime [Target Language] TypeScript
Template 4: Formalize Existing Spec
When you already have a natural-language spec or API definition, paste it directly for formalization.
Convert the following spec into a VDM-SL formal specification. --- {Paste your existing spec or API definition here} --- Pay special attention to formalizing: - {Ambiguous area 1} - {Ambiguous area 2} After formalizing, run verification.
Template 5: Generate Contract Tests
Turn a verified spec (and its design documents) into executable contract tests.
Generate contract tests from {SpecFile}. [Input] - VDM-SL spec: {path} - {If design docs exist: paths to PROTOCOL.md / API-SIGNATURES.md} [Output] - Test framework: {Vitest / Jest} - Target implementation: {path to the implementation under test} Cover type invariants, pre/post-conditions, boundary values{, and state transitions}.
Tips for Writing Prompts
- Be specific about rules — "Stock must not go below 0" is better than "validate stock". Boundary values produce precise pre/post/invariant conditions.
- State inter-agent call order — "A.post → B.pre" is the core of multi-agent contracts. Making this explicit enables cross-agent verification.
- Start small — Use Template 1 and let Claude ask follow-up questions. The verify phase will surface missing edge cases.
- Use "Run the integrated workflow" for end-to-end — Triggers the pipeline (define → syntax/type check → prove where needed → generate → test) with error-recovery support.
MD→VDM-SL→MD Pipeline
A workflow that takes an existing incomplete specification (Markdown) as input, systematically detects and resolves ambiguities through VDM-SL conversion, and regenerates a natural language specification from VDMJ-checked VDM-SL. This is also the core mechanism behind Template 4 "Formalize Existing Spec."
Core of the Pipeline
The very act of attempting to convert natural language to VDM-SL functions as ambiguity detection. When you try to write type definitions, pre-conditions, or post-conditions, the "parts you cannot write" emerge structurally—because the original natural language specification is ambiguous.
import-natural-spec
Reads the Markdown specification and attempts VDM-SL conversion. Parts that cannot be converted are detected as ambiguities.
Resolve ambiguities through dialogue
Detected ambiguities are presented to the user in priority order to confirm interpretations.
verify-spec
Runs VDMJ for syntax checking, type checking, and proof obligation (PO) generation to mechanically check specification consistency. This does not mean the POs have been proved.
export-human-spec
Reverse-converts VDMJ-checked VDM-SL into a structured Markdown specification reviewable by domain experts.
7 Ambiguity Patterns
Attempting VDM-SL conversion structurally exposes these seven types of ambiguity:
- Vague quantifiers — "multiple" cannot define a type (seq? set? upper bound?)
- Undefined terms — the states of "active" are not enumerated
- Implicit constraints — rules not stated, e.g., whether proxy orders are allowed
- Missing error cases — behavior on payment failure is undefined
- Ambiguous relationships — one-to-many or many-to-many is unclear
- Temporal ambiguity — strictness of processing order is unknown
- Boundary conditions — inclusive or exclusive (≤ vs <) is unclear
Priority-Ordered Dialogue Resolution
Detected ambiguities are classified into three priority levels and resolved sequentially through user dialogue. AI never silently resolves ambiguity; every interpretation choice is presented to the user.
Blocking — Cannot write VDM-SL type definitions (resolved first)
Important — Affects pre-conditions or post-conditions
Clarifying — Makes the specification more precise
Traceability and VDMJ Verification
The generated VDM-SL specification maintains bidirectional traceability by carrying [REQ-nnn] tags and original natural language text as comments for each element. After mechanical checking via VDMJ (syntax checking, type checking, and proof obligation generation), the pipeline proceeds to the next step.
Reverse Conversion to Natural Language
The VDMJ-checked VDM-SL is converted into a structured specification document reviewable by domain experts and non-technical stakeholders. Translation rules:
typesType definitions → "What things exist"
prePre-conditions (pre) → "Prerequisites"
postPost-conditions (post) → "Guarantees"
invInvariants (inv) → "Rules that always hold"
This natural language specification is a derived artifact; the VDM-SL is the source of truth. Modification requests from stakeholder review flow back through VDM-SL update → verification → regeneration.