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 smt-verifygit 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/smt-verify)<a href="https://agentmods.dev/skills/kotaroyamame/formal-agent-contracts/smt-verify"><img src="https://agentmods.dev/badge/skills/kotaroyamame/formal-agent-contracts/smt-verify/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/smt-verify"><img src="https://agentmods.dev/badge/skills/kotaroyamame/formal-agent-contracts/smt-verify.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.00118 | $0.02094 |
| Opus 5 | $0.00059 | $0.01047 |
| Sonnet 5 | $0.00024 | $0.00419 |
| Haiku 4.5 | $0.00012 | $0.00209 |
Grade A, and why
smt-verify 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 11d 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 — 206 lines — stays where its author put it; the contents beside it link to each section on GitHub.
PO → SMT-LIB Conversion and Z3 Verification
Convert proof obligations (POs) generated by VDMJ into SMT-LIB format and verify them with Z3.
VDMJが生成した証明責務（PO）をSMT-LIB形式に変換し、Z3で自動検証する。
Prerequisites
Z3 Installation Check
which z3 || pip install z3-solver --break-system-packages
If Z3 is not available, guide the user through installation.
Z3がない場合はユーザーにインストールを案内する。
VDMJ Setup
Locate the VDMJ JAR using the same method as the verify-spec skill.
verify-specスキルと同じ方法でVDMJ JARを特定する。
Verification Flow
Step 1: PO Generation
Generate POs using the verify-spec procedure. Skip if PO output already exists.
verify-specの手順でPOを生成する。すでにPO出力がある場合はスキップ。
java -jar <VDMJ_JAR> -vdmsl <files...> -p 2>&1
Step 2: Convert Each PO to SMT-LIB
For each generated PO, perform the following conversion steps.
各POについて以下の手順で変換する。
2a. Generate Type Declarations
Scan all types appearing in the PO and declare them in SMT-LIB.
Follow conversion rules in references/type-mapping-rules.md.
Key mappings:
nat→Int+(>= x 0)constraintnat1→Int+(>= x 1)constraint- Record types →
declare-datatypes+ constructors/selectors seq1 of char→String+(> (str.len s) 0)constraintmap K to V→ uninterpreted sort +map_apply/map_domfunctionsset of T→(Array T Bool)characteristic function representation
POに出現する全型をSMT-LIBで宣言する。変換ルールは references/type-mapping-rules.md に従う。
2b. Generate Auxiliary Definitions
Define invariants, pre-conditions, and post-conditions referenced by the PO using define-fun:
POが参照する不変条件・事前条件・事後条件を define-fun で定義する:
(define-fun inv_TypeName ((x TypeSort)) Bool ...)
(define-fun pre_funcName ((arg1 Sort1) ...) Bool ...)
Include type constraints (nat/nat1 bounds, seq1 non-empty constraints) in invariant definitions.
2c. Convert the PO Body
Convert PO expressions following references/expression-mapping-rules.md.
PO式を references/expression-mapping-rules.md に従って変換する。
What ships with it
7 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.
- 11d ago First seen · 206 lines · 118 tokens per session scan A 875e9e298bc5
smt-verify is a skill published in the GitHub repository kotaroyamame/formal-agent-contracts (1 stars, last pushed 2mo ago), licensed MIT. It adds 118 tokens to every session and 2,094 once invoked, about $0.0006 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
math-and-combinatorics
Reference patterns for mathematical and combinatorial problem-solving. Covers modular arithmetic, prime sieves, GCD/LCM, binomial coefficients, fast exponentiation, counting techniques, inclusion-exclusion, and game theory. Load this skill when a problem involves number theory, combinatorics, modular operations, or…
claude-code-session-broker
Use when running Arcgentic V2 in Claude Code and fixed Planner, Developer, and Auditor role sessions must be coordinated through a broker.
arcgentic
Use when the user says Arcgentic, asks to use Arcgentic, or wants an idea taken through a complete plan → development → self-audit → external audit workflow in Codex.
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.…
session-mode
Use when a project has not yet stored session mode, when a user asks for complete arcgentic workflow execution, or when role identity handoff prompts are needed.
cross-session-handoff
Read, write, snapshot, and lock .arcgentic/state.yaml across planner, dev, audit, and optional test sessions.