Formal Agent Contracts
Documentation
A Claude Code plugin that brings formal methods to multi-agent development. Define inter-agent contracts in VDM-SL, run VDMJ syntax/type checks and proof-obligation generation, optionally check provable POs with Z3, and generate TypeScript/Python code with runtime contract enforcement. v2.0 adds Phase 2 design document generation (PROTOCOL.md, API-SIGNATURES.md) and contract test auto-generation; v2.2 adds per-module model routing to cut token cost — all through natural conversation with Claude.
What does it do?
When multiple AI agents collaborate to build a system, they need unambiguous agreements about inputs, outputs, and guarantees. Natural language specs are too vague; tests only cover the cases you write. This plugin lets you define mathematically precise contracts and combine specification-time mechanical checks, PO verification where proof is possible, and runtime contract checks. Test generation checks concrete cases; it is not mathematical proof.
Define
Natural language → VDM-SL
Verify
Syntax/type checks, PO generation
Prove
Check translated SMT formulas
Generate
TypeScript / Python code
Design Docs
NEWPROTOCOL.md generation
Test Gen
NEWGenerate finite-case contract tests
Import
MD spec → VDM-SL conversion
Export
VDM-SL → readable spec doc
Scope of Assurance
Using VDM-SL does not by itself mean something has been proved. Each step has a different assurance boundary.
Write a formal spec
Use VDM-SL to state types, pre/post-conditions, and invariants. This is not yet proof.
Check the spec
Run VDMJ syntax/type checks and PO generation. PO generation is the entry point to proof.
Prove properties
Z3 checks the translated SMT formula under its assumptions. Treating this as a result about the source VDM-SL property requires a separate check that the translation preserves meaning. It does not prove that generated code implements the specification.
Test behavior
Execute the spec or generated code on concrete cases. Finite tests are useful evidence, not proof.
No formal methods expertise required. Claude guides you through every step and explains results in plain language.
From writing tests to deriving them
Invariants, pre/post-conditions, and transition rules provide a basis for test expectations. They support test generation, but missing requirements and translation errors can remain. Review the mapping from specification to tests and execute the tests.
Boundaries and transitions enumerate themselves
A title-length constraint suggests 100/101-character boundary cases, and transition rules suggest transition tests. The generate-tests skill generates candidates; completeness and correct expectations still need review.
Practically unlimited volume
VDM-SL ships with combinatorial testing (traces): VDMJ expands operation-sequence templates into hundreds of thousands to millions of test sequences and runs reduced subsets. QuickCheck similarly explores proof obligations by sampling. The ceiling on test volume shifts from human effort to compute.
Re-derived whenever the spec changes
After a specification change, regenerate tests and record the requirement/specification revision and execution results. Missed regeneration and incorrect generated tests can still cause drift, so review the changes and rerun the tests.
That said, no volume of finite test runs amounts to proof (see Scope of Assurance above). This is exactly why the plugin pairs test generation with PO verification and Z3 proving.
Recent Features (v2.0–v2.2)
Phase 2 Design Document Generation
PROTOCOL.md records message type names and API-SIGNATURES.md records shared function signatures to connect the VDM-SL specification with detailed design. These documents provide a common reference for finding naming mismatches; their presence alone does not prevent them. Combine design review with executable contract tests.
Contract Test Auto-Generation
Auto-generate Jest/Vitest-compatible contract tests from both VDM-SL specifications (type invariants, pre/post-conditions) and design documents (PROTOCOL.md, API-SIGNATURES.md). Covers type validation, boundary values, protocol conformance, and state transition tests to detect spec-design-implementation drift at runtime.
Database Schema Derivation (v2.1.0)
Derive a database schema (DDL) from VDM-SL types and invariants by numbered mapping rules (R1–R18) — record types become tables, invariants become CHECK/UNIQUE/FK/trigger constraints. Infidelities the DDL cannot express (nat→BIGINT, transition rules, cross-row invariants) are logged in a DEVIATIONS retrenchment table with a concrete compensation, and a TRACEABILITY matrix maps every invariant to its enforcement point.
Model Routing (v2.2.0)
A heuristic selects a model tier (light / standard / heavy) from contract complexity signals. The workflow calls for escalation after two failed checks and applies the same VDMJ checks and contract tests. It does not guarantee quality or cost savings; report not-run, unknown, and failed checks separately and measure outcomes and cost.
Development Background
In AI-driven development of a multi-component system, skipping the detailed design phase (Phase 2) and generating code directly from VDM-SL specs led to integration bugs such as message type name mismatches. This was not a VDM-SL limitation — the root cause was the missing Phase 2 in the VDM-SL → detailed design → implementation flow. v2.0 closes this gap.
Documentation
Getting Started
Start HereGo from zero to your first contract-enforced agent in under 5 minutes. This guide covers installation, prerequisites, and your first end-to-end workflow.
Skills Reference
ReferenceComplete reference for all 15 skills: 8 forward skills (define-contract, verify-spec, smt-verify, generate-code, generate-tests, generate-db-schema, route-models, integrated-workflow) + 4 reverse skills (extract-spec, refine-spec, reconcile-code, reverse-workflow) + 2 import/export skills (import-natural-spec, export-human-spec) + the formal-methods-guide reference.
Examples & Tutorials
TutorialA complete walkthrough of the Task Manager example — from a one-sentence description to a VDMJ-checked specification and running TypeScript code with runtime contract enforcement.
Configuration & API
AdvancedRuntime contract settings, tool setup, VDM-SL type mapping reference, and environment variables for customizing the plugin behavior.
Evaluation Report
HistoricalA historical exploratory record of 30 fixtures. Controls include intentional gaps, and the old mutation runner counted execution errors as kills. Scores are preserved as history and cannot establish plugin effectiveness.
Quick Install
/plugin marketplace add anthropics/claude-plugins-community /plugin install formal-agent-contracts@claude-community
It is listed in Claude's official community directory, so you can also find it under Discover in the /plugin menu. Then say "run the full workflow for a new agent" and Claude will guide you through the entire pipeline.
Or, to get the newest release right away, add the repository directly (the official directory can lag a release behind):
/plugin marketplace add kotaroyamame/formal-agent-contracts /plugin install formal-agent-contracts@formal-agent-contracts