Issues

• aver proof main.av exports without panicking now (#1449) but the Lean build fails in three shapes: Inhabited Bytes for fuel panic, Decidable on a Result of a record tuple, free oracle variable in effectful cases

  jasisz/aver#1462 · Filter by author n1bor opened on Sep 26, 2026
  1

• Prove source request-trace equivalence for yield lowering

  jasisz/aver#1376 · Filter by author jasisz opened on Sep 15, 2026

• Concurrency as data plus effects: an explicit coordinator for ordered decisions, proven laws for order-free knowledge

  enhancement
  jasisz/aver#1329 · Filter by author jasisz opened on Sep 10, 2026

• Lean export: close the remaining historical corpus parity gaps

  jasisz/aver#1010 · Filter by author jasisz opened on Aug 19, 2026
  2

• self-host parity: higher-order functions, doc continuation, discharge fence

  enhancement
  jasisz/aver#436 · Filter by author jasisz opened on Jun 6, 2026
  2

• 0.25: retire classify-time fused leaf-ops — move runtime Result/Option fusion onto MIR

  jasisz/aver#434 · Filter by author jasisz opened on Jun 5, 2026
  1