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
SMT proof within PO scope
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
Use Z3 or another prover to prove POs. The result is limited to properties formalized as proof obligations.
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
One of the biggest payoffs of a rigorous specification is testing. Invariants, pre/post-conditions, and transition rules are themselves test oracles: they define what "correct" means. Instead of hand-writing test cases one by one, you derive them from the spec mechanically.
Boundaries and transitions enumerate themselves
Write "title is at most 100 characters" and the 100/101-character boundary tests follow; write the transition rules and the generate-tests skill enumerates every transition pattern.
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
Tests are derived from the spec as a single source of truth, so when the spec changes you simply regenerate. The staleness and drift that plague hand-written test suites structurally cannot happen.
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
Improves the bridge from VDM-SL specifications (Phase 1) to detailed design (Phase 2). PROTOCOL.md manages message type names as Single Source of Truth, while API-SIGNATURES.md defines shared module function signatures. Structurally prevents 'message type name mismatch' and 'field name drift' bugs by enriching the detailed design phase. verify-spec now also checks design documents for completeness.
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)
Routes each module to the lightest capable model tier (light / standard / heavy) based on objective complexity signals in the contract itself — implicit definitions, invariants, quantifiers, PO counts — cutting token cost in the code- and test-generation phases. Verification gates are unchanged: whichever model generates the artifact, the same VDMJ checks and contract tests judge it, and a module that fails verification twice escalates one tier automatically.
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
NEWQuantitative comparison experiment between plugin users and non-users. Exploratory results across 30 trials (3 tasks × 5 trials per group) suggest positive effects on spec coverage and test 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