Instructions file CodexOpenCode
Instructions for Verified-zkEVM/clean, covering agents.md - ai agent context for clean, what is clean?, project structure, core concepts and the circuit monad.
180 3d ago A 3,447 tokens
original MIT
Instructions file
Instructions for Verified-zkEVM/clean, a project described as: Lean circuit DSL.
180 3d ago A 3 tokens
copy · 100% MIT
lean-mcp
03Skill Claude CodeCodex
This skill enables interactive inspection of Lean proof states using the Lean Language Server Protocol via mcporter.
180 3d ago A 0 tokens
original MIT
Instructions file CodexOpenCode
Instructions for Verified-zkEVM/VCVio, covering vcvio — ai agent guide, fast start, attribution, headers, and docstrings, module scopes and what this project is.
142 3d ago A 5,618 tokens
original Apache-2.0
Instructions file
Instructions for Verified-zkEVM/VCVio, a project described as: A Lean library for machine-checked cryptographic proofs.
142 3d ago A 3 tokens
copy · 100% Apache-2.0
crypto
06Agent
For the LatticeCrypto/ directory layout, scheme entry points, and proof-vs-concrete split, see docs/agents/lattice.md.
142 3d ago A 0 tokens
original Apache-2.0
Agent
This page collects compact examples that show how the cryptographic framework layers compose on concrete schemes.
142 3d ago A 0 tokens
original Apache-2.0
gotchas
08Agent
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…
142 3d ago A 0 tokens
original Apache-2.0
interaction
09Agent
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.
142 3d ago A 0 tokens
original Apache-2.0
interop
10Agent
Interop/ is an experimental sibling to LatticeCrypto/ whose job is to let VCVio reason about Lean code emitted by Rust verification frontends.
142 3d ago A 0 tokens
original Apache-2.0
lattice
11Agent
The lattice stack is split into five layers.
142 3d ago A 0 tokens
original Apache-2.0
Agent
This guide records the intended long-term boundary between PolyFun and VCVio under Lean's module system. It is the decision record for visibility, import all, and the OracleComp/PFunctor.FreeM relationship.
142 3d ago A 0 tokens
original Apache-2.0
notation
13Agent
NOTE: Legacy code and comments may still use the old [= x | comp] notation (without Pr prefix). Always use Pr[...] in new code.
142 3d ago A 0 tokens
original Apache-2.0
oracle-comp
14Agent
An oracle specification maps index types to response types.
142 3d ago A 0 tokens
original Apache-2.0
probability
15Agent
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.
142 3d ago A 0 tokens
original Apache-2.0
Agent
VCVio.ProgramLogic.Tactics.Relational; the umbrella import is still the intended default.
142 3d ago A 0 tokens
original Apache-2.0
Agent
Agent "proof-workflows" from Verified-zkEVM/VCVio, covering proof workflows, proof strategy decision tree, monadic normalization with monadnorm, game-hopping recipe and step 1: state the security theorem.
142 3d ago A 0 tokens
original Apache-2.0
Agent
This guide explains the query-tracking stack in VCVio/OracleComp/QueryTracking/.
142 3d ago A 0 tokens
original Apache-2.0
Instructions file CodexOpenCode
Instructions for Verified-zkEVM/evm-asm, covering ai agent guide for evmasm, what this project is (and where it's going), start here, build system and artifact-cache mode (lakeartifactcache=true).
54 2d ago A 12,406 tokens
original MIT
Instructions file
Instructions for Verified-zkEVM/evm-asm, covering claude.md, plan.md maintenance, proof-first (dcode) ports, proof conventions and module system.
54 2d ago A 1,306 tokens
original MIT
Agent
Measurement boundary (2026-08-11, origin/main at b068e565a). The current planning denominator is 973 definitions across 365 source files under Programs/ and Dispatch.lean, enumerated by python3 scripts/asmtoprogram.py coverage and its generated docs/4ch8f-asm-to-program-coverage.md report: 406 ALREADY-STRUCTURED, 140…
54 2d ago A 0 tokens
original MIT
Agent
Registry of unverified EvmAsm/Codegen/Programs/ modules that still define RISC-V assembly-string probes but are linked into no zisk BuildUnit, so they are deadweight a future PR can git rm. The list is generated and reproducible by committed scripts/scandeadprobes.py (re-run it to refresh); entries are cross-checked…
54 2d ago A 0 tokens
original MIT
Agent
Status: phase-2 design drafted; implementation is held for maintainer review. Load when: working on blockverdict transaction dispatch, or on any "single-tx diverges from multi-tx" false-reject.
54 2d ago A 0 tokens
original MIT
Agent
Moved out of AGENTS.md to keep the agent guide compact. Load this when.
54 2d ago A 0 tokens
original MIT