Agent skill

Vero Dafny Pitfalls

Load BEFORE translating any Dafny item to Lean 4 to avoid known Dafny→Lean pitfalls.

Apache-2.0Auto-check: notesWriting & Content

Install Vero Dafny Pitfalls

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a claude-code

Project install by default; add -g for ~/.claude/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-dafny-pitfalls --agent claude-code

Project scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .claude/skills && cp -r skills-src/.claude/skills/vero-dafny-pitfalls .claude/skills/vero-dafny-pitfalls && rm -rf skills-src

Use ~/.claude/skills/ instead of .claude/skills for a personal install. The folder must contain SKILL.md.

Claude Code skills documentation · loads skills from .claude/skills/

Paste into Claude Code

Install the "vero-dafny-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-dafny-pitfalls into .claude/skills/vero-dafny-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-dafny-pitfalls", then confirm the skill loads.

Claude Code copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

$skill-installer

$skill-installer install https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-dafny-pitfalls

Type this inside Codex. $skill-installer <name> installs a curated skill from openai/skills. The installer writes to $CODEX_HOME/skills (default ~/.codex/skills). Restart Codex if the skill does not show up.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a codex

Project install goes to .agents/skills/; add -g for ~/.codex/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-dafny-pitfalls --agent codex

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .agents/skills && cp -r skills-src/.claude/skills/vero-dafny-pitfalls .agents/skills/vero-dafny-pitfalls && rm -rf skills-src

Use ~/.agents/skills/ instead of .agents/skills for a personal install.

Codex skills documentation · loads skills from .agents/skills/

Paste into Codex

Install the "vero-dafny-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-dafny-pitfalls into .agents/skills/vero-dafny-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-dafny-pitfalls", then confirm the skill loads.

Codex copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a cursor

Project install goes to .agents/skills/; add -g for ~/.cursor/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-dafny-pitfalls --agent cursor

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/.claude/skills/vero-dafny-pitfalls .cursor/skills/vero-dafny-pitfalls && rm -rf skills-src

Use ~/.cursor/skills/ instead of .cursor/skills for a personal install.

Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/

Paste into Cursor

Install the "vero-dafny-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-dafny-pitfalls into .cursor/skills/vero-dafny-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-dafny-pitfalls", then confirm the skill loads.

Cursor copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

gemini skills install

$ gemini skills install https://github.com/sunblaze-ucb/vero.git --path .claude/skills/vero-dafny-pitfalls

--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a gemini-cli

Project install goes to .agents/skills/; add -g for ~/.gemini/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-dafny-pitfalls --agent gemini-cli

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/.claude/skills/vero-dafny-pitfalls .gemini/skills/vero-dafny-pitfalls && rm -rf skills-src

Use ~/.gemini/skills/ instead of .gemini/skills for a personal install, then run /skills reload.

Gemini CLI skills documentation · loads skills from .gemini/skills/, .agents/skills/

Paste into Gemini CLI

Install the "vero-dafny-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-dafny-pitfalls into .gemini/skills/vero-dafny-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-dafny-pitfalls", then confirm the skill loads.

Gemini CLI copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-dafny-pitfalls

Installs for Copilot at project scope by default; add --scope user for a personal install. Preview a skill first with gh skill preview. Needs GitHub CLI 2.90.0 or later (public preview).

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a github-copilot

Project install goes to .agents/skills/; add -g for ~/.copilot/skills/.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .github/skills && cp -r skills-src/.claude/skills/vero-dafny-pitfalls .github/skills/vero-dafny-pitfalls && rm -rf skills-src

Use ~/.copilot/skills/ instead of .github/skills for a personal install. Commit .github/skills so cloud agent and code review can use it.

GitHub Copilot skills documentation · loads skills from .github/skills/, .claude/skills/, .agents/skills/

Paste into GitHub Copilot

Install the "vero-dafny-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-dafny-pitfalls into .github/skills/vero-dafny-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-dafny-pitfalls", then confirm the skill loads.

GitHub Copilot copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

skills CLI

$ npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a opencode

OpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.

GitHub CLI

