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.
Use after human review of vero-discover output to compute dependency closure of selected items, plan Lean file layout, and determine translation order.
Install Vero Select
$ npx skills add sunblaze-ucb/vero --skill vero-select -a claude-codeProject install by default; add -g for ~/.claude/skills/.
$ gh skill install sunblaze-ucb/vero vero-select --agent claude-codeProject scope by default; add --scope user for a personal install. Needs GitHub CLI 2.90.0 or later (public preview).
$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .claude/skills && cp -r skills-src/.claude/skills/vero-select .claude/skills/vero-select && rm -rf skills-srcUse ~/.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/
Install the "vero-select" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-select into .claude/skills/vero-select/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-select", 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 install https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-selectType 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.
$ npx skills add sunblaze-ucb/vero --skill vero-select -a codexProject install goes to .agents/skills/; add -g for ~/.codex/skills/.
$ gh skill install sunblaze-ucb/vero vero-select --agent codexProject scope by default (.agents/skills/); add --scope user for a personal install.
$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .agents/skills && cp -r skills-src/.claude/skills/vero-select .agents/skills/vero-select && rm -rf skills-srcUse ~/.agents/skills/ instead of .agents/skills for a personal install.
Codex skills documentation · loads skills from .agents/skills/
Install the "vero-select" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-select into .agents/skills/vero-select/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-select", 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.
$ npx skills add sunblaze-ucb/vero --skill vero-select -a cursorProject install goes to .agents/skills/; add -g for ~/.cursor/skills/.
$ gh skill install sunblaze-ucb/vero vero-select --agent cursorProject scope by default (.agents/skills/); add --scope user for a personal install.
$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .cursor/skills && cp -r skills-src/.claude/skills/vero-select .cursor/skills/vero-select && rm -rf skills-srcUse ~/.cursor/skills/ instead of .cursor/skills for a personal install.
Cursor skills documentation · loads skills from .cursor/skills/, .agents/skills/, .claude/skills/, .codex/skills/
Install the "vero-select" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-select into .cursor/skills/vero-select/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-select", 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 https://github.com/sunblaze-ucb/vero.git --path .claude/skills/vero-select--scope user (default) or --scope workspace; --path is the subfolder of the repo that holds the skill; --consent skips the security confirmation prompt.
$ npx skills add sunblaze-ucb/vero --skill vero-select -a gemini-cliProject install goes to .agents/skills/; add -g for ~/.gemini/skills/.
$ gh skill install sunblaze-ucb/vero vero-select --agent gemini-cliProject scope by default (.agents/skills/); add --scope user for a personal install.
$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .gemini/skills && cp -r skills-src/.claude/skills/vero-select .gemini/skills/vero-select && rm -rf skills-srcUse ~/.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/
Install the "vero-select" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-select into .gemini/skills/vero-select/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-select", 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.
$ gh skill install sunblaze-ucb/vero vero-selectInstalls 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).
$ npx skills add sunblaze-ucb/vero --skill vero-select -a github-copilotProject install goes to .agents/skills/; add -g for ~/.copilot/skills/.
$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .github/skills && cp -r skills-src/.claude/skills/vero-select .github/skills/vero-select && rm -rf skills-srcUse ~/.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/
Install the "vero-select" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-select into .github/skills/vero-select/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-select", 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.
$ npx skills add sunblaze-ucb/vero --skill vero-select -a opencodeOpenCode documents no install command of its own. Project install goes to .agents/skills/; add -g for ~/.config/opencode/skills/.
$ gh skill install sunblaze-ucb/vero vero-select --agent opencodeProject scope by default (.agents/skills/); add --scope user for a personal install.
$ git clone --depth 1 https://github.com/sunblaze-ucb/vero.git skills-src && mkdir -p .opencode/skills && cp -r skills-src/.claude/skills/vero-select .opencode/skills/vero-select && rm -rf skills-srcUse ~/.config/opencode/skills/ instead of .opencode/skills for a personal install.
OpenCode skills documentation · loads skills from .opencode/skills/, .claude/skills/, .agents/skills/
Install the "vero-select" agent skill from https://github.com/sunblaze-ucb/vero/tree/main/.claude/skills/vero-select into .opencode/skills/vero-select/ in this project. Copy the whole folder (SKILL.md and every file beside it), keep the folder name "vero-select", 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-select- GitHub stars
- 107
- Token cost
- ~3.7k tokens
- SKILL.md length
- 1,205 words
- Files
- 1
- Skills in repo
- 16
- Repo updated
- First seen
- Licence
- Apache-2.0
At a glance
Use after human review of vero-discover output to compute dependency closure of selected items, plan Lean file layout, and determine translation order.
- Works in 5 steps: Parse selections → Compute dependency closure → Layer assignment → …
- Tasks that involve Translation
- SKILL.md covers When to use, Input, Step 1: Parse selections and Step 2: Compute dependency…, plus 7 more sections
- Instructions only: no scripts, shell commands, URLs or credentials in SKILL.md
What it does
Vero Select is an agent skill from sunblaze-ucb/vero. Use after human review of vero-discover output to compute dependency closure of selected items, plan Lean file layout, and determine translation order. Produces curation/selection.md and curation/selectionplan.json.
Its SKILL.md is about 3.7k 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-select”
Requirements
- Pre-approved tools (allowed-tools): Read, Write, Bash, Grep, Glob
Workflow steps
5 steps, taken from the step headings in SKILL.md.
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:
ReadWriteBashGrepGlob
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 markdown and json).
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 Select loads about 3.7k tokens when it runs. Until then it costs about 57 tokens; SKILL.md has 1,205 words of instructions outside code blocks.
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, 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). 1,205 words, ~3,704 tokens.
Download SKILL.mdSave it as
.claude/skills/vero-select/SKILL.md (or your agent's skills folder).- name
- vero-select
- description
- Use after human review of vero-discover output to compute dependency closure of selected items, plan Lean file layout, and determine translation order. Produces curation/selection.md and curation/selection_plan.json.
- allowed-tools
- Read, Write, Bash, Grep, Glob
VCG Selection: Dependency Closure and Translation Planning
Read human-annotated discovery markdowns, compute the dependency closure of selected items, plan the Lean file layout, and determine the layer-by-layer translation order.
When to use
- After human review of
curation/discovery/*.md(items checked/unchecked) - To compute what must be translated based on selections + dependencies
- To plan the Lean output directory structure and translation order
Input
Human-annotated discovery files at curation/discovery/*.md where each item line reads:
- [x] category=<api|api_helper|spec|spec_helper|type|test> <item>— included, with curator-confirmed category- [ ] category=<…> <item>— excluded from the benchmark
The category was suggested by vero-discover and confirmed (or overridden) by the curator during review.
Step 1: Parse selections
For each discovery file (prefer discovery_report.json — same data, structured):
- Extract every checked item as
(item, category). - Extract the dependency list attached to each item.
- Build a dependency graph:
item → [dependency names].
Step 2: Compute dependency closure
Starting from the set of checked items, close under dependencies:
closure = dict((item, category) for (item, category) in checked)
worklist = list(checked)
while worklist:
item = worklist.pop()
for dep in dependencies(item):
if dep not in closure:
# Inherit a default category for auto-pulled items:
# - A type dependency → category=type
# - A spec's bare-name → category=spec_helper
# - An API's call-dep → category=api_helper (flagged — see below)
closure[dep] = infer_category(item, dep)
worklist.append(dep)Closure warnings — two kinds
Kind 1: auto-included items. The closure pulled in an item the curator didn't check.
- `funcA` (checked, category=api) depends on `TypeB` (NOT checked) — **pulled in as category=type**
- From: `src--module1.dfy.md`
- Reason: type dependency in `funcA`'s signatureKind 2: category mismatch (hard error). A spec references a bare-name item that isn't marked as a spec helper (or type, or API via impl.<…>). A spec cannot typecheck against a name that won't be curated.
- Spec `push_pop_roundtrip` (category=spec) references bare name `toSeq` — **mismatch**
- Problem: `toSeq` is marked category=api_helper, which by default is not curated.
- Fix one of:
- (a) Promote `toSeq` to category=spec_helper (curator provides the body).
- (b) Rewrite the spec to reference `impl.<pkg>.toSeq` and promote `toSeq` to category=api.
- (c) Drop the spec.Spec-helper auto-promotion. If closure would pull a bare-name spec dependency in with a weaker category (api_helper, or missing), silently bump it to category=spec_helper and emit a Kind-1 warning. This is the mechanism that prevents a spec from being under-scoped into an un-typechecking state.
The curator can then either:
- Accept the auto-promotion (leave as-is).
- Override by explicitly categorizing the dependency differently.
- Uncheck the spec to drop the whole chain.
Step 2b: Scope-warning check against old curation
If a sibling benchmarks/<name>_old/ exists, compute two counts from the current closure and two from the old tree:
| Metric | Current closure | Old tree |
|---|---|---|
| API count | count of category=api in closure | count old implementation tasks / code slots in the old tree |
| Spec count | count of category=spec in closure | count old proof/spec obligations in the old tree |
If either current count is lower than the old count, emit a scope warning as the first paragraph of selection.md:
> ⚠ **Scope warning.** Current closure has N APIs and M specs. The pre-existing
> `benchmarks/<name>_old/` has N' APIs and M' specs. If N < N' or M < M', the
> curator is probably under-scoping. Review and widen the checkboxes before
> proceeding.Do not silently proceed — surface the discrepancy by kind so the curator knows whether APIs, Specs, or both are short.
Step 3: Layer assignment
Assign each item in the closure to a translation layer:
| Layer | Contents | Rule |
|---|---|---|
| 0 | Types with no type dependencies | Foundation types |
| 1 | Types depending on Layer 0 types | Compound types |
| 2 | Spec helpers + API helpers depending only on Layer 0–1 types | Curator-given vocabulary |
| 3 | APIs depending only on earlier layers | Implementation obligations |
| 4+ | APIs depending on earlier APIs | Composition |
| S | Specs (reference items in any earlier layer; Spec files are independent of each other) | Proof obligations |
| T | Tests | #guard blocks |
Rules:
- Types → Spec/API helpers → APIs → Specs → Tests.
- Within the same layer, items are independent and can be translated in parallel.
- A
category=specitem always lands in Layer S, regardless of dep depth. - A
category=spec_helperitem lands in Layer 2 alongside other spec-helpers even if it depends on a type — the goal is thatSpec/<Module>.leancan import the helpers directly viaImpl/<Module>.leanwithout pulling in the full API chain.
Step 4: Plan Lean File Layout
Map source files to Lean files, mirroring the source directory structure:
| Source file | Lean file | Namespace |
|---|---|---|
src/tree.dfy | ProjectName/Tree.lean | ProjectName.Tree |
src/merkle.dfy | ProjectName/Merkle.lean | ProjectName.Merkle |
| ... | ... | ... |
Add spec and test files:
| Purpose | Lean file | Depends on |
|---|---|---|
| Spec for Tree | ProjectName/Spec/Tree.lean | ProjectName/Tree.lean |
| Tests | ProjectName/Test.lean | All API files |
Step 5: Estimate Metrics
For each planned Lean file, estimate:
| File | Items | code slots (est.) | spec obligations (est.) | opaque (est.) | axiom (est.) | Notes |
|---|---|---|---|---|---|---|
Tree.lean | 5 types | 0 | 0 | 0 | 0 | All types, fully defined |
Merkle.lean | 5 fns | 5 | 0 | 0 | 0 | Complex bodies become API slots |
Spec/Tree.lean | 11 thms | 0 | 11 | 0 | 0 | Frozen spec obligations |
| ... | ... | ... | ... | ... | ... |
Estimation rules:
- Types → 0 code slots (types are always fully defined)
body: given→ 0 code slotscategory=apiwith non-opaque body → 1 code slot per functionbody: opaque→ 1 opaque per function, + N axioms for proved properties- Each selected theorem/lemma → 1 spec obligation
- Each function with
ensures→ 1 companion spec def (spec task)
Show full SKILL.md (522 more words)Show less
Companion Def Pairs
Identify functions that need companion spec definitions. A companion pair consists of:
- Function —
def f := <translated reference impl>inside acodemarker (implementation task after pre-agent materialization) - Spec def —
def f_spec : Prop := <property>(body given — IS the specification) - Downstream proof task — generated later from the spec def; translate does not emit
Proof/
These arise from:
- Dafny functions with
ensuresclauses - Verus
fnwithensures(generates companion theorem) - Any function whose correctness is stated as a separate lemma
Mark companion pairs in the metrics — they generate one code slot and one spec obligation in curation; proof tasks are materialized downstream from the spec obligation.
Output: curation/selection.md
# Selection Report: {project_name}
## Selection Summary
| Category | Selected | Closure-added | Total | Skipped |
|----------|--------:|-------------:|------:|--------:|
| Types | N | N | N | N |
| Spec functions | N | N | N | N |
| Exec functions | N | N | N | N |
| Predicates | N | N | N | N |
| Theorems | N | N | N | N |
| Axioms | N | N | N | N |
| Tests | N | N | N | N |
| **Total** | **N** | **N** | **N** | **N** |
## Closure Warnings
- `itemA` depends on `itemB` (not selected) — pulled into closure
- Source: `path/to/file`
- Reason: {type dep | call dep | proof dep}
## Translation Layers
### Layer 0: Foundation Types
| Item | Source | Lean file | Notes |
|------|--------|-----------|-------|
| `Tree` | `tree.dfy` | `Project/Tree.lean` | 2 constructors |
| ... | ... | ... | ... |
### Layer 1: Compound Types
...
### Layer 2: Core Functions
...
### Layer S: Specifications
| Item | Source | Lean file | Depends on |
|------|--------|-----------|------------|
| `height_leavesIn` | `tree.dfy` | `Project/Spec/Tree.lean` | `Tree.leavesIn` |
| ... | ... | ... | ... |
### Layer T: Tests
| Item | Source | Lean file | Tests |
|------|--------|-----------|-------|
| `test_deposit` | `RunDeposit.dfy` | `Project/Test.lean` | `deposit`, `getDepositRoot` |
## Lean File Layout
{ProjectName}/ ├── {ProjectName}.lean (root import hub) ├── {ProjectName}/ │ ├── Tree.lean (Layer 0) │ ├── Merkle.lean (Layer 2) │ ├── Contract.lean (Layer 3) │ ├── Spec/ │ │ ├── Tree.lean (Layer S) │ │ ├── Merkle.lean (Layer S) │ │ └── Contract.lean (Layer S) │ └── Test.lean (Layer T) ├── lakefile.toml └── lean-toolchain
## Estimated Metrics
| File | Items | sorry (est.) | opaque | axiom | Lines (est.) |
|------|------:|------------:|-------:|------:|------------:|
| ... | ... | ... | ... | ... | ... |
| **Total** | **N** | **N** | **N** | **N** | **N** |
## Human Review Notes
[Reviewer adds notes, adjustments, approval here]Machine-Readable Output: curation/selection_plan.json
Also write a JSON file with the structured selection plan:
{
"selected_items": [
{
"name": "Stack",
"qualified_name": "Stack",
"category": "type",
"visibility": "public",
"source_file": "Stack.dfy",
"source_line": 3,
"checked": true,
"closure_added": false,
"lean_file": "DummyDafny/Impl/Stack.lean",
"lean_name": "Stack",
"layer": 0
},
{
"name": "push",
"qualified_name": "push",
"category": "api",
"visibility": "public",
"source_file": "Stack.dfy",
"source_line": 8,
"checked": true,
"closure_added": false,
"lean_file": "DummyDafny/Impl/Stack.lean",
"lean_name": "push",
"layer": 3
},
{
"name": "toSeq",
"qualified_name": "toSeq",
"category": "spec_helper",
"visibility": "internal",
"source_file": "Stack.dfy",
"source_line": 22,
"checked": false,
"closure_added": true,
"closure_promoted_from": "api_helper",
"lean_file": "DummyDafny/Impl/Stack.lean",
"lean_name": "toSeq",
"layer": 2
},
{
"name": "push_pop_roundtrip",
"qualified_name": "push_pop_roundtrip",
"category": "spec",
"visibility": "public",
"source_file": "StackSpec.dfy",
"source_line": 5,
"checked": true,
"closure_added": false,
"lean_file": "DummyDafny/Spec/Stack.lean",
"lean_name": "spec_push_pop_roundtrip",
"layer": 100
}
],
"layers": {
"0": ["Stack"],
"2": ["toSeq"],
"3": ["push", "pop", "peek", "size"],
"100": ["push_pop_roundtrip", "push_increases_size"],
"200": ["test_main"]
},
"lean_files": {
"DummyDafny/Impl/Stack.lean": ["Stack", "toSeq", "push", "pop", "peek", "size"],
"DummyDafny/Spec/Stack.lean": ["push_pop_roundtrip", "push_increases_size"],
"DummyDafny/Test.lean": ["test_main"]
},
"closure_warnings": [
{
"kind": "auto_included",
"item": "toSeq",
"reason": "spec `push_pop_roundtrip` references bare name; promoted to spec_helper"
}
],
"category_counts": {
"api": 4,
"api_helper": 0,
"spec": 2,
"spec_helper": 1,
"type": 1,
"test": 1
},
"old_benchmark_counts": {
"present": false,
"api": null,
"spec": null
}
}Layer convention: 0–99 for types / helpers / APIs, 100+ for specs (Layer S), 200+ for tests (Layer T). lean_name is the destination Lean identifier (for spec items, prefix with spec_ per paradigm).
Workflow (incremental — avoid one giant Write at the end)
Read inputs and emit outputs one chunk at a time. A monolithic "digest-everything-then-write-selection.md" plan tends to hit long thinking stalls on repos with 15+ discovery files. Instead:
Step 1 — Prefer discovery_report.json over the markdowns.
Read curation/discovery_report.json first. It has the full
dependency graph in ~1/10th the tokens of the markdown set. Only read
a specific discovery/<file>.md when you need human-added review
notes for a borderline item. Do NOT read all 19 markdowns up-front.
Step 2 — Parse checkboxes cheaply.
Use a single Bash call with grep "^- \[x\]" curation/discovery/*.md
to pull out the selected-item lines (and their file-of-origin). Do
NOT Read every markdown just to find the [x]s.
Step 3 — Compute closure deterministically. Walk the dependency graph from the selected set. This is a pure graph computation; no thinking required.
Step 4 — Write selection.md section by section.
Do NOT compose the whole report in a single Write. Emit it in this
order, each as its own Write / Edit call:
Writethe header +## Selection Summarytable.Editto append## Closure Warnings.Editto append## Translation Layers— and within it, one Edit per layer (Layer 0, then Layer 1, …, then Layer S, then Layer T). Each layer Edit keepsselection.mdvalid markdown.Editto append## Lean File Layout(tree diagram).Editto append## Estimated Metrics.Editto append## Human Review Notes(empty — reviewer fills in).
Between edits, pause for the closure computation — emit any surprising closure additions as a Write to the file before continuing, so partial progress is observable to the curator even if the session is interrupted.
Step 5 — Emit selection_plan.json last.
Only after selection.md is complete and self-consistent. One Write.
Check-in rule: before each Write/Edit, in one sentence name which section you are about to emit. This makes stalled-in-thinking episodes obvious to a watching human (they see "I will now emit Layer 2" and then the next log line in ≤ 30s).
(See Step 2b above for the scope-warning rule against an existing benchmarks/<name>_old/.)
© 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-select of sunblaze-ucb/vero.
Open the folder on GitHubat commit 0a7325d
Compare with similar skills
Vero Select 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.
| Skill | Stars | Used in | Tokens | Auto-check | Licence | Repo updated |
|---|---|---|---|---|---|---|
| Vero Select this skillsunblaze-ucb/vero | 107 | — | ~3.7k | Automated safety check: Notes | Apache-2.0 | |
| Translation Diff ExportDevolutions/UniGetUI | 26k | — | ~1.1k | Automated safety check: Pass | MIT | |
| Sync Translationssymfony/symfony | 31k | — | ~1.9k | Automated safety check: Pass | MIT | |
| Translation Diff ImportDevolutions/UniGetUI | 26k | — | ~750 | Automated safety check: Pass | MIT | |
| Translation Diff TranslateDevolutions/UniGetUI | 26k | — | ~934 | Automated safety check: Pass | MIT | |
| Generate Translationspayloadcms/payload | 45k | — | ~1.1k | Automated safety check: Pass | MIT |
Similar skills
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…
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.
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.
Generate Translations
payloadcms/payload
A skill your agent uses when new translation keys are added to packages to generate new translations strings
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.
More from sunblaze-ucb/vero
All 16 skills in this repoVero 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.
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.
Vero Coq Pitfalls
sunblaze-ucb/vero
Load BEFORE translating any Coq item to Lean 4 to avoid known Coq→Lean pitfalls.
Vero Dafny Pitfalls
sunblaze-ucb/vero
Load BEFORE translating any Dafny item to Lean 4 to avoid known Dafny→Lean pitfalls.
Vero Lean Pitfalls
sunblaze-ucb/vero
Load BEFORE writing any Lean 4 translation to avoid common Lean pitfalls (universes, coercions, type-class resolution, notation).
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.
Related
Categories
Questions about Vero Select
What does Vero Select do?
Use after human review of vero-discover output to compute dependency closure of selected items, plan Lean file layout, and determine translation order. Vero Select is an agent skill from sunblaze-ucb/vero. Use after human review of vero-discover output to compute dependency closure of selected items, plan Lean file layout, and determine translation order.
When should I use Vero Select?
Vero Select fits situations like: tasks that involve Translation.
How do I install Vero Select in Claude Code?
Run `npx skills add sunblaze-ucb/vero --skill vero-select -a claude-code`. Or copy the skill folder (.claude/skills/vero-select in sunblaze-ucb/vero) into .claude/skills/vero-select in your project. Claude Code loads it when a task matches its description.
How do I install Vero Select in Codex?
Run `npx skills add sunblaze-ucb/vero --skill vero-select -a codex`. Or copy the skill folder (.claude/skills/vero-select in sunblaze-ucb/vero) into .agents/skills/vero-select in your project. Codex loads it when a task matches its description.
Can I use Vero Select 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-select -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-select, .gemini/skills/vero-select, .github/skills/vero-select and .opencode/skills/vero-select in your project.
What does Vero Select need to run?
SKILL.md names no scripts, command-line tools or credentials: Vero Select is instructions for the agent only. Its frontmatter pre-approves these tools: Read, Write, Bash, Grep, Glob.
Does Vero Select 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 Select 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 Select use?
Vero Select 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 Select use?
About 3.7k tokens (SKILL.md is roughly 15k 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 Select?
Skills that share tags, products or a category with Vero Select: 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 Select?
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.