Issues

• Find why an extraction module is rebuilt during proof checking on a reused workspace

  area: verificationbugfix & reliabilityconsumer: int256
  NethermindEth/LeanCIL#561 · Filter by author benaadams opened on Nov 11, 2026

• Step exact-fuel leaf proofs with the shared stepping tactics

  area: proofsconsumer: int256feature
  NethermindEth/LeanCIL#559 · Filter by author benaadams opened on Nov 11, 2026

• Stepping prints an info-level "Error: index out of bounds" on a body that is still a variable

  area: proofsbugfix & reliability
  NethermindEth/LeanCIL#558 · Filter by author benaadams opened on Nov 11, 2026

• Measure and bound the cost of fact preparation in the stepping tactics

  area: proofsperformance
  NethermindEth/LeanCIL#557 · Filter by author benaadams opened on Nov 11, 2026

• Carry static-world validity and helper-written home facts across walked stores

  area: proofsconsumer: int256feature
  NethermindEth/LeanCIL#556 · Filter by author benaadams opened on Nov 11, 2026

• Walk stores into by-reference argument cells in a snapshot contract walk

  area: proofsconsumer: int256feature
  NethermindEth/LeanCIL#555 · Filter by author benaadams opened on Nov 11, 2026

• Test closure-scoped first verify through the CLI on a real extraction

  area: verificationtests
  Feature

  NethermindEth/LeanCIL#545 · Filter by author benaadams opened on Nov 10, 2026

• Use the cached certified library for workspace in a LeanCIL checkout

  area: verificationperformance
  Feature

  NethermindEth/LeanCIL#544 · Filter by author benaadams opened on Nov 10, 2026

• Investigate certified library builds that differ byte for byte under one cache key

  area: verificationbugfix & reliability
  Bug

  NethermindEth/LeanCIL#543 · Filter by author benaadams opened on Nov 10, 2026

• Outline a helper call whose callee calls or stores beside a test

  area: extractorarea: proofsfeature
  Feature

  NethermindEth/LeanCIL#542 · Filter by author benaadams opened on Nov 10, 2026

• Declare a public proof surface checked by consumer-shaped regression proofs

  area: proofsfeature
  Feature

  NethermindEth/LeanCIL#539 · Filter by author benaadams opened on Nov 9, 2026

• Audit axioms once per module instead of printing them per theorem

  area: proofsrefactor & cleanup
  Feature

  NethermindEth/LeanCIL#538 · Filter by author benaadams opened on Nov 9, 2026

• Experiment: prove closed scalar instruction stretches by kernel evaluation

  area: proofsperformance
  Feature

  NethermindEth/LeanCIL#537 · Filter by author benaadams opened on Nov 9, 2026

• Provide a reviewed library of common C# specifications

  area: proofsfeaturefuture
  Feature

  NethermindEth/LeanCIL#534 · Filter by author benaadams opened on Nov 9, 2026

• Step instructions through opcode-selected lemmas and checked facts, without naming evaluator internals

  area: proofsfeature
  Feature

  NethermindEth/LeanCIL#529 · Filter by author benaadams opened on Nov 9, 2026

• Reuse a certified proof when an unrelated assembly rebuild leaves its extraction unchanged

  area: verificationperformance
  Feature

  NethermindEth/LeanCIL#525 · Filter by author benaadams opened on Nov 9, 2026

• Refresh live Lean goals after workspace extraction changes without manual file restart

  area: verificationfeature
  NethermindEth/LeanCIL#523 · Filter by author benaadams opened on Nov 9, 2026

• Provide a proof-facing facade module with an import-closure budget

  area: proofsperformance
  NethermindEth/LeanCIL#522 · Filter by author benaadams opened on Nov 9, 2026

• Avoid repeated extraction and verification preparation in the proof watch loop

  area: verificationperformance
  NethermindEth/LeanCIL#521 · Filter by author benaadams opened on Nov 9, 2026

• Measure end-to-end proof authoring latency on representative consumer workloads

  area: verificationperformance
  NethermindEth/LeanCIL#520 · Filter by author benaadams opened on Nov 9, 2026

• Pilot memory-safety verification of MessagePack v4 SIMD integer encoding

  area: proofsfeaturefuture
  NethermindEth/LeanCIL#519 · Filter by author benaadams opened on Nov 9, 2026

• new-proof: outline aggregate homes and broader struct receiver loops

  area: proofsfeature
  NethermindEth/LeanCIL#492 · Filter by author benaadams opened on Nov 5, 2026

• Support recursive calls proved by a decreasing measure

  area: extractorarea: proofsfeaturefuture
  NethermindEth/LeanCIL#484 · Filter by author benaadams opened on Nov 5, 2026

• Support throwing and handling exceptions

  area: extractorarea: proofsfeaturefuture
  NethermindEth/LeanCIL#483 · Filter by author benaadams opened on Nov 5, 2026

• Support delegates, lambdas and closures

  area: extractorarea: proofsfeaturefuture
  NethermindEth/LeanCIL#482 · Filter by author benaadams opened on Nov 5, 2026