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 agents/verified-zkevm/vcvio/gotchasgit clone --depth 1 https://github.com/Verified-zkEVM/VCVioWrote 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/agents/verified-zkevm/vcvio/gotchas)<a href="https://agentmods.dev/agents/verified-zkevm/vcvio/gotchas"><img src="https://agentmods.dev/badge/agents/verified-zkevm/vcvio/gotchas.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.00000 | $0.05702 |
| Opus 5 | $0.00000 | $0.02851 |
| Sonnet 5 | $0.00000 | $0.01140 |
| Haiku 4.5 | $0.00000 | $0.00570 |
Grade A, and why
gotchas 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 5d 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 — 384 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Gotchas and Troubleshooting
Critical (Will Bite You Immediately)
1. Probability semantics require the right spec class
Any file using evalSPMF, probOutput, probEvent, or Pr[...] on OracleComp spec needs [IsProbabilitySpec spec]. evalDist / 𝒟[…] also needs a MeasurableSpace on the result type. Lemmas that use uniform cardinalities, PMF.uniformOfFintype, or connect support to nonzero probability need [IsUniformSpec spec]. Plain support works on arbitrary OracleComp spec.
Symptom: "failed to synthesize instance" mentioning MonadLiftT (OracleComp spec) SPMF, IsProbabilitySpec, IsUniformSpec, or EvalDistCompatible.
Fix: Add [IsProbabilitySpec spec] for arbitrary per-query probability semantics, or [IsUniformSpec spec] for uniform oracle semantics. If you already have [spec.Fintype] [spec.Inhabited] and want uniform sampling, install a local instance with IsUniformSpec.ofFintypeInhabited spec.
2. autoImplicit = false is set globally in lakefile.lean
Every variable must be explicitly declared. Do not rely on Lean's auto-implicit mechanism,
and do not add set_option autoImplicit false in individual files.
Symptom: "unknown identifier" for variables you expected Lean to infer.
3. evalSPMF is simulateQ; evalDist is measure-valued
evalSPMF is simulateQ with m = PMF and the IsProbabilitySpec.toPMF query implementation. Under [IsUniformSpec spec], those query distributions are propositionally the uniform distributions. The evalSPMF_eq_simulateQ identity is definitional (rfl). The primary evalDist is the successful-output measure façade; on discrete free programs it agrees with the direct FreeM.denote fold.
4. ++ₒ is dead — use +
The README and large amounts of commented-out code use ++ₒ for combining oracle specs. The current API uses standard + (HAdd).
5. Delete obsolete commented-out code
Do not keep large commented-out Lean blocks around as reference material,
especially if they use obsolete patterns ([= x | ...], ++ₒ, simulate',
getM, guard via Alternative). Delete them instead. This is distinct from
unfinished live proof attempts, which should be preserved with stop.
Use Examples/OneTimePad/Basic.lean as the canonical reference for current style.
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.
- 5d ago First seen · 384 lines · 0 tokens per session scan A b39bcbc30fc0
gotchas is an agent published in the GitHub repository Verified-zkEVM/VCVio (144 stars, last pushed yesterday), licensed Apache-2.0. It costs nothing until one of its globs matches a file; then it loads 5,702 tokens. 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 agents, from other repositories
acto-critic
ACToR-style discriminator for the Thermite toolchain. Hunts for divergence between the toolchain's behavior and its authority (the design doc + the conformance corpus + Verus/Kani golden files). ALWAYS writes a FAILING test that pins down the divergence — NEVER writes a fix. Dispatch when a builder/fixer declares…
acto-builder
Multi-file authorized agent for shipping missing Thermite-toolchain infrastructure that exceeds acto-fixer's single-file scope — a whole component a design doc calls for that does not yet exist (a parser module + its AST consumers; the combinator registry + its lowering hooks; the forge check pipeline + its JSON…
acto-doc-author
Authors design docs under .design/ / .md that ADAPT to existing Thermite-toolchain code and the thermite-design.md thesis. Each REQ status table is grounded in quoted-code evidence from the current implementation. REQs are classified BINARY — SHIPPED (end-to-end functional with a non-test production consumer + tests +…
acto-fixer
Applies the MINIMAL fix for exactly ONE pinned divergence found by acto-critic. The failing test pins the divergence; the fix makes that test pass. Never bundles multiple fixes. Never refactors adjacent code. Single-file scope (escalate to acto-builder if the fix spans files). After the fix, runs the full gauntlet and…
Tenable Cloud Exposure PQC Posture Portal
Self-hosted web portal showing post-quantum cryptography readiness for cloud resources using Tenable Cloud Exposure's native SSL/TLS PQC telemetry.
encryption-standards-checker
Data encryption and cryptographic standards specialist.