Vero Source Python

What it does

When your agent uses it

• Tasks that involve Translation

Example prompts

• “/vero-source-python”

Requirements

• Python 3

Workflow steps

5 steps, taken from the first numbered list in SKILL.md.

1. 1lake build succeeds.
2. 2Every apis[] entry in manifest.json has its abbrev + def . with a real translated reference body inside the code marker in the right Impl…
3. 3Every external lib used by the source has an opaque (and optional axiom) in global_aux, with a @review human annotation.
4. 4Spec/.lean files exist as scaffolds — import .Harness + module docstring + DO NOT MODIFY notice; they will be filled by spec_write.
5. 5Test.lean has #guards for every doctest found in source (or @review human notes for the curator if absent).

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 nothing: there is no allowed-tools line, so your agent's usual permission prompts apply.

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

  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 Source Python loads about 1.9k tokens when it runs. Until then it costs about 93 tokens; SKILL.md has 703 words of instructions outside code blocks.

Always · name and description, kept in context so the agent knows when to use it

~93

When it runs · the whole SKILL.md, loaded when a task matches

~1.9k

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

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). 703 words, ~1,936 tokens.

name

vero-source-python

description

Load BEFORE translating Python source to Lean 4. Provides Python-specific classification rules, type mappings, stdlib-opaque modeling guidance, and patterns for mapping Python constructs into the ratified bundle paradigm (Impl/ + Spec/ + Bundle + Harness). Pair with vero-discover, vero-plan, vero-translate, vero-spec-write, and vero-python-pitfalls.

-- !benchmark @start global_aux
/-- Opaque model of `math.sqrt`. The benchmark does not constrain the
    return value beyond non-negativity; downstream specs encode the
    minimum needed (e.g., square root of n is ≤ n).

    @review human: confirm this opaque model is sufficient for the
    intended specs. -/
opaque sqrt : Int → Int

axiom sqrt_nonneg : ∀ n, 0 ≤ sqrt n  -- only if a spec actually needs it
-- !benchmark @end global_aux

src/foo.py
  ↓
<Project>/Impl/Foo.lean    -- types + APIs, with translated reference impls in code markers
<Project>/Spec/Foo.lean    -- empty until spec_write fills
manifest.json -> packages[0].modules[?] = { name=Foo, impl=..., spec=..., apis=[...] }

-- File header / imports
-- !benchmark @start imports
import <Project>.Bundle
-- !benchmark @end imports

-- Module docstring (curator-written, frozen)
/-! # <Project>.Impl.<ModuleName>

<one-paragraph summary of the module's purpose, ported from the
Python module docstring + reading the source>
-/

namespace <Project>

-- Types (curator-given, frozen — no markers around individual types)
structure Foo where ...
deriving Repr, BEq

-- Sig abbrevs (one per API, listed in manifest)
abbrev BarSig := Int → Foo → Foo
abbrev BazSig := Foo → Bool

-- Opaque external models + their axioms (if needed)
-- !benchmark @start global_aux
opaque sqrt : Int → Int
-- !benchmark @end global_aux

-- APIs — one !benchmark code pair per api; body is the translated reference implementation
-- !benchmark @start code_aux def=bar
-- !benchmark @end code_aux def=bar
-- !benchmark @start code def=bar
def <Project>.bar : <Project>.BarSig :=
  -- translated Python body, not `sorry`
  ...
-- !benchmark @end code def=bar

end <Project>

def factor(n: int) -> int:
    """
    >>> factor(9)
    3
    """
    ...

/-- doctest: factor(9) -> 3 -/
#guard <Project>.factor 9 == 3

© 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-source-python of sunblaze-ucb/vero.

Open the folder on GitHubat commit 0a7325d