Configuration & API
Runtime contract settings, tool setup, VDM-SL type mapping reference, and environment variables for customizing the plugin behavior.
Runtime Contract Enforcement
Generated TypeScript and Python code includes runtime checks for every pre-condition, post-condition, and invariant. These checks can be toggled at the code generation phase.
Enabled (default)
RecommendedAll contract violations throw a ContractError at runtime with a descriptive message identifying the exact rule that was broken.
checkPre(taskId in board, "taskId must exist in board");
Disabled
Contract checks are omitted from generated code. Use only when performance is critical and the required proof obligations have been proved with SMT.
"Generate code without runtime checks"
Disabling runtime checks removes your last line of defense. Only do this after all proof obligations have been proved with Z3.
Contract Error Types
When a contract is violated at runtime, the generated code throws a typed error that identifies the category and the specific rule.
| Check Function | VDM-SL Origin | When It Fires |
|---|---|---|
checkPre() | pre clause | Before operation executes — caller sent invalid input |
checkPost() | post clause | After operation completes — implementation has a bug |
checkInv() | inv clause | On record construction — data would violate a type constraint |
checkStateInvariant() | State inv | After any state mutation — global invariant would be broken |
VDMJ Setup
VDMJ is the Java-based VDM toolchain used for syntax checking, type checking, and proof obligation generation. It is required for the verify-spec, smt-verify, and integrated-workflow skills.
Installation Steps
1. Install Java 11 or later (verify with java -version).
2. Download the standalone VDMJ JAR (vdmj-4.7.0.jar) from Maven Central, or the vdmj-suite-*-distribution.zip (with the vdmj.sh launcher) from the nickbattle/vdmj GitHub releases.
3. Place the JAR at the default location:
mkdir -p ~/.vdmj cp vdmj-*.jar ~/.vdmj/vdmj.jar
4. Verify the installation:
java -jar ~/.vdmj/vdmj.jar -help
VDMJ Commands Used by the Plugin
| Command | Purpose |
|---|---|
java -jar vdmj.jar -vdmsl file.vdmsl | Syntax and type checking |
java -jar vdmj.jar -vdmsl -p file.vdmsl | Generate proof obligations |
java -jar vdmj.jar -vdmsl -i file.vdmsl | Interactive interpreter (for testing) |
Z3 Integration
Z3 is an SMT solver used to automatically prove proof obligations generated by VDMJ. It is optional — the plugin works without it, but the smt-verify skill requires it.
Install
pip install z3-solver
Alternatively, install Z3 binaries directly from the Z3Prover/z3 GitHub releases page and add z3 to your PATH.
SMT-LIB Output Format
The plugin converts VDM-SL proof obligations to SMT-LIB 2.6 format. Each PO becomes a .smt2 file that Z3 can check independently. The verification strategy is refutation-based:
; Assert the negation of the PO (assert (not <proof-obligation>)) (check-sat) ; unsat → PO is proved (no counterexample exists) ; sat → counterexample found (PO may be false) ; unknown → solver timeout
Test Runner Setup
The generate-tests skill (new in v2.0.0) emits contract tests for Vitest or Jest from your VDM-SL specification and Phase 2 design documents (PROTOCOL.md, API-SIGNATURES.md). Install Node.js, then add a test runner to your project:
npm install -D vitest # or: npm install -D jest
VDM-SL Type Mapping
The code generator maps VDM-SL types to TypeScript and Python equivalents. The table below shows the mappings used by the generate-code skill.
| VDM-SL Type | TypeScript | Python | Notes |
|---|---|---|---|
bool | boolean | bool | — |
nat | number | int | Runtime check: ≥ 0 |
nat1 | number | int | Runtime check: ≥ 1 |
int | number | int | — |
real | number | float | — |
char | string | str | Single character |
seq of X | X[] | list[X] | Can be empty |
seq1 of X | X[] | list[X] | Runtime check: length ≥ 1 |
set of X | Set<X> | set[X] | — |
map X to Y | Map<X, Y> | dict[X, Y] | — |
[X] | X | null | Optional[X] | Optional type |
X | Y | Z | X | Y | Z | Union[X, Y, Z] | Union type |
<A> | <B> | enum / string literal | Enum | Quote types → enums |
T :: f1: X f2: Y | interface | @dataclass | Record type with named fields |
Environment Variables
The plugin defines no environment variables. The skills expect the standalone VDMJ JAR at ~/.vdmj/vdmj.jar (or vdmj.sh from the distribution ZIP on your PATH) and the z3 binary on your PATH.
Plugin File Structure
The plugin installs the following structure into your Claude Code environment. Each skill is self-contained with its own SKILL.md and optional reference files.
formal-agent-contracts/ ├── .claude-plugin/ │ ├── plugin.json # Plugin metadata and version │ └── marketplace.json ├── skills/ # 15 skills, each with SKILL.md (+ references/) │ ├── define-contract/ # contract-templates.md (7 patterns incl. Phase 2 design docs) │ ├── verify-spec/ # vdmj-setup.md │ ├── smt-verify/ # SMT conversion & type-mapping rules │ ├── generate-code/ # typescript-rules.md, python-rules.md │ ├── generate-tests/ # test-templates.md (new in v2.0.0) │ ├── generate-db-schema/ # vdm-to-sql-mapping.md, deviation-patterns.md (new in v2.1.0) │ ├── route-models/ # routing-rules.md (new in v2.2.0) │ ├── integrated-workflow/ # workflow-phases.md, session-report-template.md │ ├── extract-spec/ │ ├── refine-spec/ │ ├── reconcile-code/ │ ├── reverse-workflow/ │ ├── import-natural-spec/ │ ├── export-human-spec/ │ └── formal-methods-guide/ # vdm-sl-syntax.md, po-types-detail.md (38 PO types) ├── examples/ │ └── task-manager/ # Complete working example ├── eval/ # Evaluation framework (tasks, runs, results) ├── design/ # Design documents ├── prompt-templates.md # 7 ready-to-use prompt templates ├── README.md └── LICENSE