-
Notifications
You must be signed in to change notification settings - Fork 18
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
Macro-emit reentrancy adversary holes and entrypoint registry (single-source rely-guarantee models)
enhancementNew feature or requestNew feature or requestleanLean 4 codeLean 4 codeP1: core languageBlocks writing common contractsBlocks writing common contractsStatus: Open.#2094 In lfglabs-dev/verity;Roadmap status — week of 2026-06-29 (report 1)
documentationImprovements or additions to documentationImprovements or additions to documentationStatus: Open.#2089 In lfglabs-dev/verity;feat(EDSL): enum support (uint8-backed with range checks)
blocks:erc4337Blocks ERC-4337 EntryPoint parity/verificationBlocks ERC-4337 EntryPoint parity/verificationblocks:lidoBlocks Lido StakingRouter parity/verificationBlocks Lido StakingRouter parity/verificationenhancementNew feature or requestNew feature or requestP1: core languageBlocks writing common contractsBlocks writing common contractsStatus: Open.#2088 In lfglabs-dev/verity;feat(EDSL): first-class modifiers, inheritance (is X, Y), and virtual/override
blocks:erc4337Blocks ERC-4337 EntryPoint parity/verificationBlocks ERC-4337 EntryPoint parity/verificationblocks:lidoBlocks Lido StakingRouter parity/verificationBlocks Lido StakingRouter parity/verificationblocks:morphoBlocks Morpho Blue parity/verificationBlocks Morpho Blue parity/verificationenhancementNew feature or requestNew feature or requestP1: core languageBlocks writing common contractsBlocks writing common contractsStatus: Open.#2087 In lfglabs-dev/verity;feat(EDSL): narrow integer and fixed-bytes types (uint8–uint248, intN, bytes1–bytes31)
blocks:erc4337Blocks ERC-4337 EntryPoint parity/verificationBlocks ERC-4337 EntryPoint parity/verificationblocks:lidoBlocks Lido StakingRouter parity/verificationBlocks Lido StakingRouter parity/verificationblocks:morphoBlocks Morpho Blue parity/verificationBlocks Morpho Blue parity/verificationenhancementNew feature or requestNew feature or requestP1: core languageBlocks writing common contractsBlocks writing common contractsStatus: Open.#2086 In lfglabs-dev/verity;proof(L2): Tier 6 — external parameter/return profile widening (bytes, string, arrays, tuples, multi-returns)
P3: deferredBuilds on P0-P2 workBuilds on P0-P2 workproofLean proof workLean proof workStatus: Open.#2085 In lfglabs-dev/verity;proof(L2): Tier 4 — external calls & low-level mechanics (call frames, returndata, ECM)
P3: deferredBuilds on P0-P2 workBuilds on P0-P2 workproofLean proof workLean proof workStatus: Open.#2084 In lfglabs-dev/verity;proof(L2): Tier 5 — remaining core expressions (keccak256, constructorArg, calldata arrays, dynamicBytesEq)
P3: deferredBuilds on P0-P2 workBuilds on P0-P2 workproofLean proof workLean proof workStatus: Open.#2083 In lfglabs-dev/verity;proof(L2): Tier 3 — effects & observables (ABI encoding correctness; emit, typed reverts, returns)
P2: importantBlocks specific contract categoriesBlocks specific contract categoriesproofLean proof workLean proof workStatus: Open.#2082 In lfglabs-dev/verity;proof(L2): Tier 1 — storage & mapping operation preservation (mappingSlot bridge lemmas)
P2: importantBlocks specific contract categoriesBlocks specific contract categoriesproofLean proof workLean proof workStatus: Open.#2081 In lfglabs-dev/verity;proof(L2): Tier 2 — internal helper call preservation (close the 4 remaining interface goals)
P2: importantBlocks specific contract categoriesBlocks specific contract categoriesproofLean proof workLean proof workStatus: Open.#2080 In lfglabs-dev/verity;- Status: Open.#2071 In lfglabs-dev/verity;