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/outline-driven-development --skill deductive-verification-with-dafny-and-why3git clone --depth 1 https://github.com/OutlineDriven/outline-driven-developmentWrote 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/outline-driven-development/deductive-verification-with-dafny-and-why3)<a href="https://agentmods.dev/skills/outlinedriven/outline-driven-development/deductive-verification-with-dafny-and-why3"><img src="https://agentmods.dev/badge/skills/outlinedriven/outline-driven-development/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/outline-driven-development/deductive-verification-with-dafny-and-why3"><img src="https://agentmods.dev/badge/skills/outlinedriven/outline-driven-development/deductive-verification-with-dafny-and-why3.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector pass
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 4d 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:
- deductive-verification-with-dafny-and-why3 — 100% identical, 0 lines differ
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.
- 4d 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/outline-driven-development (52 stars, last pushed 4d 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. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-09-06.
Other skills, from other repositories
typescript-test-writing
Use this skill when writing or modifying tests in the llxprt-code repository. Covers mandatory TDD, behavioral testing, bun:test conventions and file naming, mock hygiene (no mock theater), and what never to test. Distilled from dev-docs/RULES.md, which remains the source of truth.
python-testing
A Python testing guide covering pytest, test coverage, and test-driven development (TDD), a method of writing a failing test before the code that makes it pass.
ts-library
Use when authoring TypeScript libraries or npm packages - covers project setup, package.json exports, build tooling (tsdown/unbuild), API design patterns, type inference tricks, testing, and publishing to npm. Use when bundling, configuring dual CJS/ESM output, or setting up release workflows.
nested-fixture-pattern
This skill should be used when working on Java projects with JUnit tests that have layered preconditions, expensive shared setup (servers, databases, provisioned users), or complex scenario trees. Trigger phrases include "nested fixture", "fixture pattern", "scenario tree", "layered test setup", or when the user is…
rust-development
CIEL's framework for idiomatic Rust, zero-cost abstractions, and robust error handling.
skillshare-implement-feature
Implement a feature from a spec file or description using TDD workflow. Use this skill whenever the user asks to: add a new CLI command, implement a feature from a spec, build new functionality, add a flag, create a new internal package, or write Go code for skillshare. This skill enforces test-first development…