Formal Agent Contracts
Documentation
A Claude Code plugin that brings formal methods to multi-agent development. Define inter-agent contracts in VDM-SL, verify them automatically, prove correctness 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 — 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 that are verified at specification time and enforced at runtime.
Define
Natural language → VDM-SL
Verify
Syntax, types, proof obligations
Prove
SMT-LIB + Z3 solver
Generate
TypeScript / Python code
Design Docs
NEWPROTOCOL.md generation
Test Gen
NEWAuto-generate contract tests
Import
MD spec → VDM-SL conversion
Export
VDM-SL → readable spec doc
No formal methods expertise required. Claude guides you through every step and explains results in plain language.
What's New in v2.0
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.
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.
Development Background
While developing a hybrid-chatbot project (3-component real-time chat system) using AI-driven development, skipping the detailed design phase (Phase 2) and going directly from VDM-SL specs to code generation caused 5 integration bugs. This was not a VDM-SL limitation — the root cause was the absence of Phase 2 in the VDM-SL → detailed design → implementation flow. v2.0 supports this architect improvement.
Documentation
Getting Started
Start HereGo from zero to a verified, 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 14 skills: 8 forward skills (define-contract, verify-spec, smt-verify, generate-code, integrated-workflow, formal-methods-guide, import-natural-spec, export-human-spec) + 4 reverse skills (extract-spec, refine-spec, reconcile-code, reverse-workflow) + 2 new v2.0 skills (define-protocol, generate-tests).
Examples & Tutorials
TutorialA complete walkthrough of the Task Manager example — from a one-sentence description to verified, 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. Statistically significant effects confirmed across 30 data points (3 tasks × 5 trials).
Quick Install
/plugin marketplace add kotaroyamame/formal-agent-contracts
Then say "run the full workflow for a new agent" and Claude will guide you through the entire pipeline.