設定とAPI
ランタイム契約設定、ツール設定、VDM-SL型マッピングリファレンス、プラグイン動作カスタマイズ用環境変数。
ランタイム契約エンフォースメント
生成されたTypeScriptとPythonコードには、すべての事前条件、事後条件、不変条件のランタイムチェックが含まれます。これらチェックはコード生成フェーズで切り替え可能。
有効（デフォルト）
推奨契約違反はすべてランタイム時にContractErrorをスロー。違反された正確なルールを識別する説明的メッセージを含む。
checkPre(taskId in board, "taskId must exist in board");
無効
契約チェックは生成コードから除外。パフォーマンスが重要で、必要な証明責務がZ3で証明済みの場合のみ使用。
"Generate code without runtime checks"
ランタイムチェックを無効化すると最後の防衛線を失います。すべての証明責務がZ3で証明された後のみ実施してください。
契約エラータイプ
契約がランタイムで違反されると、生成コードはカテゴリと具体的ルールを識別する型付きエラーをスロー。
| チェック関数 | VDM-SL由来 | 発火時期 |
|---|---|---|
checkPre() | pre句 | 操作実行前 — 呼び出し側が無効な入力を送信 |
checkPost() | post句 | 操作完了後 — 実装にバグがある |
checkInv() | inv句 | レコード構築時 — データが型制約に違反 |
checkStateInvariant() | ステート不変条件 | 状態変更後 — グローバル不変条件が破壊される |
VDMJ設定
VDMJはJavaベースのVDMツールチェーン。構文チェック、型チェック、証明責務生成に使用。verify-spec、smt-verify、integrated-workflowスキルに必須。
インストール手順
1. Java 11以上をインストール（java -versionで確認）。
2. Maven Centralから単体JAR（vdmj-4.7.0.jar）を、またはnickbattle/vdmj GitHubリリースからvdmj-suite-*-distribution.zip（vdmj.sh同梱）をダウンロード。
3. デフォルト位置にJARを配置:
mkdir -p ~/.vdmj cp vdmj-*.jar ~/.vdmj/vdmj.jar
4. インストールを検証:
java -jar ~/.vdmj/vdmj.jar -help
プラグインで使用されるVDMJコマンド
| コマンド | 目的 |
|---|---|
java -jar vdmj.jar -vdmsl file.vdmsl | 構文と型チェック |
java -jar vdmj.jar -vdmsl -p file.vdmsl | 証明責務を生成 |
java -jar vdmj.jar -vdmsl -i file.vdmsl | 対話式インタープリタ（テスト用） |
Z3統合
Z3はVDMJで生成された証明責務を自動証明するSMTソルバー。オプション — プラグインなしで動作しますが、smt-verifyスキルには必須。
インストール
pip install z3-solver
または、Z3Prover/z3 GitHubリリースページからZ3バイナリを直接インストールしてz3をPATHに追加。
SMT-LIB出力形式
プラグインはVDM-SL証明責務をSMT-LIB 2.6形式に変換。各POは.smt2ファイルになり、Z3が独立してチェック可能。検証戦略は反論ベース:
; 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
テストランナー設定
generate-testsスキル（v2.0.0新機能）はVDM-SL仕様とPhase 2設計文書（PROTOCOL.md、API-SIGNATURES.md）からVitest/Jest用の契約テストを生成します。Node.jsをインストールし、プロジェクトにテストランナーを追加してください:
npm install -D vitest # or: npm install -D jest
VDM-SL型マッピング
コード生成器はVDM-SL型をTypeScriptとPython等価物にマッピング。以下の表はgenerate-codeスキルで使用されるマッピングを示す。
| VDM-SL型 | TypeScript | Python | 注記 |
|---|---|---|---|
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 |
環境変数
プラグインに環境変数はありません。各スキルは単体VDMJ JARを ~/.vdmj/vdmj.jar に（または配布版ZIPのvdmj.shをPATH上に）、z3バイナリをPATH上に想定します。
プラグインファイル構造
プラグインはClaude Code環境に以下の構造をインストール。各スキルは独立し、独自のSKILL.mdとオプション参照ファイルを持つ。
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