菜单
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.
默认使用会先检查来源的 Prompt；你也可以切换为直接命令，或下载本地副本。
决定是否安装前，请先阅读 SKILL.md，以及 SkillsMP 当前展示的配套文件。
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
直接命令不会经过审查 Prompt；运行前请先检查来源。
npx skills add https://github.com/hashintel/hash --skill dafny-verification命令会保持在同一行。复制前请横向滚动并检查完整内容。
想先保存到本地？可下载 SkillsMP 当前能够提供的文件。
正在显示 SKILL.md
| name | 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. |
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:
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.
Acquire and improve an epistemically responsible source-side account through conversation and consulted material. Use before substantive interviewing, source consultation, consequential correction or conflict resolution, and when recording workpiece evidence.
Elicit or transcribe a target claim and the definitions and supporting claims its justification rests on, maintain a recoverable claims workpiece, prepare statement cards for an external claims ledger, and explain what the ledger's standing does and does not establish. Use for a claim-formalization interview, a mission or milestone proposal, a card faithfulness review, or a question about what is established.
Elicit or revise software behavior, maintain a recoverable behavior workpiece, and author or review honest Gherkin feature documents. Use for a behavior-specification interview, Gherkin document, executable-specification draft, or review of any of them.