Examples & Tutorials
A 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.
Task Manager — Full Workflow Example
This example was built with the integrated workflow, checked with VDMJ, and selected POs were checked with SMT. The full source code is available at examples/task-manager/. examples/task-manager/
38
Proof obligations generated
23 / 23
Smoke tests passed
13
Runtime contract checks
Define — VDM-SL Specification
The task manager manages tasks with IDs, titles, descriptions, status (Todo / InProgress / Done), priority (Low / Medium / High), and optional assignees. The key business rule: once a task is Done, it cannot transition back to Todo or InProgress.
module TaskManager definitions types TaskId = nat1; Priority = <Low> | <Medium> | <High>; Status = <Todo> | <InProgress> | <Done>; Task :: id : TaskId title : seq1 of char desc : seq of char status : Status priority : Priority assignee : [seq1 of char] inv t == len t.title <= 100 and len t.desc <= 500; TaskBoard = map TaskId to Task inv board == forall id in set dom board & board(id).id = id; functions ValidTransition: Status * Status -> bool ValidTransition(fromSt, toSt) == if fromSt = toSt then true else if fromSt = <Done> then false else true; operations CreateTask: seq1 of char * seq of char * Priority * [seq1 of char] ==> TaskId CreateTask(title, desc, priority, assignee) == ... pre len title <= 100 and len desc <= 500 post RESULT in set dom board and board(RESULT).status = <Todo>; ChangeStatus: TaskId * Status ==> () ChangeStatus(taskId, newStatus) == ... pre taskId in set dom board and ValidTransition(board(taskId).status, newStatus) post board(taskId).status = newStatus; DeleteTask: TaskId ==> () DeleteTask(taskId) == ... pre taskId in set dom board post taskId not in set dom board and card dom board = card dom board~ - 1; end TaskManager
Key contracts: inv on Task enforces title/desc length limits. pre on ChangeStatus enforces valid transitions. post on DeleteTask guarantees exactly one removal.
Verify — VDMJ Results
✅ Parsed 1 module. No syntax errors ✅ Type checked 1 module. No type errors 📋 Generated 38 proof obligations Key POs: PO 8 — State init obligation: initial state satisfies invariant PO 22 — CreateTask postcondition: RESULT is in dom board with status <Todo> PO 27 — ChangeStatus postcondition: status updated, title preserved PO 36 — DeleteTask postcondition: taskId removed, board size decreased by 1
38 POs were generated automatically. These cover type obligations, subtype constraints, state invariant preservation, and operation post-condition correctness. Each was explained in plain language by Claude.
Prove — SMT Verification
3 representative POs converted to SMT-LIB and verified:
PO 8 (state init): ✅ Proved — empty board satisfies invariant PO 27 (ChangeStatus post): ✅ Proved — status updated, title preserved PO 36 (DeleteTask post): ✅ Proved — taskId removed, size decreased
Generate — TypeScript Code
The VDM-SL spec was compiled to TypeScript with runtime contract checks. Generated changeStatus method:
changeStatus(taskId: TaskId, newStatus: Status): void { // Pre-conditions (from VDM-SL) checkPre(this.board.has(taskId), `taskId ${taskId} not in dom board`); checkPre(validTransition(oldTask.status, newStatus), `Invalid transition: ${oldTask.status} → ${newStatus}`); const oldTitle = oldTask.title; const updated = mkTask(oldTask.id, oldTask.title, oldTask.desc, newStatus, oldTask.priority, oldTask.assignee); this.board.set(taskId, updated); // Post-conditions (from VDM-SL) checkPost(this.board.get(taskId)!.status === newStatus, `status must be ${newStatus}`); checkPost(this.board.get(taskId)!.title === oldTitle, `title must be preserved`); this.checkStateInvariant(); }
Every pre, post, and inv from the VDM-SL spec becomes a runtime checkPre/checkPost/checkInv call. Violations throw a ContractError with the exact violated rule.
Test — Smoke Test Results
=== TaskManager: Integrated Workflow Smoke Test === --- 1. Task Creation --- ✓ CreateTask: 'Design API' (High, Alice) ✓ CreateTask: 'Write Tests' (Medium, Bob) ✓ CreateTask: empty title rejected ✓ CreateTask: title > 100 chars rejected ✓ CreateTask: desc > 500 chars rejected --- 2. Status Transitions --- ✓ ChangeStatus: Todo → InProgress ✓ ChangeStatus: InProgress → Done ✓ ChangeStatus: Done → InProgress rejected ✓ ChangeStatus: Done → Todo rejected ✓ ChangeStatus: Todo → Todo (no-op) --- 3. Update & Delete --- ✓ UpdateTask: title & priority changed, status preserved ✓ DeleteTask: board size decreased by 1 ✓ DeleteTask: already deleted taskId rejected --- 5. Board Summary --- ✓ GetSummary: counts match board size --- 7. Invariant Enforcement --- ✓ mkTask: TaskId=0 (nat1) rejected ✓ mkTask: empty title (seq1 of char) rejected === Results: 23 passed, 0 failed ===
All 23 tests passed. Valid inputs succeed; invalid inputs (empty title, forbidden transitions, non-existent IDs) are caught by the generated contract checks with clear error messages. Since v2.0.0, the generate-tests skill can also produce a full Vitest/Jest contract test suite (type-invariant, pre/post-condition, state-transition, and boundary tests) from the spec and design documents.
Contract Patterns
The plugin includes 7 built-in contract templates for common agent architectures — v2.0.0 adds a Phase 2 design-document template and a hybrid decision agent. Use these as starting points when defining new agents.
Transform Agent
Stateless input → output conversion. Example: a translation agent that converts text between languages.
CRUD Agent
Create/Read/Update/Delete with persistent state. Example: the Task Manager shown above.
Pipeline Agent
Sequential data processing stages. Example: an ETL agent that extracts, transforms, and loads data.
Mediator Agent
Orchestrates multiple sub-agents. Example: an order processor that coordinates inventory, payment, and shipping.
Validation Agent
Validates input data against compound constraints and reports precise errors. Example: composite constraint checks with structured error reporting.
Design Document Template (v2.0.0)
Generates Phase 2 design documents (PROTOCOL.md, API-SIGNATURES.md): message type registry, payload structures, state transition matrix, and API signatures.
Hybrid Decision Agent (v2.0.0)
Score-based compound decisions: score calculation, threshold comparison, and decision logic.