$ gh skill install sunblaze-ucb/vero vero-dafny-pitfalls --agent opencode

Project scope by default (.agents/skills/); add --scope user for a personal install.

Manual copy

$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/.claude/skills/vero-dafny-pitfalls .opencode/skills/vero-dafny-pitfalls && rm -rf skills-src

Use ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.

OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/

Paste into OpenCode

Install the "vero-dafny-pitfalls" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-dafny-pitfalls into .opencode/skills/vero-dafny-pitfalls/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-dafny-pitfalls", then confirm the skill loads.

OpenCode copies the folder itself, the same result as the manual copy. Check what it changed before you commit it.

Facts

Skill name: vero-dafny-pitfalls
GitHub stars: 107
Token cost: ~1.2k tokens
SKILL.md length: 310 words
Files: 1
Skills in repo: 16
Repo updated: Aug 17, 2026
First seen: Oct 7, 2026
Licence: Apache-2.0

At a glance

Load BEFORE translating any Dafny item to Lean 4 to avoid known Dafny→Lean pitfalls.

Works in 10 steps: ghost vs Compiled Code → method vs function → seq → List T → …
Tasks that involve Translation
SKILL.md covers 1. ghost vs Compiled Code, 2. method vs function, 3. seq → List T and 4. map, plus 6 more sections
Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

Vero Dafny Pitfalls is an agent skill from sunblaze-ucb/vero. Load BEFORE translating any Dafny item to Lean 4 to avoid known Dafny→Lean pitfalls. Pair with vero-source-dafny and vero-lean-pitfalls.

Its SKILL.md is about 1.2k tokens, which your agent loads only when the skill is triggered. It is a single SKILL.md file with no bundled scripts.

It sits in Writing & Content, covering Translation. The licence is Apache-2.0.

When your agent uses it

Tasks that involve Translation

Example prompts

“/vero-dafny-pitfalls”

Requirements

Pre-approved tools (allowed-tools): Read, Write, Edit, Bash, Grep, Glob

Workflow steps

10 steps, taken from the step headings in SKILL.md.

ghost vs Compiled Code
method vs function
seq → List T
map
decreases → termination_by
multiset and set
ensures with Multiple Return Values
Dafny Traits and Classes
forall/exists Quantifiers
Dafny's := vs Lean's :=

What it can do on your machine

Read from SKILL.md and the folder at commit 0a7325d. It shows what the files ask for, not the result of running them.

Tool permissions
Pre-approves these tools, so the agent can use them without asking each time:
- Read
- Write
- Edit
- Bash
- Grep
- Glob
From allowed-tools in the SKILL.md frontmatter.
Runs code
No scripts in the folder and no shell commands in SKILL.md (its code samples are lean and dafny).
From the folder's file list and the shell code blocks in SKILL.md.
Network
No URLs in SKILL.md.
From URLs in SKILL.md, links to its own repository left out.
Credentials
Names no API keys, tokens, secrets or passwords.
From names ending in _API_KEY, _TOKEN, _SECRET, _KEY or _PASSWORD in SKILL.md.

Context cost

Vero Dafny Pitfalls loads about 1.2k tokens when it runs. Until then it costs about 39 tokens; SKILL.md has 310 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it: ~39
When it runs · the whole SKILL.md, loaded when a task matches: ~1.2k

Estimates: characters ÷ 4, the usual rule of thumb; real counts depend on the model's tokenizer. Scripts and assets cost tokens only if the agent reads them.

Safety

Auto-check: notes

The automated check noted patterns worth knowing about, such as sudo or a known installer.

NotePre-approves every shell command (allowed-tools: Bash)SKILL.md
```
allowed-tools: Read, Write, Edit, Bash, Grep, Glob
```

Automated static check — not a guarantee. Review scripts before installing. It scans the text of SKILL.md for risky patterns (piping downloads into a shell, reading credential files, hidden Unicode, destructive commands); files beside SKILL.md are not scanned.

SKILL.md

The full file from sunblaze-ucb/vero at commit 0a7325d, republished under its Apache-2.0 licence (© sunblaze-ucb). 310 words, ~1,162 tokens.

