Issues

• Rocq proof: byte inverse axioms omit byte well-formedness premises

  Wasm-DSL/spectec#246 · Filter by author davidads-Humanis-AIs opened on Oct 19, 2026

• Unsound undep transformation

  Wasm-DSL/spectec#244 · Filter by author zilinc opened on Oct 13, 2026

• question about licensing of the mechanizations

  Wasm-DSL/spectec#243 · Filter by author ecioppettini opened on Oct 9, 2026
  3

• Upstreaming middlend passes

  Wasm-DSL/spectec#238 · Filter by author zilinc opened on Jun 10, 2026
  3

• Uniqueness of variables in the environment

  Wasm-DSL/spectec#236 · Filter by author zilinc opened on Jun 3, 2026
  2

• Preserving (dependent) typeability in IL->IL passes

  Wasm-DSL/spectec#235 · Filter by author zilinc opened on May 31, 2026
  29

• Frontend.Dim assertion failure

  Wasm-DSL/spectec#180 · Filter by author zilinc opened on Aug 6, 2025
  1

• Add dependencies to dune-project

  Wasm-DSL/spectec#175 · Filter by author raoxiaojia opened on Jul 22, 2025
  1

• Cannot match a variable against an optional non-terminal in a rule definition

  Wasm-DSL/spectec#132 · Filter by author yusungsim opened on Nov 7, 2024
  2

• Spec conversion burndown list

  Wasm-DSL/spectec#67 · Filter by author rossberg opened on Feb 4, 2024