Search results

Call logic lemmas in programs

enhancementNew feature or requestNew feature or request

Status: Open.

#2031 In creusot-rs/creusot;

· Lysxia opened on Apr 12, 2026

Two issues with #[bitwise_mode]`

Status: Open.

#2028 In creusot-rs/creusot;

· jhjourdan opened on Apr 12, 2026

Check type invariant when constructing a new struct/enum value

Status: Open.

#2027 In creusot-rs/creusot;

· jhjourdan opened on Apr 9, 2026

Support strict type invariant checking?

enhancementNew feature or requestNew feature or request

Status: Open.

#2025 In creusot-rs/creusot;

· Kixunil opened on Apr 8, 2026

Make it possible for derives to emit check(ghost)

enhancementNew feature or requestNew feature or request

Status: Open.

#2014 In creusot-rs/creusot;

· Kixunil opened on Mar 27, 2026

rustc-like error messages for failed proofs

enhancementNew feature or requestNew feature or request

error-messagesImprove error messagesImprove error messages

Status: Open.

#2012 In creusot-rs/creusot;

· Kixunil opened on Mar 27, 2026

ERROR_UNBOUND emitted when constants, structs and modules are combined

bugSomething isn't workingSomething isn't working

Status: Open.

#2009 In creusot-rs/creusot;

· Kixunil opened on Mar 26, 2026

Rename equality operators

enhancementNew feature or requestNew feature or request

Status: Open.

#1998 In creusot-rs/creusot;

· Lysxia opened on Mar 21, 2026

Default specs on trait impl methods

enhancementNew feature or requestNew feature or request

Status: Open.

#1992 In creusot-rs/creusot;

· Lysxia opened on Mar 17, 2026

Redesigning "spec traits"

discussion

enhancementNew feature or requestNew feature or request

Status: Open.

#1991 In creusot-rs/creusot;

· Lysxia opened on Mar 17, 2026

Use extern_spec for derived implementations

enhancementNew feature or requestNew feature or request

Status: Open.

#1990 In creusot-rs/creusot;

· Lysxia opened on Mar 17, 2026

Send and Sync should be #[trusted] traits

bugSomething isn't workingSomething isn't working

soundnessEnhance soundnessEnhance soundness

Status: Open.

#1989 In creusot-rs/creusot;

· jhjourdan opened on Mar 16, 2026