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-claude-plugin --skill deductive-verification-with-dafny-and-why3git clone --depth 1 https://github.com/OutlineDriven/odin-claude-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-claude-plugin/deductive-verification-with-dafny-and-why3)<a href="https://agentmods.dev/skills/outlinedriven/odin-claude-plugin/deductive-verification-with-dafny-and-why3"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/deductive-verification-with-dafny-and-why3/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-claude-plugin/deductive-verification-with-dafny-and-why3"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/deductive-verification-with-dafny-and-why3.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.00048 | $0.01213 |
| Opus 5 | $0.00024 | $0.00607 |
| Sonnet 5 | $0.00010 | $0.00243 |
| Haiku 4.5 | $0.00005 | $0.00121 |
Grade A, and why
deductive-verification-with-dafny-and-why3 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 deductive-verification-with-dafny-and-why3 — 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 — 40 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Deductive verification with Dafny and Why3
Contract
| Field | Bound contract |
|---|---|
| Trigger | The task is to prove the pre-conditions, post-conditions, and loop invariants of imperative code with an SMT-backed prover: Dafny for annotate-then-verify on executable code, Why3 for multi-prover goals over WhyML. Methodology stays with proof-driven. |
| Authority | Reversible local: writes only Dafny and WhyML source files, prover configuration, and session files under the project; rollback is version control. No remote mutation. |
| Side effect | Local writes to annotated sources, the Why3 user configuration, and .why3session.xml proof sessions. No remote mutation. |
| Done | The module verifies with no unproved obligations: dafny verify reports zero errors, or every Why3 goal is Valid and why3 replay re-confirms the session. |
Inputs
- Code to verify: Dafny sources (
.dfy) or WhyML sources (.mlw), new or existing. - The property set: pre-conditions, post-conditions, loop invariants, and termination measures.
- Dafny 4.11 (current release 4.11.0, 2026-08-25), installed per dafny.org with
dotnet tool install --global dafny, Homebrew, or the binary archive; the release bundles its own Z3. Reference: DafnyRef at dafny.org. - Why3 1.8.2, installed with
opam install why3(addwhy3-idefor the GUI), with at least one prover detected. Manual at why3.org/doc. - Pipeline fact: Dafny verification lowers to Boogie, which encodes to Z3.
Procedure
- Install and detect provers. Install Dafny or Why3, then confirm a solver exists. Dafny carries a bundled Z3, so its CLI runs directly. Why3 needs
why3 config detectto find provers (Alt-Ergo, CVC4, CVC5, Z3) and record them in the user configuration. Done when:dafny verifyruns on a trivial file, orwhy3 config detectlists at least one prover. - Write the contracts first. State
requiresandensureson every method or function,modifieswhere a method touches the heap, and adecreasesmeasure on recursion. Give everywhileloop aninvariantset, because Dafny verifies loops through their specifications. In WhyML, writerequires,ensures, and avarianttermination measure on eachlet rec. Done when: every property is in the source and the first verification run names unproved goals instead of failing on structure. - Clear failures one obligation at a time. Read the error span, state the missing intermediate fact as an
assert, and re-verify. Strengthen a loop invariant before touching the post-condition. Acalcchain decomposes an arithmetic gap in Dafny. Cap noisy output with--verification-error-limit:<n>(default 5; 0 reports all). Done when: the targeted obligation passes and no new obligation appeared. - Drive Why3 goals across provers. Run
why3 prove file.mlwfor a batch summary of Valid, Unknown, or Timeout per goal. Openwhy3 ide file.mlwto run one goal under alternate provers and apply transformations such as split. Save the session, then re-check it in batch withwhy3 replay <project-directory>, which reruns every proof stored in the directory'swhy3session.xml. Done when: every goal is Valid under a prover recorded in the session andwhy3 replayconfirms it. - Gate the result. Delivered code has zero verification errors and no weakened contract: never drop a
requiresorensuresto make a goal pass, and make an inferred loop invariant explicit when the proof depends on it. Rundafny runfor an executable check, ordafny translate cs|java|go|py(js also exists; cpp has limited support) when a build target is set. Done when: verification is clean, the executable check or translation target succeeds, and the contracts in the diff match the stated properties.
What ships with it
1 file 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 · 40 lines · 48 tokens per session scan A d566e53910ed
deductive-verification-with-dafny-and-why3 is a skill published in the GitHub repository OutlineDriven/odin-claude-plugin (35 stars, last pushed 2d ago), licensed Apache-2.0. It adds 48 tokens to every session and 1,213 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 deductive-verification-with-dafny-and-why3, differing in 0 lines, and is treated as a copy.
Other skills, from other repositories
systematic-debugging
Use when encountering any bug, test failure, or unexpected behavior, before proposing fixes.
local-ai-agents
Build local-first AI agents that run entirely on a developer workstation with Microsoft Foundry Local and Qwen function-calling models. Covers Small Language Models (SLMs), the OpenAI-compatible local endpoint, sandboxed local tools, local RAG with Chroma, local MCP servers, hybrid cloud/local routing, and the…
next-cache-components-adoption
Turn on Cache Components in a Next.js app and resolve the blocking routes it surfaces. Use when the user wants to enable, adopt, or migrate to Cache Components, flip the cacheComponents flag, work through a flood of blocking-prerender / instant validation errors, run the cache-components-instant-false codemod, or…
insight-error-page
Write or audit an insight-kind error page for the Next.js dev overlay. Use when creating a new errors/ .mdx page, auditing an existing one, or checking that a page matches the framework fix cards. Covers page structure, title alignment, FixCard cards with Copy prompt button, code snippets, terminology verification…
next-cache-components-optimizer
Drive a Next.js route to instant navigation by setting up an agentic loop, under Cache Components / PPR, on initial load (hard navigation) and client-side navigation (soft navigation). Encode the goal as a failing @next/playwright instant() e2e and work it to green, one verified route at a time; the shipped test then…
next-partial-prefetching-adoption
Turn on Partial Prefetching in a Next.js app and work through the insights it surfaces. Use when the user wants to enable or adopt Partial Prefetching, flip the partialPrefetching flag, opt routes in with export const prefetch = 'partial', audit Link prefetch={true} behavior, preserve existing prefetched UI with…