Issues

• Design a mature backend-neutral Uneffect specification DSL

  effort:Lenhancementpriority:P1status:queued
  mizchi/uneffect#64 · Filter by author mizchi opened on Aug 29, 2026 · Phase 2 — Specification expressiveness

• Generalize CFG value lattices and recurrence widening

  effort:Lenhancementpriority:P1status:queued
  mizchi/uneffect#25 · Filter by author mizchi opened on Aug 28, 2026 · Phase 2 — Specification expressiveness

• Add interprocedural alias and dynamic refinement evidence

  effort:XLenhancementpriority:P2status:queued
  mizchi/uneffect#24 · Filter by author mizchi opened on Aug 27, 2026 · Phase 3 — Production integration

• Track top-level module initialization effects

  effort:Menhancementpriority:P0status:queued
  mizchi/uneffect#18 · Filter by author mizchi opened on Aug 25, 2026 · Phase 1 — Proof boundaries
  11

• Complete React function component lifecycle semantics

  effort:XLenhancementpriority:P2status:queued
  mizchi/uneffect#16 · Filter by author mizchi opened on Aug 24, 2026 · Phase 3 — Production integration
  57

• Implement proof-gated optimizer transformations

  effort:XLenhancementpriority:P3status:queued
  mizchi/uneffect#13 · Filter by author mizchi opened on Aug 24, 2026 · Phase 4 — Proof consumers

• Complete Node and Web event-loop ownership semantics

  effort:XLenhancementpriority:P2status:queued
  mizchi/uneffect#10 · Filter by author mizchi opened on Aug 24, 2026 · Phase 3 — Production integration
  1

• Reach native Corsa frontend semantic parity

  effort:Lenhancementpriority:P2status:queued
  mizchi/uneffect#8 · Filter by author mizchi opened on Aug 24, 2026 · Phase 3 — Production integration
  1

• Investigate independently checkable proof evidence

  effort:Menhancementpriority:P2status:queued
  mizchi/uneffect#7 · Filter by author mizchi opened on Aug 24, 2026 · Phase 3 — Production integration

• Complete interprocedural typed-array and SHA-256 verification

  effort:XLenhancementpriority:P1status:queued
  mizchi/uneffect#6 · Filter by author mizchi opened on Aug 24, 2026 · Phase 2 — Specification expressiveness

• Complete temporal collection parity and TLC trace interoperability

  effort:Menhancementpriority:P1status:queued
  mizchi/uneffect#5 · Filter by author mizchi opened on Aug 24, 2026 · Phase 2 — Specification expressiveness

• Complete contract-derived property generators and shrinking

  effort:Lenhancementpriority:P1status:queued
  mizchi/uneffect#4 · Filter by author mizchi opened on Aug 24, 2026 · Phase 2 — Specification expressiveness

• Generalize temporal invariant synthesis and temporal formulas

  effort:Lenhancementpriority:P1status:queued
  mizchi/uneffect#2 · Filter by author mizchi opened on Aug 24, 2026 · Phase 2 — Specification expressiveness