Issues

• size_of not having check(ghost) appears weird

  discussion
  creusot-rs/creusot#2279 · Filter by author Kixunil opened on Oct 1, 2026
  1

• C-like enum as {integer} cast loses some information

  enhancement
  creusot-rs/creusot#2274 · Filter by author Kixunil opened on Sep 29, 2026
  1

• Specifying Hash and Hasher

  add-specsenhancement
  creusot-rs/creusot#2264 · Filter by author Kixunil opened on Sep 25, 2026
  5

• --span-mode=relative is broken

  buglow-priority
  creusot-rs/creusot#2232 · Filter by author Lysxia opened on Aug 19, 2026

• Contract projecting a private field emits literal ERROR_UNBOUND_<field> tokens in cross-module callers' coma (why3 syntax error)

  bug
  creusot-rs/creusot#2203 · Filter by author jay-oraclizer opened on Jul 12, 2026
  1

• size_of should pedantically be unknown for #[repr(Rust)] types

  soundness
  creusot-rs/creusot#2186 · Filter by author dianegolfouse opened on Jul 2, 2026
  4

• String literals

  bug
  creusot-rs/creusot#2184 · Filter by author jhjourdan opened on Jul 1, 2026
  1

• C-string literals are not supported by Creusot

  enhancement
  creusot-rs/creusot#2182 · Filter by author niooss-ledger opened on Jul 1, 2026
  1

• Reduce the effort needed to get well-typed Rust code to compile with Creusot

  discussionenhancement
  creusot-rs/creusot#2172 · Filter by author Lysxia opened on Jun 25, 2026
  7

• Whitelist external traits for dyn

  enhancement
  creusot-rs/creusot#2167 · Filter by author Lysxia opened on Jun 24, 2026

• ICE using literal bytes

  bug
  creusot-rs/creusot#2161 · Filter by author niooss-ledger opened on Jun 23, 2026
  8

  

• Use the Reborrows trait for Ghost and Token ghost types

  enhancement
  creusot-rs/creusot#2156 · Filter by author jhjourdan opened on Jun 22, 2026

• Allow omitting the body of logic(opaque) functions

  enhancement
  creusot-rs/creusot#2121 · Filter by author Lysxia opened on May 28, 2026
  1

• Incremental verification workflow

  enhancement
  creusot-rs/creusot#2120 · Filter by author Lysxia opened on May 27, 2026
  2

• Setup for dev versions of Creusot

  enhancement
  creusot-rs/creusot#2115 · Filter by author Lysxia opened on May 22, 2026
  3

• Termination check doesn't handle default impls

  bugtermination
  creusot-rs/creusot#2110 · Filter by author Lysxia opened on May 18, 2026
  1

• Better syntax for specifying functions that call closures

  discussionenhancement
  creusot-rs/creusot#2074 · Filter by author jhjourdan opened on Apr 28, 2026
  3

• Notation for chained comparisons

  enhancement
  creusot-rs/creusot#2063 · Filter by author Lysxia opened on Apr 24, 2026
  6

• Support ? in logic

  enhancement
  creusot-rs/creusot#2062 · Filter by author Lysxia opened on Apr 24, 2026

• Call logic lemmas in programs

  enhancement
  creusot-rs/creusot#2031 · Filter by author Lysxia opened on Apr 12, 2026
  6

• Check type invariant when constructing a new struct/enum value

  enhancement
  creusot-rs/creusot#2027 · Filter by author jhjourdan opened on Apr 9, 2026

• Support strict type invariant checking?

  enhancement
  creusot-rs/creusot#2025 · Filter by author Kixunil opened on Apr 8, 2026
  11

• Make it possible for derives to emit check(ghost)

  enhancement
  creusot-rs/creusot#2014 · Filter by author Kixunil opened on Mar 27, 2026
  3

• rustc-like error messages for failed proofs

  enhancementerror-messages
  creusot-rs/creusot#2012 · Filter by author Kixunil opened on Mar 27, 2026
  16

• Rename equality operators

  enhancement
  creusot-rs/creusot#1998 · Filter by author Lysxia opened on Mar 21, 2026
  16