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/interopgit 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/interop)<a href="https://agentmods.dev/agents/verified-zkevm/vcvio/interop"><img src="https://agentmods.dev/badge/agents/verified-zkevm/vcvio/interop.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.02764 |
| Opus 5 | $0.00000 | $0.01382 |
| Sonnet 5 | $0.00000 | $0.00553 |
| Haiku 4.5 | $0.00000 | $0.00276 |
Grade A, and why
interop 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 — 210 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Interop with Rust verification frontends (hax, aeneas)
Interop/ is an experimental sibling to LatticeCrypto/ whose job is to
let VCVio reason about Lean code emitted by Rust verification frontends:
- hax: MIR → Lean/F*/Coq/EasyCrypt/ProVerif/SSProve via a 35-phase OCaml engine. Lean target produces code in the
Hax.RustM := ExceptT Error Optionmonad. - aeneas: MIR → Lean/Coq/F* via Charon's LLBC + functional translation. Lean target produces code in an inductive
Aeneas.Std.Result α := ok | fail | div.
Current baseline (Lean 4.33): both integrations are dormant and the
aggregate Interop target is excluded from CI. Hax is not yet Lean
4.33-compatible. Aeneas publishes a Lean 4.31 build, so its VCVio bridge must
be ported and revalidated independently before being enabled.
Both backends collapse panic + divergence into the same shape; VCVio adds
oracle access on top. The framework-side target monad is
Interop.Rust.RustOracleComp.
TCB Isolation Contract
This is the headline guarantee: adding Interop/ does not increase the
trusted computing base (TCB) of core VCVio.
Rust verification frontends drag in a sizeable trusted layer (extraction
engine, Charon's LLBC frontend, the backend's own runtime axioms), and we
never want a routine lake build of the core framework to inherit that.
The contract is therefore enforced at three levels:
- Lake:
Interopis its ownlean_libinlakefile.lean, sibling toLatticeCrypto/Examples. Cross-library imports are physical. - CI:
scripts/check-interop-isolation.shgreps for forbidden imports..github/workflows/interop-isolation.ymlruns it on every PR and on pushes tomain. The script also runs without a Lean toolchain, so it is fast and never blocks on Mathlib cache or build flakiness. - Reverse direction:
Interop/**may import fromVCVio/**,ToMathlib/**,Hax.…, andAeneas.…, but not fromLatticeCrypto/**,Examples/**,LatticeCryptoTest/**,Extern/**,VCVioWidgets/**, orVCVioTest/**. Those libraries are themselves clients of VCVio, so Interop depending on them would create circular layering and pull user-facing libraries into the Interop TCB.
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 · 210 lines · 0 tokens per session scan A 4944ee122730
interop is an agent published in the GitHub repository Verified-zkEVM/VCVio (142 stars, last pushed 5d ago), licensed Apache-2.0. It costs nothing until one of its globs matches a file; then it loads 2,764 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.
speckit.checklist
Generate a custom checklist for the current feature based on user requirements.