Issues

• Remove profile_independent_agreement now that ProfileAgreement.of_flags covers it

  area: proofs
  Task

  NethermindEth/LeanCIL#277 · Filter by author benaadams opened on Oct 24, 2026

• Certify a method on several profiles from one manifest entry

  area: proofsarea: verificationconsumer: int256
  Feature

  NethermindEth/LeanCIL#276 · Filter by author benaadams opened on Oct 24, 2026

• Step through setLocal with a LocalSnapshots invariant

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#275 · Filter by author benaadams opened on Oct 24, 2026

• verify-batch shares extraction-independent support only from the first group

  area: verificationconsumer: int256
  Task

  NethermindEth/LeanCIL#271 · Filter by author benaadams opened on Oct 24, 2026

• Consumer certificate check and kernel replay up to 1.9x slower per case between 199af3d and 08a2d7c

  area: verificationconsumer: int256
  Bug

  NethermindEth/LeanCIL#270 · Filter by author benaadams opened on Oct 24, 2026

• Memory step retry needs staticInstruction passed, and the memory strategy has an unreachable branch

  area: proofs
  Task

  NethermindEth/LeanCIL#266 · Filter by author benaadams opened on Oct 24, 2026

• Feature steps unfold FeatureProfile.evaluate into a 17-arm match

  area: proofsconsumer: int256
  Task

  NethermindEth/LeanCIL#265 · Filter by author benaadams opened on Oct 24, 2026

• Supplied step facts are skipped inside a tactic have

  area: proofsconsumer: int256
  Bug

  NethermindEth/LeanCIL#263 · Filter by author benaadams opened on Oct 24, 2026

• Checked-step tactics: gaps found converting a consumer's hand-written stepping

  area: proofsconsumer: int256
  Bug

  NethermindEth/LeanCIL#252 · Filter by author benaadams opened on Oct 24, 2026

• Detect and ease consumer breakage from semantic-model changes; scope #212's opaque Vector128 locals

  area: extractorarea: proofsarea: verificationconsumer: int256
  Bug

  NethermindEth/LeanCIL#249 · Filter by author benaadams opened on Oct 24, 2026

• Forwarder contracts

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#244 · Filter by author benaadams opened on Oct 24, 2026

• Refinement modulo dead locals

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#242 · Filter by author benaadams opened on Oct 24, 2026

• SIMD lane-wise lemma library for integer intrinsics and carry/borrow cascades

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#241 · Filter by author benaadams opened on Oct 24, 2026

• ValidCall: transport lemmas, or deprecate it in favour of MethodContract.pre

  area: proofsconsumer: int256
  Task

  NethermindEth/LeanCIL#240 · Filter by author benaadams opened on Oct 24, 2026

• Build InvocationCertificate from a successful invoke

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#239 · Filter by author benaadams opened on Oct 24, 2026

• Kind-generic local snapshots, threaded through stepping

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#238 · Filter by author benaadams opened on Oct 24, 2026

• Composable straight-line segment contracts and code placement

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#237 · Filter by author benaadams opened on Oct 24, 2026

• Contract-aware stepping: apply registered contracts or proved child runs at call sites

  area: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#236 · Filter by author benaadams opened on Oct 24, 2026

• Profile-family gates: Holds.reprofile and one proof for many profiles

  area: proofsarea: verificationconsumer: int256
  Feature

  NethermindEth/LeanCIL#235 · Filter by author benaadams opened on Oct 24, 2026

• Extractor-emitted profile-parametric method bodies

  area: extractorarea: proofsconsumer: int256
  Feature

  NethermindEth/LeanCIL#234 · Filter by author benaadams opened on Oct 24, 2026

• Export contract sidecars whose proofs assume an initialized type

  area: proofsarea: verificationconsumer: int256
  Feature

  NethermindEth/LeanCIL#233 · Filter by author benaadams opened on Oct 24, 2026

• Exercise derived public contracts through DLL export and import

  area: proofsarea: verificationtests
  Task

  NethermindEth/LeanCIL#231 · Filter by author benaadams opened on Oct 24, 2026

• Support static-table libraries in forced full contract verification

  area: proofsarea: verification
  Feature

  NethermindEth/LeanCIL#229 · Filter by author benaadams opened on Oct 24, 2026

• Independently verify transitive contract dependency graphs

  area: proofsarea: verification
  Feature

  NethermindEth/LeanCIL#228 · Filter by author benaadams opened on Oct 24, 2026

• Support memory-backed Span and ReadOnlySpan parameters, locals and slices

  area: extractor
  Feature

  NethermindEth/LeanCIL#163 · Filter by author benaadams opened on Oct 22, 2026
  1