---
name: hashintel-dafny-verification
description: "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."
license: "NOASSERTION"
metadata:
  decimalai-skill-id: "fdd5744f-de7f-4964-a647-022678bfb1ce"
  decimalai-version-id: "f9c9e6f4-391d-4ad4-a69c-5c4dd8bcffb7"
  decimalai-version: "2"
  decimalai-body-sha256: "c949ace05929a81cdb11c93dc17cfd94c973dcce3766775c84c14e10e6aa2415"
  decimalai-name: "hashintel/dafny-verification"
  decimalai-format: "1"
  decimalai-invocation: "model"
  decimalai-source: "https://app.decimal.ai/s/hashintel-dafny-verification@2/SKILL.md"
---
# Stub: capability-aware verification lifecycle

Aligned to core as of `223d721`.

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.