Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add kotaroyamame/formal-agent-contracts --skill generate-db-schemagit clone --depth 1 https://github.com/kotaroyamame/formal-agent-contractsWrote 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-db-schema)<a href="https://agentmods.dev/skills/kotaroyamame/formal-agent-contracts/generate-db-schema"><img src="https://agentmods.dev/badge/skills/kotaroyamame/formal-agent-contracts/generate-db-schema/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-db-schema"><img src="https://agentmods.dev/badge/skills/kotaroyamame/formal-agent-contracts/generate-db-schema.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.00221 | $0.03721 |
| Opus 5 | $0.00111 | $0.01861 |
| Sonnet 5 | $0.00044 | $0.00744 |
| Haiku 4.5 | $0.00022 | $0.00372 |
Grade A, and why
generate-db-schema 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 10d 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 — 202 lines — stays where its author put it; the contents beside it link to each section on GitHub.
DBスキーマ導出スキル (v2.1.0)
確定した VDM-SL 仕様（型定義・不変条件・状態定義・操作）から、データベーススキーマ（DDL）を規則的に導出するスキルです。設計判断を LLM の自由作文に任せるのではなく、番号付きの写像規則（R1〜R18、references/vdm-to-sql-mapping.md）を適用し、規則で写せない箇所は乖離（deviation）として明示的に記録します。
設計原理
このスキルは形式手法の**データ具体化（data reification）**の考え方に基づきます：
- 導出できるものは機械的に導出する — 抽象型→具体表現の対応は規則で決まる。LLM が「それらしいスキーマを推測」してはならない
- 写せないものは隠さず記録する —
nat（無限）→BIGINT（有限）のような忠実でない写像は retrenchment（譲歩）として DEVIATIONS.md に残し、その箇所にランタイム契約チェックとテストを集中させる - すべての不変条件に担保箇所を与える — 各
invは「DB制約 / アプリ層チェック / 契約テスト」のいずれかで守られ、その対応を TRACEABILITY.md が示す。担保箇所のない不変条件が残ったら導出は未完成
成果物
| ファイル | 内容 |
|---|---|
db/schema.sql |
DDL（テーブル、型、CHECK/UNIQUE/FK 制約、トリガー、コメント） |
db/DEVIATIONS.md |
retrenchment 表：仕様と DB 表現の乖離と、その補償手段 |
db/TRACEABILITY.md |
不変条件・契約 → 担保箇所（DB制約名 / アプリ層 / テスト）の対照表 |
ステップ1：入力の解析
目的：VDM-SL 仕様から永続化対象を特定する
ユーザーに確認する情報：
- 仕様ファイル：対象の
.vdmslファイル（複数可） - 永続化スコープ：state 定義の全コンポーネントを永続化するか、一部か
（例：
board : TaskBoardは永続化、セッション的な一時状態は対象外） - 既存スキーマ：ゼロから作るか、既存 DB への追加か（追加ならマイグレーション形式で出力）
仕様から抽出する要素：
✓ 型定義: record型、quote型（列挙）、基本型の別名、合成型（map/set/seq/optional）
✓ 型不変条件: inv 節（値域、長さ、形式）
✓ state 定義: コンポーネント、状態不変条件、init
✓ 操作: atomic ブロック（トランザクション境界の候補）、事前・事後条件
ステップ2：対象 DB と規約の確認
目的：方言と命名規約を固定する
- DBMS：PostgreSQL（デフォルト・最も表現力が高い）/ MySQL / SQLite。
方言差は
references/vdm-to-sql-mapping.mdの各規則に併記 - 命名規約：デフォルトは snake_case、テーブル名は複数形（
Task→tasks）。 VDM 名との対応は schema.sql のコメントに必ず残す - 予約語回避：
desc→description等。変換は TRACEABILITY.md に記録
ステップ3：写像規則の適用
目的：references/vdm-to-sql-mapping.md の規則 R1〜R18 を順に適用する
主要規則の概要（詳細・方言差は参照文書）：
| 規則 | VDM-SL | DB 表現 |
|---|---|---|
| R1 | record 型 | テーブル（1フィールド=1カラム） |
| R2 | state の map K to V |
V のテーブルに K を主キーとして埋め込む |
| R3 | quote 型の合併 <A>|<B> |
ENUM 型（PostgreSQL）/ VARCHAR + CHECK IN |
| R4 | nat / nat1 / int / bool |
BIGINT + CHECK / BOOLEAN ※整数は乖離 D-NUM |
| R5 | seq of char / seq1 of char |
TEXT / TEXT + CHECK (length > 0)。inv に長さ上限があれば VARCHAR(n) |
| R6 | optional [T] |
NULL 許容カラム |
| R7 | 単一値の型不変条件 | CHECK 制約 |
| R8 | map のキー一意性 | 主キー（構造として自動的に成立） |
| R9 | inv board(id).id = id 型（キー=フィールド） |
構造的に成立（フィールドを主キーに昇格）※記録のみ |
| R10 | エンティティ間参照の不変条件 | FOREIGN KEY |
| R11 | forall の一意性主張 |
UNIQUE 制約 / 部分インデックス |
| R12 | 状態遷移規則（ValidTransition 等） |
UPDATE トリガー（OLD/NEW 比較）またはアプリ層 ※乖離 D-TRANS |
| R13 | 複数コンポーネントにまたがる状態不変条件 | トリガー / 遅延制約 / アプリ層 ※乖離 D-CROSS |
| R14 | set of T / seq of T（char 以外） |
結合テーブル（順序が要る seq は position カラム付き） |
| R15 | atomic ブロック・複数代入の操作 |
トランザクション境界（BEGIN/COMMIT）としてコメントに明記 |
| R16 | real |
DOUBLE PRECISION ※乖離 D-FLOAT。金額なら NUMERIC を対話で確認 |
| R17 | state の単一値コンポーネント（nextId 等） |
シングルトン状態テーブル、または連番なら SEQUENCE/IDENTITY への置換を対話で確認 ※乖離 D-SEQ |
| R18 | token / 合成キー |
サロゲートキー + UNIQUE、対話で確認 |
What ships with it
2 files 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.
- 10d ago First seen · 202 lines · 221 tokens per session scan A c7b047a0ba2d
generate-db-schema is a skill published in the GitHub repository kotaroyamame/formal-agent-contracts (1 stars, last pushed 2mo ago), licensed MIT. It adds 221 tokens to every session and 3,721 once invoked, about $0.0011 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
db-audit
Database performance and safety audit. 70+ checks across 13 dimensions (DB1-DB13): query patterns, indexes, schema design, connections, transactions, migrations, caching, query optimization, ORM anti-patterns, observability, data lifecycle, DB security, and migration deployment safety. Code-level checks for all ORMs.…
performance-audit
Full-stack performance health check across 12 dimensions. Rendering, bundles, assets, API/network, algorithms, memory, database, caching, Web Vitals, backend runtime, concurrency, and framework-specific pathologies. Evidence-based Impact Models with confidence tiers and a prioritized optimization roadmap. Switches…
mako-database
TRIGGER when: user asks about database schema, RLS policies, foreign keys, stored procedures, or table DDL directly. Covers dbping, dbcolumns, dbfk, dbrls, dbrpc, dbtableschema.
caching
HybridCache (.NET 9+), output caching, cache-aside pattern, and IMemoryCache — registration, usage, invalidation, and key strategy.
mako-neighborhoods
TRIGGER when: user wants entity-wide context for a table, route, or RPC -- schema + RLS + readers + writers + downstream touches all at once. Covers tableneighborhood, routecontext, rpcneighborhood.
ef-core-patterns
EF Core best practices reference — safe migrations, query optimization, configuration patterns, and common pitfalls.