Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx agentmods add skills/leanprover/lean-beam/rocq-beamnpx skills add leanprover/lean-beam --skill rocq-beamgit clone --depth 1 https://github.com/leanprover/lean-beamWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/leanprover/lean-beam/rocq-beam)<a href="https://agentmods.dev/skills/leanprover/lean-beam/rocq-beam"><img src="https://agentmods.dev/badge/skills/leanprover/lean-beam/rocq-beam.svg" alt="Measured on agentmods" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5 | $0.00038 | $0.02446 |
| Opus 5 | $0.00019 | $0.01223 |
| Sonnet 5 | $0.00008 | $0.00489 |
| Haiku 4.5 | $0.00004 | $0.00245 |
Grade A, and why
rocq-beam scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 4d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 242 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Rocq Beam
Use this skill when a Rocq project needs the narrow Rocq-facing surface that lean-beam already exposes, especially while porting Rocq developments to Lean. This is an optional auxiliary mode of the lean-beam toolchain, not a separate product or a second full workflow stack.
The goal is cheap Rocq proof-state inspection through coq-lsp, without turning Rocq support into a broad standalone interface.
Do not use coqtop or any fallback executor. Only coq-lsp is trusted.
This is the Rocq-only skill. It should stay focused on Rocq and should not require Lean-specific
workflow guidance. Do not factor shared Lean/Rocq skill instructions into a common helper;
duplicate short guidance if both skills need it.
Setup
From the lean-beam repo root:
./scripts/install-beam.sh --codex --rocq-skill
Use --claude --rocq-skill, --pi --rocq-skill, --opencode --rocq-skill, or
--vibe --rocq-skill instead when installing for Claude Code, Pi Agent, OpenCode, or Mistral Vibe.
Use --all-skills --rocq-skill when you want every supported agent skill target.
The installer puts lean-beam in ~/.local/bin, stages the self-contained runtime under
BEAM_INSTALL_ROOT (default ~/.local/share/beam), and installs the optional Rocq skill only when
--rocq-skill is paired with a selected agent skill target.
Restart active agent sessions after installation.
The user-facing setup and installer reference is docs/SETUP.md. The Rocq status and setup page is docs/ROCQ.md.
Rocq Setup
Rocq-specific setup:
cd /path/to/lean-beam
bash tests/setup-rocq-opam.sh
Skill Surface
This skill documents the current Rocq-facing lean-beam workflow surface. Keep the surface narrow:
the current wrapper is for goal inspection against saved files, not for hidden proof-session
mutation.
Supported command families:
- start and own a Rocq wrapper session:
lean-beam serve rocq - inspect the selected session state:
lean-beam status - inspect goals after an existing sentence:
lean-beam rocq-goals-after - inspect goals before a sentence or after speculative sentence text within that basis:
lean-beam rocq-goals-prev - inspect tracked files and daemon state:
lean-beam open-files,lean-beam stats,lean-beam reset-stats
What ships with it
1 file beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 4d ago First seen · 242 lines · 38 tokens per session scan A 5eb229611e93
rocq-beam is a skill published in the GitHub repository leanprover/lean-beam (24 stars, last pushed 4d ago), licensed Apache-2.0. It adds 38 tokens to every session and 2,446 once invoked, about $0.0002 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other skills, from other repositories
exploratory-data-analysis
Perform bounded, local exploratory analysis of explicitly supported scientific files. Use for redacted CSV/TSV/JSON profiles; optional NumPy, HDF5, FASTA/FASTQ, and basic image metadata inspection; missingness/leakage audits; outlier and transformation sensitivity; and rigorous EDA report scaffolds. Other domain…
evaluating-with-leakage-gates
Evaluate an OpenMed de-identification or clinical NER model against the leakage-first release gates G1a through G8, which gate releases on residual PHI leakage rather than on F1. Use when the user wants to run the OpenMed eval harness on a synthetic golden set, decide whether a de-id model is RELEASABLE or…
mapping-to-snomed
Maps clinical concept spans extracted by OpenMed to SNOMED CT concepts through a USER-SUPPLIED terminology server (the user's own Ontoserver, Snowstorm, or UMLS/UTS), never a bundled vocabulary. Use when the user wants to code findings, disorders, procedures, body structures, or substances to SNOMED CT, run an ECL…
mixed-precision
Use FP16/BF16 mixed precision to accelerate training and reduce memory. Use when optimizing GPU performance.
tooluniverse-drug-research
Comprehensive drug profiling — mechanism, primary/secondary targets, drug interactions, clinical-trial status, adverse events (FAERS), pharmacogenomics, and approval history. Use for full drug investigation reports, 'tell me about drug X' queries, and assembling drug profiles for clinicians, researchers, or regulatory…
audit-scientific-figure
Review and score an existing scientific illustration in visible draw.io, Microsoft PowerPoint, or WPS Presentation without hiding defects through flattening. Use for reference-fidelity checks, layout cleanup, connector review, text-fit checks, deep editability and raster-atomicity inspection, local-region gates, or…