Issues

• Initialization transcription: contract creation and internal String helpers unsupported at 600014d5

  lfglabs-dev/verity#2465 · Filter by author Th0rgal opened on Sep 30, 2026

• G23: public state-variable getters cannot be hop targets (StorageSlot vs hopCallView)

  bug
  lfglabs-dev/verity#2439 · Filter by author Th0rgal opened on Sep 23, 2026

• #check_contract: fail-closed CEI treats every internal helper call as an interaction and a write, so faithful Solidity bodies need allow_post_interaction_writes almost everywhere (Pareto G22)

  lfglabs-dev/verity#2435 · Filter by author Th0rgal opened on Sep 19, 2026

• macro/#check_contract: let _ ← f lowers to a __discard local that the compiler's reserved-prefix check rejects (Pareto G21)

  lfglabs-dev/verity#2434 · Filter by author Th0rgal opened on Sep 19, 2026

• macro: zero-argument context-taking helper called as a bare statement is not threaded (Pareto G20)

  lfglabs-dev/verity#2431 · Filter by author Th0rgal opened on Sep 19, 2026

• verity_contract bodies hit a Lean 4.31 do-notation elaboration failure (name-dependent) with mutable reassignments interleaved with binds

  lfglabs-dev/verity#2427 · Filter by author Th0rgal opened on Sep 18, 2026

• Typed interface calls cannot return multiple values

  lfglabs-dev/verity#2424 · Filter by author Th0rgal opened on Sep 18, 2026
  1

• Ergonomics: Contracts namespace clashes, reserved identifiers (from/to/this), reserved ERC-20 helper names, callee-first ordering

  lfglabs-dev/verity#2423 · Filter by author Th0rgal opened on Sep 18, 2026

• Auto view-frame proof fails on require/revert and static calls, forcing view markers to be dropped

  lfglabs-dev/verity#2422 · Filter by author Th0rgal opened on Sep 18, 2026

• Statement/expression forms rejected in verity_contract bodies: if-without-else, mutable monadic rebinds, Int256/Bool ternaries, Bool negation

  lfglabs-dev/verity#2421 · Filter by author Th0rgal opened on Sep 18, 2026

• Absolute parent slots and diamond rejection prevent reusing OZ upgradeable parents across inheritance chains

  lfglabs-dev/verity#2420 · Filter by author Th0rgal opened on Sep 18, 2026

• override bodies are elaborated at the parent's position (cannot use child helpers); no super.f(args)

  lfglabs-dev/verity#2419 · Filter by author Th0rgal opened on Sep 18, 2026

• Interface-typed storage fields are rejected (design note promises them); no address-to-interface cast for storage-held callees

  lfglabs-dev/verity#2418 · Filter by author Th0rgal opened on Sep 18, 2026

• Storage: Bool/Uint8/Bytes32 scalars, packed bool/address slots and FixedArray Uint256 gaps cannot be declared (solc layout parity)

  lfglabs-dev/verity#2417 · Filter by author Th0rgal opened on Sep 18, 2026

• EVMYulLean fork conformance probe failed

  lfglabs-dev/verity#2359 · Filter by author github-actions opened on Aug 17, 2026

• Macro-emit reentrancy adversary holes and entrypoint registry (single-source rely-guarantee models)

  enhancementleanP1: core language
  lfglabs-dev/verity#2094 · Filter by author Th0rgal opened on Jul 3, 2026

• proof(L2): Tier 4 — external calls & low-level mechanics (call frames, returndata, ECM)

  P3: deferredproof
  lfglabs-dev/verity#2084 · Filter by author Th0rgal opened on Jul 2, 2026

• proof(L2): Tier 3 — effects & observables (ABI encoding correctness; emit, typed reverts, returns)

  P2: importantproof
  lfglabs-dev/verity#2082 · Filter by author Th0rgal opened on Jul 2, 2026
  1

• Track EntryPoint feature PRs needed for ERC-4337 Verity parity

  lfglabs-dev/verity#2071 · Filter by author Th0rgal opened on Jun 28, 2026

• feat(codegen): emit solc-shaped ABI, allocation, arithmetic, and library Yul helpers

  lfglabs-dev/verity#2059 · Filter by author Th0rgal opened on Jun 24, 2026

• feat(codegen): solc-shaped internal helper outlining for Yul identity targets

  lfglabs-dev/verity#2058 · Filter by author Th0rgal opened on Jun 24, 2026

• feat(CodeData): typed byte-layout proof surface for CREATE2/SSTORE2 code-as-storage

  lfglabs-dev/verity#2023 · Filter by author Th0rgal opened on Jun 13, 2026

• feat(Patterns): typed EIP-712 / ecrecover signature-flow pattern

  blocks:erc4337blocks:morphoenhancementP3: deferred
  lfglabs-dev/verity#2002 · Filter by author Th0rgal opened on Jun 12, 2026

• feat(Events): broaden source-shaped emit surface (dynamic/struct event args)

  enhancement
  lfglabs-dev/verity#2000 · Filter by author Th0rgal opened on Jun 12, 2026
  2

• feat(Semantics): first-class multicall + delegatecall frame semantics (bytes[] iteration)

  enhancement
  lfglabs-dev/verity#1997 · Filter by author Th0rgal opened on Jun 12, 2026