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/probabilitygit 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/probability)<a href="https://agentmods.dev/agents/verified-zkevm/vcvio/probability"><img src="https://agentmods.dev/badge/agents/verified-zkevm/vcvio/probability.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.06961 |
| Opus 5 | $0.00000 | $0.03481 |
| Sonnet 5 | $0.00000 | $0.01392 |
| Haiku 4.5 | $0.00000 | $0.00696 |
Grade A, and why
probability 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 — 360 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Probability Reasoning (EvalDist and ProbComp)
For the cross-project survey of SPMF, Mathlib measures and kernels, PolyFun
coalgebraic limits, ArkLib, Bluebell/Iris, and possible long-term migration paths, see
Probability Semantics for Computations: Landscape and Design Options.
The accepted design for new work is
Denotational Probability Semantics: use
Mathlib measures for closed denotations, kernels for environment/state-indexed computations,
effect-preserving outcome types for transformers, and keep Pr[...] as the discrete compatibility
surface. docs/reading/ indexes the full design record.
The primary notation is now measure-valued: 𝒟[mx] : Measure α. The former finite distribution
API is explicit as evalSPMF mx / 𝒮[mx]. Pr[...] remains the discrete compatibility façade;
theorems probOutput_eq_evalSPMF_toMeasure, probEvent_eq_evalSPMF_toMeasure, and
probFailure_eq_evalSPMF_toMeasure state its meaning through the explicit compatibility measure.
Direct FreeM measure semantics has corresponding FreeM.evalDist_apply_singleton and
FreeM.evalDist_apply_setOf coherence lemmas. This split is intentional. An unconditional
Eq.rec law for Pr[...] only needs equality of result types in the discrete façade, whereas a
measure denotation also depends on the selected MeasurableSpace; type equality does not identify
those structures. We therefore do not install a blanket finite-type measurable-space instance.
evalDist_eq_evalSPMF_toMeasure is the sole deprecated whole-denotation bridge. It applies to the
canonical compatibility adapter; measure-native semantics should remain on 𝒟[…] instead of
round-tripping through the finite backend.
Core Definitions
| Definition | Type | Notation | Defined in |
|---|---|---|---|
evalDist mx |
Measure α |
𝒟[mx] |
EvalDist/Defs/Measure.lean |
evalSPMF mx |
SPMF α |
𝒮[mx] |
EvalDist/Defs/Basic.lean |
probOutput mx x |
ℝ≥0∞ |
Pr[= x | mx] |
EvalDist/Defs/Basic.lean |
probEvent mx p |
ℝ≥0∞ |
Pr[p | mx] |
EvalDist/Defs/Basic.lean |
probFailure mx |
ℝ≥0∞ |
Pr[⊥ | mx] |
EvalDist/Defs/Basic.lean |
support mx |
Set α |
— | EvalDist/Defs/Support.lean |
finSupport mx |
Finset α |
— | EvalDist/Defs/Support.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 · 360 lines · 0 tokens per session scan A 244f5608b015
probability 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 6,961 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
glm-math-director
Stage 4 of the GLM chain. Solves the homework and physics numbers with strict unit checks, verifies LaTeX decomposes correctly, and assigns color identities to symbols. Sandbox when available on the platform; otherwise state derivation in checks.
grok-math-director
Stage 4 of the Grok chain. Must use codeinterpreter to solve homework and physics numbers, check units, and verify LaTeX. websearch only for cited constants.
astrobiologist
Reasons from habitability, redox disequilibrium, and Bayesian biosignature frameworks through Mars (Perseverance, Viking perchlorate lessons), Europa Clipper ocean worlds, agnostic signatures and the Ladder of Life Detection, while treating abiotic mimics, preservation, and LUCA phylogenomics as constraints—not…
citizen-entomologist
Curiosity-driven insect guide that celebrates discovery, uses common names alongside scientific names, and channels observations into citizen science platforms like iNaturalist and BugGuide.
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…