Issues

• Rc/Arc::get_mut_unchecked contract does not encode its aliasing precondition

  model-checking/verify-rust-std#693 · Filter by author feliperodri opened on Sep 23, 2026

• The pinned Kani reports a failed compare_exchange as a success

  model-checking/verify-rust-std#673 · Filter by author kanapitsas opened on Sep 3, 2026

• Challenge 28 (flt2dec): Kani's uninitialized-memory checker cannot analyze the MaybeUninit prefixes

  model-checking/verify-rust-std#671 · Filter by author kanapitsas opened on Sep 3, 2026

• Challenge 12 (NonZero): known verification gaps from tool limits (follow-up to #637)

  model-checking/verify-rust-std#656 · Filter by author feliperodri opened on Aug 25, 2026

• Tautological postconditions: some merged contracts hold for any implementation (demonstrated by mutation)

  model-checking/verify-rust-std#630 · Filter by author KyleClouthier opened on Aug 6, 2026
  2

• Proposal: two acceptance criteria for verification harnesses

  model-checking/verify-rust-std#617 · Filter by author KyleClouthier opened on Jul 27, 2026

• Challenge 31: Enriching MIR Consts

  Challenge
  model-checking/verify-rust-std#594 · Filter by author dkcumming opened on Apr 29, 2026

• Challenge 30: Progress Public MIR

  Challenge
  model-checking/verify-rust-std#591 · Filter by author dkcumming opened on Apr 24, 2026

• Add Tool: Verus

  Tool Application
  model-checking/verify-rust-std#554 · Filter by author elanortang opened on Mar 3, 2026
  8

  

• Challenge 29: Safety of boxed

  Challenge
  model-checking/verify-rust-std#526 · Filter by author AlexLB99 opened on Jan 12, 2026

• Challenge 28: Safety of float to decimal conversion module

  Challenge
  model-checking/verify-rust-std#524 · Filter by author AlexLB99 opened on Jan 12, 2026
  1

• Add Tool: Creusot

  Tool Application
  model-checking/verify-rust-std#493 · Filter by author Lysxia opened on Sep 16, 2025
  6

  

• Could Kani CI summary be simplified?

  Question
  model-checking/verify-rust-std#411 · Filter by author zjp-CN opened on Jul 7, 2025
  4

• How to integrate distributed-verification into verify-rust-std?

  Question
  model-checking/verify-rust-std#409 · Filter by author zjp-CN opened on Jul 7, 2025
  1

  

• Challenge 27: Verify atomically reference-counted Cell implementation

  Challenge
  model-checking/verify-rust-std#383 · Filter by author AlexLB99 opened on Jun 6, 2025

• Challenge 26: Verify reference-counted Cell implementation

  Challenge
  model-checking/verify-rust-std#382 · Filter by author AlexLB99 opened on Jun 6, 2025
  7

• Challenge 25: Verify the safety of VecDeque functions

  Challenge
  model-checking/verify-rust-std#286 · Filter by author thanhnguyen-aws opened on Mar 18, 2025
  3

• Challenge 24: Verify the safety of Vec functions part 2

  Challenge
  model-checking/verify-rust-std#285 · Filter by author thanhnguyen-aws opened on Mar 18, 2025
  2

• Challenge 23: Verify the safety of Vec functions part 1

  Challenge
  model-checking/verify-rust-std#284 · Filter by author thanhnguyen-aws opened on Mar 18, 2025
  6

• Challenge 18: Verify the safety of slice iter functions - part 1

  Challenge
  model-checking/verify-rust-std#282 · Filter by author thanhnguyen-aws opened on Mar 18, 2025
  3

• Challenge 17: Verify the safety of slice functions

  Challenge
  model-checking/verify-rust-std#281 · Filter by author thanhnguyen-aws opened on Mar 18, 2025
  6

• Challenge 16: Verify the safety of Iterator functions

  Challenge
  model-checking/verify-rust-std#280 · Filter by author thanhnguyen-aws opened on Mar 18, 2025
  3

• Challenge 22: Verify the safety of str iter functions

  Challenge
  model-checking/verify-rust-std#279 · Filter by author thanhnguyen-aws opened on Mar 18, 2025
  2

• Challenge 21: Verify the safety of substring-related functions in str::pattern

  Challenge
  model-checking/verify-rust-std#278 · Filter by author thanhnguyen-aws opened on Mar 18, 2025

• Challenge 20: Verify the safety of char-related functions in str::pattern

  Challenge
  model-checking/verify-rust-std#277 · Filter by author thanhnguyen-aws opened on Mar 18, 2025