Issues

• Suspected semantics bug: index_slice reverses IndexRef operands (lean and Rocq)

  mit-pdos/perennial#643 · Filter by author danielntmd opened on Nov 11, 2026
  1

• Add functional specs for time.Time comparisons (Before/After/Equal)

  mit-pdos/perennial#642 · Filter by author kris-gaudel opened on Nov 9, 2026

• assumeSumNoOverflowSigned rejects y = 0, so append(s, empty...) never returns in the model

  mit-pdos/perennial#641 · Filter by author Ode-to-a-Nightingale opened on Nov 8, 2026

• Goose and Go-semantics defects found on master: are fixes still welcome there, and on lean?

  mit-pdos/perennial#638 · Filter by author shubham3-ucb opened on Oct 14, 2026

• goose: records of field-less structs are generated in Prop; emit Record t : Type :=

  mit-pdos/perennial#637 · Filter by author shubham3-ucb opened on Oct 14, 2026

• Bug in Goose-generated code for map.for_range?

  mit-pdos/perennial#614 · Filter by author marshtompsxd opened on Jun 3, 2026
  1

• Don't load slice values in a for range unless they're explicitly used in the for statement

  mit-pdos/perennial#600 · Filter by author upamanyus opened on Apr 8, 2026

• go_string parsing doesn't handle multi-character escape sequences

  mit-pdos/perennial#593 · Filter by author lredlin opened on Mar 27, 2026

• delete more old files in src/{algebra,base_logic}

  mit-pdos/perennial#549 · Filter by author sanjit-bhat opened on Feb 21, 2026

• Nondeterminisitc make error during opam install --deps-only . (race condition during parallel make?)

  mit-pdos/perennial#523 · Filter by author marshtompsxd opened on Dec 21, 2025
  6

• wp_start / wp_end should automatically add / remove fupd's

  mit-pdos/perennial#518 · Filter by author sanjit-bhat opened on Dec 5, 2025

• goose pair notation conflicts with record-update set notation

  mit-pdos/perennial#487 · Filter by author sanjit-bhat opened on Nov 20, 2025
  1

• Add type-agnostic comparison to language semantics

  mit-pdos/perennial#476 · Filter by author tchajed opened on Nov 14, 2025

• make wp_if_destruct more robust

  mit-pdos/perennial#471 · Filter by author sanjit-bhat opened on Nov 12, 2025

• rm side-effecting exports from New.proof.sync

  mit-pdos/perennial#470 · Filter by author sanjit-bhat opened on Nov 12, 2025

• delete old branches

  mit-pdos/perennial#444 · Filter by author sanjit-bhat opened on Nov 5, 2025
  1

• Cleanup Python CI

  mit-pdos/perennial#428 · Filter by author sanjit-bhat opened on Oct 31, 2025

• Not clear whether pointers to empty structs/slices have same semantics as go

  mit-pdos/perennial#357 · Filter by author lredlin opened on Sep 8, 2025
  3

• Automation can't handle name collisions when helper functions use same parameter functions as outer function

  mit-pdos/perennial#338 · Filter by author lredlin opened on Aug 29, 2025

• Have a proper plan for export ordering

  mit-pdos/perennial#327 · Filter by author sanjit-bhat opened on Aug 20, 2025
  1

• More features related to prefixes in Iris proposition names

  mit-pdos/perennial#206 · Filter by author upamanyus opened on Mar 19, 2025
  2

• Failing test cases for tactics

  mit-pdos/perennial#78 · Filter by author upamanyus opened on Jul 18, 2024
  1

• Check print assumptions in CI

  mit-pdos/perennial#70 · Filter by author upamanyus opened on Jun 21, 2024
  2