# Dafny Verification

> Stub. Elicit software correctness obligations, maintain a recoverable correctness workpiece, and author or review Dafny specifications with an honest account of what was stated, assumed, discharged, skipped, or trusted. Use for a correctness interview or a Dafny specification or proof review.

- Skill: `hashintel/dafny-verification` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add hashintel/dafny-verification`
- Raw SKILL.md: https://api.skillmd.com/api/skills/hashintel/dafny-verification/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: hashintel (https://skillmd.com/u/hashintel)
- Updated: 2026-09-22
- Page: https://skillmd.com/skills/hashintel/dafny-verification

---


# Stub: capability-aware verification lifecycle

This skill is a placeholder home. It records the proposed disclosure shape from the accepted Ampcode pressure test and authors no procedure yet.

Proposed shape, not yet earned:

```text
dafny-verification
├─ elicitation and workpiece maintenance
│  ├─ activate `elicitation`
│  ├─ references/software-correctness-elicitation.md
│  └─ templates/workpiece.md          when recording or revising
└─ formalization and evidence
   ├─ references/dafny-specification.md
   └─ references/proof-checks.md
```

Whether specification and verification are one job skill or two (`dafny-specification`, `dafny-verification`) is an open cardinality question that this stub does not settle.