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/interactiongit 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.01307 |
| Opus 5 | $0.00000 | $0.00654 |
| Sonnet 5 | $0.00000 | $0.00261 |
| Haiku 4.5 | $0.00000 | $0.00131 |
Grade A, and why
interaction 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 — 112 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Interaction Integration
VCVio depends on PolyFun for the generic interaction framework. Do not duplicate PolyFun's interaction guide here. Use this page for VCV-specific runtime, computational, and example integration only.
Source of Truth
Generic protocol theory lives in PolyFun:
- Sequential specs, transcripts, decorations, strategies, append, replicate, and state chains:
PolyFun.Interaction.Basic.* - Two-party, multiparty, and concurrent interaction layers:
PolyFun.Interaction.TwoParty.*,PolyFun.Interaction.Multiparty.*,PolyFun.Interaction.Concurrent.* - Generic UC interfaces, open processes, structural boundary traces, open theory, notation, environment actions, and leakage scaffolding:
PolyFun.Interaction.UC.*
For conceptual background, read PolyFun's docs/wiki/interaction.md and the module docstrings in the PolyFun dependency.
VCVio should only document how those generic APIs are instantiated with probabilistic semantics, oracle computations, and crypto examples.
VCV-Specific Layers
VCVio retains the computational and runtime interpretation of PolyFun's generic UC layer:
| File | Purpose |
|---|---|
VCVio/Interaction/UC/Computational.lean |
Computational observation layer for UC-style emulation using subprobability measures and total variation distance. |
VCVio/Interaction/UC/Runtime.lean |
Synchronous runtime semantics for closed open processes, including processSemantics, processSemanticsProbComp, and processSemanticsOracle. |
VCVio/Interaction/UC/AsyncRuntime.lean |
Asynchronous runtime semantics with process ticks and environment events. |
VCVio/Interaction/UC/AsyncSecurity.lean |
Fair-PPT security wrappers for asynchronous env-open executions. |
VCVio/Interaction/UC/Standard.lean |
Standard VCVio UC imports and conveniences. |
VCVio/Interaction/UC/StdDoBridge.lean |
Bridges from VCVio program-logic/Std.Do idioms into the UC runtime layer. |
These files may import PolyFun interaction modules.
Generic interaction modules should not be reintroduced under VCVio/Interaction or ToMathlib.
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 · 112 lines · 0 tokens per session scan A 813958646763
interaction 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,307 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.
AGENT_STRATEGIC_MEETING_PROTOCOL_v4.0
Quantum Shield Project - Strategic Decision Framework.