Agent
Scope audit for evm-asm-n9rtz, against execution-specs bd8c673 ([email protected]). The baseline is [email protected] (a0c182656). This is a classification document, not a porting claim.
54 2d ago A 0 tokens
original MIT
Agent
This note is for changes to statelessguest, the EEST converter, and any RISC-V code that reads the stateless payload. The invariant is simple: the zkVM guest must consume the same stateless input content as execution-specs runstatelessguest.
54 2d ago A 0 tokens
original MIT
tactics-deep
51Agent
Moved out of AGENTS.md to keep the agent guide compact. Load this when.
54 2d ago A 0 tokens
original MIT
Agent
The single page that says what remains to prove for the north-star theorem and where each piece plugs in. Keep it updated whenever an obligation changes status (same discipline as PLAN.md).
54 2d ago A 0 tokens
original MIT
Agent
Working notes for bead evm-asm-0w05f.9 (GH #10207). The emitted guest's LIVE verdict path is statelessGuestUnit → statelessGuestEpilogue → statelessverdictv2 (statelessVerdictV2GuestClosure, BlockVerdictV2.lean:217-528) + the runtime dispatcher; anything not in that closure is a probe.
54 2d ago A 0 tokens
original MIT
Agent
Scoping document for bead evm-asm-0w05f (GH #10207): migrate the whole stack from [email protected] (execution-specs bd8c673) to [email protected] (execution-specs 40f956fab76463e113cb7f0dda4a8a263a1ee776, published 2026-07-10). SpecRef reached full-suite v0.5.0 conformance (25,477 fixtures, succ FAIL 0)…
54 2d ago A 0 tokens
original MIT
Agent
The high-level decision guide for any bead of the shape "verify " or "swap for a verified implementation". The mechanics (class table, scaffold, VC closers, deploy gates) live in port-playbook.md — read that when you start typing. Read THIS page when you are deciding what to prove, against what interface, and what to…
54 2d ago A 0 tokens
original MIT
Agent
Status: FALSE ACCEPT CONFIRMED (diagnostic only; no guest behavior change).
54 2d ago A 0 tokens
original MIT
wp-framework
57Agent
This guide explains the Rv64 weakest-precondition layer added under EvmAsm/Rv64/WP/. It is meant for proof authors who already know the separation-logic cpsTripleWithin style, but have not used the WP certificate mechanism before.
54 2d ago A 0 tokens
original MIT
Instructions file CodexOpenCode
Instructions for Verified-zkEVM/CompPoly, covering comppoly ai agent guide, fast start, where to work, guardrails and deeper docs.
47 4d ago A 1,775 tokens
original Apache-2.0
Instructions file
Instructions for Verified-zkEVM/CompPoly, a project described as: Computable Polynomials in Lean.
47 4d ago A 3 tokens
copy · 100% Apache-2.0