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 agentmods add skills/outlinedriven/odin-gemini-cli-extension/proof-drivennpx skills add OutlineDriven/odin-gemini-cli-extension --skill proof-drivengit clone --depth 1 https://github.com/OutlineDriven/odin-gemini-cli-extensionWrote 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/outlinedriven/odin-gemini-cli-extension/proof-driven)<a href="https://agentmods.dev/skills/outlinedriven/odin-gemini-cli-extension/proof-driven"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-gemini-cli-extension/proof-driven.svg" alt="Measured on agentmods" 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 | $0.00033 | $0.01616 |
| Opus 5 | $0.00016 | $0.00808 |
| Sonnet 5 | $0.00007 | $0.00323 |
| Haiku 4.5 | $0.00003 | $0.00162 |
Grade A, and why
proof-driven 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 5d 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.
This is a copy
100% identical to proof-driven — 0 lines differ, which has more behind it and is treated as the original. This page carries a canonical link to it rather than competing with it.
How it starts
The opening of the file, as written. The whole thing — 150 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Proof-driven development
Prove properties from requirements before writing code. Proofs guide implementation, not the reverse. Zero unproven properties in final code.
Modern insight (2025): PBT + example tests pairing is the standard -- properties discover edge cases, example tests prevent regressions and serve as documentation. Counterexamples from shrinking should always become permanent regression tests. AI-assisted PBT (Anthropic 2025) can generate properties from docstrings, but human judgment for property selection remains essential.
See frameworks for language-specific PBT and stateful testing tools. See examples for brief property test patterns per language. See formal-tools for theorem provers and bounded model checkers.
Property Categories
| Category | Description | Example |
|---|---|---|
| Postcondition | Output satisfies contract | sorted(sort(xs)) |
| Invariant | Property preserved by operation | len(xs) == len(sort(xs)) |
| Idempotence | f(f(x)) == f(x) |
deduplicate(deduplicate(xs)) |
| Inverse / Round-trip | g(f(x)) == x |
decode(encode(x)) == x |
| Model-based | Implementation matches reference | my_sort(xs) == stdlib_sort(xs) |
| Commutativity | Order doesn't matter | a + b == b + a |
| Metamorphic | Relationship between outputs | sin(-x) == -sin(x) |
Most effective (OOPSLA 2025): Model-based properties (~80% bug detection), postconditions (~65%). Least effective: properties that reimplement the logic under test.
Anti-pattern: Don't reimplement the function in the property. Properties should be simpler than the code they test.
When to Apply
- Critical algorithms (sort, search, crypto, compression)
- Financial calculations (rounding, currency conversion)
- Consensus/distributed protocols (invariants across nodes)
- Safety-critical systems (medical, automotive, aerospace)
- Data structure invariants (balanced tree, heap property)
- Serialization round-trip (encode/decode fidelity)
- Stateful systems (databases, queues, caches) -- via stateful PBT
What ships with it
3 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.
- 5d ago First seen · 150 lines · 33 tokens per session scan A 0dd3b85b8b6c
proof-driven is a skill published in the GitHub repository OutlineDriven/odin-gemini-cli-extension (5 stars, last pushed 1mo ago), licensed Apache-2.0. It adds 33 tokens to every session and 1,616 once invoked, about $0.0002 per session on Opus 5. A static security scan graded it A with 0 findings. It is 100% identical to proof-driven, differing in 0 lines, and is treated as a copy.
Other skills, from other repositories
tests-purge-unneeded
Delete tests that don't catch real bugs — the inverse of TDD. Use when reviewing legacy test suites, slow CI investigations, refactor-driven test sweeps, or evaluating whether a test the type system already covers should stay. Thesis — a test exists only if removing it would let a real bug reach production.
test-driven
Test-Driven Development (TDD) across any supported language. Use when implementing features or fixes with TDD methodology, writing tests before code, or following XP-style development.
askme
Verbalized Sampling (VS) protocol for intent exploration before planning, mode-aware. Default exhaustive runs full VS; collaborative runs tip-sharing dialogue; adversarial walks the design tree one fork at a time. Auto-detects from phrasing ("help me refine" → collaborative, "poke holes" → adversarial); override via…
design
Set visual and interaction direction for any UI surface (web, React, TUI, CLI, desktop, Qt, design-system tokens) before any UI code. Direction-first: generates 3-4 distinct directions via verbalized sampling, picks one via per-axis single-select, then derives palette, typography, spacing, motion budget. Loads when…
git-branchless
Enforce idiomatic git-branchless during planning and executing tasks — detached-HEAD-first work, in-memory rebase via git move, event-log recovery via git undo, deferred branch creation, speculative-merge git sync for base updates. Use when planning or executing multi-commit work, history rewrites, stack edits…
grill-ai-mastery
Hybrid interview that probes AI-engineering mastery by tip-vocabulary depth — entity referencing, loop closure, observability, harness improvement — not by token usage or LOC. Start collaborative (two-way tip exchange), escalate to adversarial probing when depth is lacking. Trigger when the user says "interview me on…