Download SKILL.mdSave it as .claude/skills/vero-dafny-pitfalls/SKILL.md (or your agent's skills folder).

name: vero-dafny-pitfalls
description: Load BEFORE translating any Dafny item to Lean 4 to avoid known Dafny→Lean pitfalls. Pair with vero-source-dafny and vero-lean-pitfalls.
allowed-tools: Read, Write, Edit, Bash, Grep, Glob

Dafny → Lean 4 Translation Pitfalls

Issues specific to translating Dafny to Lean 4.

1. ghost vs Compiled Code

Problem: Dafny ghost variables/functions exist only for verification. In Lean, there's no ghost keyword — use noncomputable for functions that can't be computed, or keep them as pure spec defs.

Dafny:

dafny

ghost function SeqSum(s: seq<int>): int

Lean:

lean

-- If used only in specs/proofs:
def seqSum (s : List Int) : Int := s.foldl (· + ·) 0

-- If it references opaque types:
noncomputable def seqSum (s : List Int) : Int := s.foldl (· + ·) 0

Key: Ghost functions that are pure and have clear definitions should have their body GIVEN. Do not leave sorry in curated Impl/Spec files; use an explicit opaque plus trusted axiom only when the source item is intentionally trusted or external.

2. method vs function

Dafny distinction:

Dafny	Semantics	Lean translation
`function`	Pure, can appear in specs	`def f := body` (give body if simple)
`method`	Imperative, may mutate	`def f := <translated reference impl>` with `code` markers
`ghost method`	Proof-only imperative	usually drop, or convert stated property into a `spec_*`
`lemma`	Proof	benchmark obligation `def spec_* (impl : RepoImpl) : Prop`, no markers
`predicate`	Spec vocabulary	`def f : ... → Prop := ...`, no markers unless it is selected as an API

3. seq`<T>` → List T

Problem: Dafny seq<T> is an immutable sequence. Map to List T.

Common operations:

lean

-- seq<T> operations → List equivalents
-- |s|          → s.length
-- s[i]         → s.get ⟨i, h⟩  (with bound proof)
-- s[i..j]      → s.drop i |>.take (j - i)
-- s + t        → s ++ t
-- s[i := v]    → s.set ⟨i, h⟩ v
-- [v] + s      → v :: s
-- s == t       → s = t

4. map<K,V>

Dafny maps:

dafny

var m: map<string, int>;
m[key]           // lookup (partial)
m[key := value]  // update
key in m         // membership

Lean:

lean

-- For computation: use Std.HashMap
-- For proofs: use a function K → Option V

-- If the map is used in computable code:
def MyMap (K V : Type) := Std.HashMap K V

-- If only in specs:
def MyMap (K V : Type) := K → Option V

5. decreases → termination_by

Dafny:

dafny

function Fib(n: nat): nat
  decreases n

Lean:

lean

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n + 2 => fib (n + 1) + fib n
termination_by n => n

For API reference implementations, add termination_by / decreasing_by when Lean cannot infer termination. The downstream LLM-facing scaffold may replace marker bodies with sorry, but the curated source should build with the real body.

6. multiset and set

Dafny multiset<T>: Use List T and reason about permutations, or Multiset T from Mathlib if available.

Dafny set<T>: Use Finset T for finite sets, or Set T for mathematical sets in proofs.

7. ensures with Multiple Return Values

Dafny:

dafny

method Divide(a: int, b: int) returns (q: int, r: int)
  requires b > 0
  ensures a == q * b + r
  ensures 0 <= r < b

Lean: Use a product type:

lean

def divide (a b : Int) : Int × Int :=
  (a / b, a % b)

def divide_spec (a b : Int) : Prop :=
  b > 0 →
  let (q, r) := divide a b
  a = q * b + r ∧ 0 ≤ r ∧ r < b

8. Dafny Traits and Classes

Dafny:

dafny

trait Comparable {
  function CompareTo(other: Comparable): int
}
class MyType extends Comparable { ... }

Lean: Use type classes:

lean

class Comparable (α : Type) where
  compareTo : α → α → Int

structure MyType where
  ...
  deriving Inhabited

instance : Comparable MyType where
  compareTo _a _b := 0  -- replace with the translated Dafny body

9. forall/exists Quantifiers

Dafny:

dafny

forall i :: 0 <= i < |s| ==> s[i] > 0
exists i :: 0 <= i < |s| && s[i] == target

Lean:

lean

∀ i, i < s.length → s.get ⟨i, by omega⟩ > 0
∃ i, ∃ (h : i < s.length), s.get ⟨i, h⟩ = target

10. Dafny's := vs Lean's :=

Problem: In Dafny, := is assignment (mutable). In Lean, := is definition (immutable). Translate Dafny method bodies that use := as state-passing:

Dafny:

dafny

method Push(s: Stack, v: int) returns (s': Stack) {
  s' := Cons(v, s);
}

Lean:

lean

def push (s : Stack) (v : Int) : Stack :=
  Stack.cons v s

Files

Just SKILL.md in .claude/skills/vero-dafny-pitfalls of sunblaze-ucb/vero.

Open the folder on GitHubat commit 0a7325d

Compare with similar skills

Vero Dafny Pitfalls next to the 5 skills that share the most tags, products or categories with it. Stars are the repository's; “used in” counts other GitHub owners with a copy.

Vero Dafny Pitfalls compared with similar skills
Skill	Stars	Used in	Tokens	Auto-check	Licence	Repo updated
Vero Dafny Pitfalls this skillsunblaze-ucb/vero	107	—	~1.2k	Automated safety check: Notes	Apache-2.0	1 mo ago
Translation Diff ExportDevolutions/UniGetUI	26k	—	~1.1k	Automated safety check: Pass	MIT	yesterday
Sync Translationssymfony/symfony	31k	—	~1.9k	Automated safety check: Pass	MIT	today
Translation Diff ImportDevolutions/UniGetUI	26k	—	~750	Automated safety check: Pass	MIT	yesterday
Translation Diff TranslateDevolutions/UniGetUI	26k	—	~934	Automated safety check: Pass	MIT	yesterday
Generate Translationspayloadcms/payload	45k	—	~1.1k	Automated safety check: Pass	MIT	yesterday

Similar skills

Translation Diff Export
Devolutions/UniGetUI
Compares UniGetUI JSON locale files against English, identifies untranslated or source-changed keys, and generates patch, reference, and handoff files for a target language.
26k GitHub stars~1.1k tokensUpdated yesterday
Writing & ContentAuto-check passed
Sync Translations
symfony/symfony
Synchronize translation catalogs across maintained Symfony branches: find messages that newer branches added to the English catalogs but that are still missing from the oldest maintained branch…
31k GitHub stars~1.9k tokensUpdated today
Writing & ContentAuto-check passed
Translation Diff Import
Devolutions/UniGetUI
Merges translated key-value pairs from a UniGetUI JSON localization patch back into the full language file and validates the merged result.
26k GitHub stars~750 tokensUpdated yesterday
Writing & ContentAuto-check passed
Translation Diff Translate
Devolutions/UniGetUI
Translates a sparse UniGetUI JSON language patch, writes completed entries into the working copy, preserves placeholders and terminology, and prepares the patch for merge-back.
26k GitHub stars~934 tokensUpdated yesterday
Writing & ContentAuto-check passed
Generate Translations
payloadcms/payload
A skill your agent uses when new translation keys are added to packages to generate new translations strings
45k GitHub stars~1.1k tokensUpdated yesterday
Writing & ContentAuto-check passed
InkOS Creative Harness
Narcooo/inkos
Drives long-form fiction, scripts, storyboards, interactive films and long-document translation through InkOS, with every change made by a typed action.
10k GitHub starsUsed in 1 repo~1.1k tokens
Writing & ContentAuto-check passed

Questions about Vero Dafny Pitfalls

What does Vero Dafny Pitfalls do?

Load BEFORE translating any Dafny item to Lean 4 to avoid known Dafny→Lean pitfalls. Vero Dafny Pitfalls is an agent skill from sunblaze-ucb/vero. Load BEFORE translating any Dafny item to Lean 4 to avoid known Dafny→Lean pitfalls.

When should I use Vero Dafny Pitfalls?

Vero Dafny Pitfalls fits situations like: tasks that involve Translation.

How do I install Vero Dafny Pitfalls in Claude Code?

Run `npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a claude-code`. Or copy the skill folder (.claude/skills/vero-dafny-pitfalls in sunblaze-ucb/vero) into .claude/skills/vero-dafny-pitfalls in your project. Claude Code loads it when a task matches its description.

How do I install Vero Dafny Pitfalls in Codex?

Run `npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a codex`. Or copy the skill folder (.claude/skills/vero-dafny-pitfalls in sunblaze-ucb/vero) into .agents/skills/vero-dafny-pitfalls in your project. Codex loads it when a task matches its description.

Can I use Vero Dafny Pitfalls in Cursor, Gemini CLI or GitHub Copilot?

Cursor, Gemini CLI, GitHub Copilot and OpenCode also load SKILL.md folders. With the skills CLI, run `npx skills add sunblaze-ucb/vero --skill vero-dafny-pitfalls -a cursor` (or -a gemini-cli, github-copilot or opencode for the others). To copy it by hand, put the folder in .cursor/skills/vero-dafny-pitfalls, .gemini/skills/vero-dafny-pitfalls, .github/skills/vero-dafny-pitfalls and .opencode/skills/vero-dafny-pitfalls in your project.

What does Vero Dafny Pitfalls need to run?

SKILL.md names no scripts, command-line tools or credentials: Vero Dafny Pitfalls is instructions for the agent only. Its frontmatter pre-approves these tools: Read, Write, Edit, Bash, Grep, Glob.

Does Vero Dafny Pitfalls access the network?

SKILL.md contains no URLs. Any network use would come from the scripts or tools the agent runs. This is read from the text; nothing was executed.

Is Vero Dafny Pitfalls safe to install?

Our automated static check of SKILL.md found notes only (pre-approves every shell command (allowed-tools: bash)), nothing it rates as a warning. It is not a guarantee. Review the folder before installing.

What licence does Vero Dafny Pitfalls use?

Vero Dafny Pitfalls is published under the Apache-2.0 licence (the repository's licence). It allows redistribution, so the full SKILL.md is shown on this page.

How many tokens does Vero Dafny Pitfalls use?

About 1.2k tokens (SKILL.md is roughly 4.6k characters). Agents keep only the skill's name and description in context until a task matches; then they load SKILL.md in full.

What are the alternatives to Vero Dafny Pitfalls?

Skills that share tags, products or a category with Vero Dafny Pitfalls: Translation Diff Export (Devolutions/UniGetUI, 26k stars), Sync Translations (symfony/symfony, 31k stars), Translation Diff Import (Devolutions/UniGetUI, 26k stars) and Translation Diff Translate (Devolutions/UniGetUI, 26k stars). The comparison table on this page puts their stars, adoption, token cost, safety result and licence side by side.

Who maintains Vero Dafny Pitfalls?

sunblaze-ucb (a GitHub organization) maintains it in sunblaze-ucb/vero, which has 107 GitHub stars. The repository holds 16 skills in this directory. The repository was last updated on August 17, 2026.

Source: sunblaze-ucb/vero on GitHub. Facts on this page come from the repository at the commit we read; the author's words are quoted as theirs.

Install Vero Dafny Pitfalls

Facts

At a glance

What it does

When your agent uses it

Example prompts

Requirements

Workflow steps

What it can do on your machine

Tool permissions

Runs code

Network

Credentials

Context cost

Safety

SKILL.md

Dafny → Lean 4 Translation Pitfalls

1. ghost vs Compiled Code

2. method vs function

3. seq<T> → List T

4. map<K,V>

5. decreases → termination_by

6. multiset and set

7. ensures with Multiple Return Values

8. Dafny Traits and Classes

9. forall/exists Quantifiers

10. Dafny's := vs Lean's :=

Files

Compare with similar skills

Similar skills

More from sunblaze-ucb/vero

Related

Questions about Vero Dafny Pitfalls

3. seq`<T>` → List T