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 OutlineDriven/odin-codex-plugin --skill proof-drivengit clone --depth 1 https://github.com/OutlineDriven/odin-codex-pluginWrote 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-codex-plugin/proof-driven)<a href="https://agentmods.dev/skills/outlinedriven/odin-codex-plugin/proof-driven"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-codex-plugin/proof-driven/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/outlinedriven/odin-codex-plugin/proof-driven"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-codex-plugin/proof-driven.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.00033 | $0.01616 |
| Opus 5.5 | $0.00013 | $0.00646 |
| Sonnet 5.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 1mo 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.
Copies of this mod
1 near-identical copy found in the catalogue:
- proof-driven — 100% identical, 0 lines differ
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.
- 1mo ago First seen · 150 lines · 33 tokens per session scan A 0dd3b85b8b6c
proof-driven is a skill published in the GitHub repository OutlineDriven/odin-codex-plugin (14 stars, last pushed 3mo ago), licensed Apache-2.0. It adds 33 tokens to every session and 1,616 once invoked, about $0.0001 per session on Opus 5.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-30.
Other skills, from other repositories
type-driven
Type-driven development. Use when developing with refined types, state machines encoded in types, or proof-carrying types; enforces totality and exhaustive pattern matching.
proof-driven
Proof-driven development. Use when implementing with formal verification using property-based testing, theorem proving, or proof tactics; zero unproven property policy enforced.
validation-first
Validation-first development. Use when developing with formal state machine specifications, invariants, and temporal properties before writing implementation code.
triage-issue
Investigate a reported bug to root cause, then emit a TDD-shaped fix plan as an issue artifact. Trigger when the user reports a bug, says "triage", asks for issue investigation, or wants a fix plan before code changes.
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.
tests-adversarial
Write adversarial tests that intentionally stress failure paths. Use when hardening error handling, stress-testing assumptions, validating boundary behavior, or hunting silent failures.