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-codex-plugin/proof-drivennpx skills add OutlineDriven/odin-codex-plugin --skill proof-drivengit clone --depth 1 https://github.com/OutlineDriven/odin-codex-pluginWhat 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 2d 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.
- 2d 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 (15 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. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other skills, from other repositories
apm-review-panel
Use this skill to run a multi-persona expert advisory review on a labelled pull request in microsoft/apm. The panel fans out to five mandatory specialists plus a test-coverage specialist (active on every PR that touches src/) plus three conditional specialists (auth, doc-writer, performance-expert), all running in…
batch-bug-shepherd
Use this skill to drive a batch of suspected bugs in microsoft/apm from raw issue list to mergeable PR queue. Fan out one triage subagent per issue (LEGIT / UNCLEAR / FIXED-AT-HEAD), gate every legit bug against PRINCIPLES.md via an apm-ceo strategic-alignment pass, cross-reference legit issues against open PRs, then…
apm-issue-autopilot
Use this skill to drive any open microsoft/apm issue (bug, feature, docs, refactor, perf) from raw intake to a mergeable PR with triage as the central, paramount gate. Run the apm-triage-panel rubric per issue first, then present ONE consolidated triage review for the whole batch and escalate to the maintainer BY…
apm-spec-guardian
Use this skill to run a four-panel adversarial advisory review on any pull request that touches the OpenAPM specification artifact (docs/src/content/docs/specs/openapm-.md), its inline / sidecar JSON Schemas (docs/src/content/docs/specs/schemas/.schema.json), or the conformance fixture seed…
apm-triage-panel
Use this skill to triage one microsoft/apm issue selected by the daily sweep, the status/needs-triage fast path, or manual dispatch. Emit one synthesized comment with a decision, label set, exact milestone, and suggested next action.
cli-logging-ux
Use this skill when editing or creating CLI output, logging, warnings, error messages, progress indicators, or diagnostic summaries in the APM codebase. Activate whenever code touches console helpers (richsuccess, richwarning, richerror, richinfo, richecho), DiagnosticCollector, STATUSSYMBOLS, CommandLogger, or any…