New: 98,000+ skills indexed from GitHub repos with 100+ stars · every skill safety-checkedBrowse top skillsTop skills
Esc to closeBrowse all skills
Submit a skillBrowse skills
Submit a skillBrowse skills

Agent skill

Vero Verus Pitfalls

by sunblaze-ucb in sunblaze-ucb/vero

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

Apache-2.0Auto-check: notesWriting & Content

Install Vero Verus Pitfalls

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

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

GitHub CLI
$ gh skill install sunblaze-ucb/vero vero-verus-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-verus-pitfalls .claude/skills/vero-verus-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/

Facts

Skill name
vero-verus-pitfalls
GitHub stars
107
Token cost
~1.1k tokens
SKILL.md length
368 words
Files
1
Skills in repo
16
Repo updated
First seen
Licence
Apache-2.0

At a glance

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

  • Works in 8 steps: external_body → opaque + noncomputable… → requires/ensures → Hypotheses + Prop → exec vs proof vs spec Functions → …
  • Tasks that involve Translation
  • SKILL.md covers 1. external_body → opaque +…, 2. requires/ensures →…, 3. exec vs proof vs spec… and 4. Ghost Variables and old(), plus 4 more sections
  • Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md

What it does

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

Its SKILL.md is about 1.1k 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-verus-pitfalls”

Requirements

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

Workflow steps

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

  1. external_body → opaque + noncomputable Chain
  2. requires/ensures → Hypotheses + Prop
  3. exec vs proof vs spec Functions
  4. Ghost Variables and old()
  5. Rust-Style Mutation → Pure Functional
  6. Linear Types / Tracked
  7. Integer Overflow
  8. Verus broadcast/reveal

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 rust).

    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 Verus Pitfalls loads about 1.1k tokens when it runs. Until then it costs about 39 tokens; SKILL.md has 368 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.1k

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). 368 words, ~1,150 tokens.

