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/notationgit clone --depth 1 https://github.com/Verified-zkEVM/VCVioWhat 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.01559 |
| Opus 5 | $0.00000 | $0.00779 |
| Sonnet 5 | $0.00000 | $0.00312 |
| Haiku 4.5 | $0.00000 | $0.00156 |
Grade A, and why
notation 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 3d 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 — 86 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Notation Reference
OracleSpec Notations
| Notation | Meaning | Defined in |
|---|---|---|
A →ₒ B |
Singleton oracle spec (OracleSpec.ofFn) |
VCVio/OracleComp/OracleSpec.lean |
[]ₒ |
Empty oracle spec (emptySpec) |
VCVio/OracleComp/OracleSpec.lean |
spec₁ + spec₂ |
PFunctor coproduct (dependent Sum.rec) |
VCVio/OracleComp/OracleSpec.lean |
⊂ₒ |
SubSpec relation | VCVio/OracleComp/Coercions/SubSpec.lean |
∘ₛ |
QueryImpl composition | VCVio/OracleComp/SimSemantics/QueryImpl/Constructions.lean |
Probability Notations
| Notation | Meaning | Defined in |
|---|---|---|
𝒟[mx] |
primary Measure denotation, evalDist mx |
VCVio/EvalDist/Defs/Measure.lean |
𝒮[mx] |
explicit finite adapter, evalSPMF mx |
VCVio/EvalDist/Defs/Basic.lean |
Pr[= x | mx] |
probOutput mx x |
VCVio/EvalDist/Defs/Basic.lean |
Pr[p | mx] |
probEvent mx p |
VCVio/EvalDist/Defs/Basic.lean |
Pr[⊥ | mx] |
probFailure mx |
VCVio/EvalDist/Defs/Basic.lean |
Pr[cond | var ← src] |
probEvent src (fun var => cond) |
VCVio/EvalDist/Defs/Basic.lean |
NOTE: Legacy code and comments may still use the old [= x | comp] notation (without Pr prefix). Always use Pr[...] in new code.
Pr[...] is a discrete compatibility notation. Use probOutput_eq_evalDist,
probEvent_eq_evalDist, or probFailure_eq_evalDist to move a scalar statement to 𝒟[...].
Sampling Notations
| Notation | Meaning | Defined in |
|---|---|---|
$ᵗ T |
uniformSample T (type-level uniform) |
VCVio/OracleComp/Constructions/SampleableType.lean |
$ xs |
uniformSelect xs (can fail on empty) |
VCVio/OracleComp/ProbComp.lean |
$! xs |
uniformSelect! xs (never fails) |
VCVio/OracleComp/ProbComp.lean |
$[0..n] |
uniformFin n (uniform Fin (n+1)) |
VCVio/OracleComp/ProbComp.lean |
$[n⋯m] |
uniformRange n m (uniform over range) |
VCVio/OracleComp/ProbComp.lean |
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.
- 3d ago First seen · 86 lines · 0 tokens per session scan A bf7dd57ef277
notation is an agent published in the GitHub repository Verified-zkEVM/VCVio (142 stars, last pushed 4d ago), licensed Apache-2.0. It costs nothing until one of its globs matches a file; then it loads 1,559 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.
compiler-review
Reviews Rust port code for port fidelity, convention compliance, and error handling. Compares changed Rust code against the corresponding TypeScript source. Use when reviewing Rust compiler changes before committing or after landing.