Getting it into your agent
It runs from inside its repository, so the clone comes first — what it calls does not travel with the file alone.
git clone --depth 1 https://github.com/kotaroyamame/formal-agent-contractsnpx agentmods add skills/kotaroyamame/formal-agent-contracts/generate-testsWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/kotaroyamame/formal-agent-contracts/generate-tests)<a href="https://agentmods.dev/skills/kotaroyamame/formal-agent-contracts/generate-tests"><img src="https://agentmods.dev/badge/skills/kotaroyamame/formal-agent-contracts/generate-tests/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/kotaroyamame/formal-agent-contracts/generate-tests"><img src="https://agentmods.dev/badge/skills/kotaroyamame/formal-agent-contracts/generate-tests.svg" alt="Reviewed on agentmods" width="80" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00186 | $0.08457 |
| Opus 5 | $0.00093 | $0.04228 |
| Sonnet 5 | $0.00037 | $0.01691 |
| Haiku 4.5 | $0.00019 | $0.00846 |
Grade A, and why
generate-tests scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 12d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 854 lines — stays where its author put it; the contents beside it link to each section on GitHub.
契約テスト自動生成スキル (v2.1.0)
VDM-SL形式仕様および設計文書から自動的にユニットテストコードを生成するスキルです。VDM-SL仕様に記述された型不変式、前提条件、後提条件と、設計文書(PROTOCOL.md、API-SIGNATURES.md)に記述されたプロトコル規則をテストコードに変換し、実装の正確性を検証します。
背景:VDM-SL仕様と設計文書の役割分担
エージェント開発は2つのフェーズで契約を定義します:
| フェーズ | 役割 | 成果物 | このスキルでの使用 |
|---|---|---|---|
| Phase 1:ドメイン設計 | 各エージェント内部のロジックを形式化 | VDM-SL仕様ファイル | 型不変式、前後提条件テスト生成 |
| Phase 2:インターフェース設計 | エージェント間通信を定義 | PROTOCOL.md、API-SIGNATURES.md | プロトコルテスト生成 |
実装時に発生する可能性のある問題と検出方法
| 問題カテゴリ | 例 | 検出方法 |
|---|---|---|
| 実装バグ(ドメイン層) | 後提条件のロジック誤り | ✓ VDM-SLテストで検出 |
| 言語固有の問題 | JavaScriptの型強制、nullの扱い | ✓ VDM-SLテストで検出 |
| プロトコル層バグ | メッセージ型とペイロードの不整合 | ✓ 設計文書テストで検出 |
| エッジケース | 境界値での動作未定義 | ✓ VDM-SLテストで検出 |
| 並行処理の問題 | レースコンディション(複数エージェント) | 統合テストで検出 |
このスキルは以下の2つのソースから自動テスト生成します:
VDM-SL仕様から生成:
- 型不変式テスト:型の制約が常に満たされるか
- 前提条件テスト:関数が前提条件を期待通り検証するか
- 後提条件テスト:関数が後提条件を満たす結果を返すか
- 境界値テスト:エッジケースでの動作
設計文書(PROTOCOL.md)から生成: 5. プロトコルテスト(新v2.0.0):メッセージの型安全性、状態遷移の正確性、API署名の一貫性
ステップ1:VDM-SLファイルと設計文書の解析
目的:VDM-SLファイルと設計文書から型、関数、契約、プロトコル仕様を抽出
ユーザーに以下の情報を提供してもらいます:
- VDM-SLファイル:解析対象のファイルパス
- 設計文書:PROTOCOL.md、API-SIGNATURES.md(プロトコルテスト対象)
- テスト対象関数:全関数 / 特定関数のみ
- テスト対象言語:JavaScript / TypeScript / その他
- テストフレームワーク:Vitest(推奨) / Jest / Mocha
スキルの処理:
ステップ1a: VDM-SLファイルの構文解析
✓ モジュール構造を抽出
✓ 型定義を解析
✓ 関数シグネチャを抽出
ステップ1b: 契約情報の抽出
✓ 前提条件(pre)を読み込み
✓ 後提条件(post)を読み込み
✓ 不変式(inv)を収集
ステップ1c: メタデータの生成
✓ 関数の入出力型を記録
✓ テスト生成戦略を決定
✓ テストケース数を見積もり
出力例:
[解析結果サマリー]
ファイル: HybridJudgeAgent.vdmsl
検出された型: 6個
- Score (nat1, inv: 1<=s<=100)
- Threshold (nat1, inv: 1<=t<=100)
- Action (Quote型)
- Ticket (Record型)
- ...
検出された関数: 3個
- decide(Ticket, Score, Score) -> Action
- scoreAll(seq of Score) -> seq of Score
- explain_decision(...) -> seq of char
推定テストケース数: 25-35個
ステップ1.5:モデルルーティングの確認(任意・トークン削減)
仕様ファイルの隣に model-routing.json(route-models スキルの成果物)が存在する場合:
What ships with it
1 file beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 12d ago First seen · 854 lines · 186 tokens per session scan A ed6057dae309
generate-tests is a skill published in the GitHub repository kotaroyamame/formal-agent-contracts (1 stars, last pushed 2mo ago), licensed MIT. It adds 186 tokens to every session and 8,457 once invoked, about $0.0009 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-31.
Other skills, from other repositories
verify-gates
Runs the mechanical quality gates that the arcgentic state machine requires for state transitions. Invoked indirectly by transition.sh OR directly by orchestrator agent before declaring a state transition. Use when about to call transition.sh OR when manually verifying that a round artifact meets the gate criteria.…
auto-loop
TDD-based autonomous development loop with checkpoint recovery and observability changelog.
workflow
Run the complete 5-step development workflow: focus problem → prevent over-development → test-first (TDD) → document → smart commit. Use when starting a new feature, or when the user runs /workflow or asks for the full development flow.
test-runner
Test execution reference: framework detection (pytest/jest/vitest/go/cargo/junit) and correct run/coverage commands, plus failure-analysis steps. Use when running tests, analyzing test failures, or verifying coverage after code changes.
test-first
Drive one feature through a strict TDD Red-Green-Refactor cycle with checklists for each phase. Use when implementing new functionality test-first, or when the user runs /test-first.
linked-intent-dev
Guide for linked-intent development (LID). Consult for ALL code changes. Walks changes through a mode-aware six-phase workflow (HLD → LLD → EARS → intent-narrowing edge audit → tests-first → code) with mandatory stops between each phase. Bugs walk the arrow like any other change — no short-circuit. Enforces cascade…