dafny-prove
Run Dafny verification on an rd-flow spec and iterate until proofs discharge.
Skill by KKuze
Chalk Labs
Need help deploying dafny-prove?
Chalk Labs sets up agents like this inside real teams: connected to your tools, tested on your data, with a human in the loop where it matters.
Install
Works with Claude Code, Claude apps, Codex, Cursor, Gemini CLI, GitHub Copilot, VS Code, OpenCode, Goose, Windsurf. Read the repository before you give any tool access to your data.
npx agentmarket install skill/kkuze-dafny-prove
Asks which of your tools to add it to (Claude Code, Codex, Cursor, VS Code, Windsurf, Gemini CLI, Claude Desktop) and shows the change first. See https://agentmart.dev/cli.
Get the weekly diff
The weekly diff: one email a week with new agent tools, notable updates and grade changes, plus security alerts for tools you follow. Double opt-in, one-click unsubscribe.
About
Reviews
Write a reviewNo reviews yet. Installed it? Reviews come from verified installers only. How reviews work
Permissions
What this skill can do and what it asks for, from its SKILL.md. Checked Oct 25, 2026.
- Tools
- No tools found
- Secrets
- None asked for
- Install scripts
- None found
Network hosts it talks to 1
codeload.github.com· found in install command
Files it touches
~/.claude/skills/dafny-prove
What's inside
- Skill name
dafny-prove- Description
- Run Dafny verification on an rd-flow spec and iterate until proofs discharge. Use after `dafny-refine`.
- License
- MIT
- Instructions
- 27 lines in SKILL.md · view on GitHub
Files (1)
- SKILL.md
SKILL.md (first lines)
# dafny-prove
## When to invoke
- Current phase is `dafny-prove` or `dafny-refine` has just declared the
refinement complete.
## Steps
1. Read `.formal/settings/rules/dafny-proof.md`.
2. Run:
```
rd-flow dafny verify <name>
```
3. Read `dafny/proof-report.md`:
- `verified` → advance to `dafny-build` (optional) or skip to
`implement`.
- `skipped` (no tooling) → block and request Dafny install.
- `failed` → add lemmas / strengthen `ensures` / split methods. Avoid
`assume`/`{:axiom}` unless documented in `refinement.md`.
## Handoff
On `verified`, invoke `dafny-build` if you want emitted code for the
implementation, or `implement` directly if hand-translating.From KKuze/rd-flow, MIT.
More from KKuze/rd-flow
- 0.521score
implement
KKuze
Build the implementation plan and code mapping from a verified rd-flow spec.
SkillBFreshness: BClaude Code +9 - 0.518score
validate
KKuze
Close the loop on an rd-flow spec by confirming every requirement maps to verified specs and shipping code.
SkillBFreshness: BClaude Code +9 - 0.474score
discovery
KKuze
Route a new or returning request into the refinement-driven workflow.
SkillCFreshness: CClaude Code +9 - 0.471score
dafny-build
KKuze
Compile a verified Dafny spec to a target language (cs, java, go, js, py, cpp, rs) and capture the emitted artefacts.
SkillCFreshness: CClaude Code +9 - 0.471score
tla-model
KKuze
Author the TLA+ abstract behavioural spec for an rd-flow workspace.
SkillCFreshness: CClaude Code +9 - 0.469score
dafny-refine
KKuze
Refine an rd-flow TLA+ spec into a Dafny module with concrete types and contracts.
SkillCFreshness: CClaude Code +9 - 0.469score
tla-check
KKuze
Run TLC against an rd-flow TLA+ model and triage the result.
SkillCFreshness: CClaude Code +9 - 0.447score
requirements
KKuze
Drive the requirements phase of an rd-flow spec.
SkillCFreshness: CClaude Code +9
Signals
- Stars
- 0
- Forks
- 0
- Open issues
- 1
- Last commit (this folder)
- May 12, 2026 (5 months ago)
From GitHub (fetched Oct 24, 2026).
Details
- License
- MIT
- Repository
- github.com/KKuze/rd-flow
- First seen
- Oct 24, 2026
- Last checked
- Oct 24, 2026
- Source
- GitHubgithub-graphql
More from KKuze
- 0.521score
implement
KKuze
Build the implementation plan and code mapping from a verified rd-flow spec.
SkillBFreshness: BClaude Code +9 - 0.518score
validate
KKuze
Close the loop on an rd-flow spec by confirming every requirement maps to verified specs and shipping code.
SkillBFreshness: BClaude Code +9 - 0.474score
discovery
KKuze
Route a new or returning request into the refinement-driven workflow.
SkillCFreshness: CClaude Code +9 - 0.471score
dafny-build
KKuze
Compile a verified Dafny spec to a target language (cs, java, go, js, py, cpp, rs) and capture the emitted artefacts.
SkillCFreshness: CClaude Code +9 - 0.471score
tla-model
KKuze
Author the TLA+ abstract behavioural spec for an rd-flow workspace.
SkillCFreshness: CClaude Code +9 - 0.469score
dafny-refine
KKuze
Refine an rd-flow TLA+ spec into a Dafny module with concrete types and contracts.
SkillCFreshness: CClaude Code +9
Done for you
Rather not set it up yourself?
Chalk Labs scopes, builds and runs agents for your team: the task audit, the eval harness, the integrations and the weekly ops report. Fixed scope, priced before we start.
See how we build AI agents →Read the case studies
Chalk Labs is a two-founder AI and growth studio. We build AI agents, CRMs and MVPs for Web3 and AI companies, and have shipped 50+ product and token launches.
- launches shipped
- 50+
- launches shipped
- media placements
- 500+
- media placements
- founders on every account
- 2
- founders on every account
Press we've placed: Forbes · CoinDesk · Decrypt · Cointelegraph · The Block
Rahil Jain, Co-founder, Chalk Labs. Ex-Goldman Sachs engineer. You talk to the person who builds it.
Get dafny-prove running in your business
Tell us what you want to automate. A founder replies within one working day with a plan, not a pitch deck.
Cite this page
dafny-prove skill. Agent Mart. https://agentmart.dev/skills/kkuze-dafny-prove (last updated 2026-10-24)