Download SKILL.mdSave it as .claude/skills/vero-verus-pitfalls/SKILL.md (or your agent's skills folder).
name
vero-verus-pitfalls
description
Load BEFORE translating any Verus item to Lean 4 to avoid known Verus→Lean pitfalls. Pair with vero-source-verus and vero-lean-pitfalls.
allowed-tools
Read, Write, Edit, Bash, Grep, Glob

Verus → Lean 4 Translation Pitfalls

Issues specific to translating Verus (Rust-based verification) to Lean 4.

1. external_body → opaque + noncomputable Chain

Problem: Verus #[verifier(external_body)] marks types/functions whose implementation is trusted (not verified). In Lean, translate to opaque. BUT: every downstream function referencing it must be noncomputable.

Verus:

rust
#[verifier(external_body)]
pub struct HashMap<K, V> { ... }

#[verifier(external_body)]
pub fn insert<K, V>(m: &mut HashMap<K, V>, k: K, v: V) { ... }

Lean (correct):

lean
opaque HashMap (K V : Type) : Type

opaque HashMap.insert {K V : Type} (m : HashMap K V) (k : K) (v : V) : HashMap K V

-- ALL functions using insert must be noncomputable:
noncomputable def receiveImpl (state : State) (msg : Msg) : State :=
-- !benchmark @start code def=receiveImpl
  -- translated reference body using HashMap.insert
  ...
-- !benchmark @end code def=receiveImpl

Key insight: Before using opaque, check lean_local_search("HashMap") — Lean has Std.HashMap built in. If the source just wraps a standard collection, map to the stdlib version instead.

2. requires/ensures → Hypotheses + Prop

Verus:

rust
fn deposit(&mut self, value: u64)
    requires
        self.count < MAX_COUNT,
        value > 0,
    ensures
        self.balance == old(self).balance + value,

Lean curation output:

lean
-- Function: translated reference implementation
def deposit (s : State) (value : UInt64) : State :=
-- !benchmark @start code def=deposit
  ...
-- !benchmark @end code def=deposit

-- Spec: ensures become frozen benchmark obligations, with no markers
def spec_deposit (impl : RepoImpl) : Prop :=
  ∀ (s : State) (value : UInt64),
  s.count < MAX_COUNT →
  value > 0 →
  (impl.bank.deposit s value).balance = s.balance + value.toNat

Note: requires become hypotheses (→) in the spec, not separate precondition functions. Do not emit spec markers; Spec files are frozen.

3. exec vs proof vs spec Functions

Verus distinguishes three modes:

Verus modeLean translation
exec fndef f := <translated reference impl> with code markers
proof fnbenchmark obligation def spec_* (impl : RepoImpl) : Prop in Spec, no markers
spec fnvocabulary/helper def with a full body, no markers
spec fn (opaque)opaque f_spec ... (no markers)

Key: exec functions are the LLM-editable code tasks, but curation still stores the translated reference body inside the marker. proof functions become frozen spec obligations, not curation-time theorems.

4. Ghost Variables and old()

Problem: Verus old(self) refers to the pre-state. Lean has no built-in old — you must pass both pre and post state explicitly.

Verus:

rust
ensures self.items == old(self).items.push(value)

Lean:

lean
def push_spec (pre post : Stack) (value : T) : Prop :=
  post.items = pre.items ++ [value]
Show full SKILL.md (155 more words)Show less

5. Rust-Style Mutation → Pure Functional

Problem: Verus functions take &mut self. Lean is purely functional — translate to functions that take old state and return new state.

Verus:

rust
fn push(&mut self, value: T)

Lean:

lean
def push (s : Stack T) (value : T) : Stack T :=
  { s with items := s.items ++ [value] }

6. Linear Types / Tracked

Problem: Verus tracked and Tracked<T> are ghost/proof-level values. In Lean, these become regular parameters with Prop constraints.

Simple rule: Drop tracked annotations. If the tracked value is used in specs, keep it as a regular parameter.

7. Integer Overflow

Problem: Verus uses u32, u64, etc. with overflow checking. Lean's UInt32, UInt64 wrap on overflow (modular arithmetic).

Fix: For specs that reason about overflow, use Nat or Int and add explicit bounds as hypotheses:

lean
def safe_add (a b : Nat) (h : a + b < 2^32) : Nat := a + b

8. Verus broadcast/reveal

Problem: Verus broadcast use and reveal() control lemma visibility. No direct Lean equivalent.

Fix: In Lean, all lemmas are always available. Translate broadcast lemmas as regular theorems. If the source uses reveal(f) before calling f, the Lean translation doesn't need it — unfold f or simp [f] works.

© sunblaze-ucb, Apache-2.0. Rendered from Markdown: HTML in the file is shown as text, images as links, and headings moved down two levels. Raw file

Files

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

Open the folder on GitHubat commit 0a7325d

Compare with similar skills

Vero Verus 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 Verus Pitfalls compared with similar skills
SkillStarsUsed inTokensAuto-checkLicenceRepo updated
Vero Verus Pitfalls this skillsunblaze-ucb/vero107—~1.1kAutomated safety check: NotesApache-2.0
Translation Diff ExportDevolutions/UniGetUI26k—~1.1kAutomated safety check: PassMIT
Sync Translationssymfony/symfony31k—~1.9kAutomated safety check: PassMIT
Translation Diff ImportDevolutions/UniGetUI26k—~750Automated safety check: PassMIT
Translation Diff TranslateDevolutions/UniGetUI26k—~934Automated safety check: PassMIT
Generate Translationspayloadcms/payload45k—~1.1kAutomated safety check: PassMIT

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

More from sunblaze-ucb/vero

All 16 skills in this repo

  • Vero Discover

    sunblaze-ucb/vero

    A skill your agent uses when scanning a verified source repo (Dafny, Verus, or Coq) to classify every item and produce per-file discovery markdown for human curation.

    107 GitHub stars~3.9k tokensUpdated 1 mo ago
    Auto-check: notes

  • Vero Translate

    sunblaze-ucb/vero

    A skill your agent uses when translating selected verified items from Dafny/Verus/Coq into a compilable Lean 4 benchmark.

    107 GitHub stars~4.9k tokensUpdated 1 mo ago
    Auto-check: notes

  • Vero Coq Pitfalls

    sunblaze-ucb/vero

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

    107 GitHub stars~1.5k tokensUpdated 1 mo ago
    Auto-check: notes

  • Vero Dafny Pitfalls

    sunblaze-ucb/vero

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

    107 GitHub stars~1.2k tokensUpdated 1 mo ago
    Auto-check: notes

  • Vero Lean Pitfalls

    sunblaze-ucb/vero

    Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation).

    107 GitHub stars~1.4k tokensUpdated 1 mo ago
    Auto-check: notes

  • Vero Plan

    sunblaze-ucb/vero

    Use after vero-select to write a detailed translation plan as .vero/plan.json — the authoritative contract the TRANSLATE stage executes.

    107 GitHub stars~3.6k tokensUpdated 1 mo ago
    Auto-check: notes

Categories

Questions about Vero Verus Pitfalls

What does Vero Verus Pitfalls do?

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

When should I use Vero Verus Pitfalls?

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

How do I install Vero Verus Pitfalls in Claude Code?

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

How do I install Vero Verus Pitfalls in Codex?

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

Can I use Vero Verus 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-verus-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-verus-pitfalls, .gemini/skills/vero-verus-pitfalls, .github/skills/vero-verus-pitfalls and .opencode/skills/vero-verus-pitfalls in your project.

What does Vero Verus Pitfalls need to run?

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

Does Vero Verus 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 Verus 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 Verus Pitfalls use?

Vero Verus 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 Verus Pitfalls use?

About 1.1k 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 Verus Pitfalls?

Skills that share tags, products or a category with Vero Verus 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 Verus 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.