All pull requests

Pull requests

• Challenge 8: verify smallsort safety and sorting correctness with Kani

  #694·kasimte opened Sep 23, 2026·

  ·

• Challenge 23: verify Vec mod.rs function safety with Kani

  Challenge
  #692·kasimte opened Sep 22, 2026·

  ·
  1

• Challenge 24: verify Vec IntoIter and spec_* function safety with Kani

  Challenge
  #689·kasimte opened Sep 18, 2026·

  ·

• Merge subtree update for toolchain nightly-2026-08-21

  Maintenancerust
  #687·github-actions[bot] opened Sep 13, 2026Bot·

  ·
  3

  

• Challenge 4: Verify memory safety of BTreeMap node module with Kani

  Challenge
  #684·v3risec opened Sep 10, 2026·

  ·
  1

  3

• Challenge 7: Verify safety of Atomic types and Atomic Intrinsics with Kani

  Accepted SolutionChallenge
  #683·v3risec opened Sep 8, 2026·

  ·
  1

  3

• Challenge 25: Verify the safety of VecDeque (unbounded, symbolic ring layouts, contracts on all 13 unsafe fns)

  Accepted SolutionChallenge
  #681·jrey8343 opened Sep 8, 2026·

  ·
  1

  2

  

• Challenge 8 (partial): no-UB proofs and sorting-correctness harnesses for smallsort

  Challenge
  #678·samiam713 opened Sep 7, 2026·

  ·

• Add Kani proof harnesses and contracts for unchecked_div_exact

  Maintenance
  #672·CYJ904 opened Sep 3, 2026·

  ·
  4

  

• Challenge 13: contracts and proofs for CStr trait implementations and safe methods

  Challenge
  #670·kasimte opened Sep 2, 2026·

  ·
  2

• Challenge 29: Verify the safety of Box and ThinBox in alloc::boxed

  Challenge
  #669·kasimte opened Sep 2, 2026·

  ·
  4

• Challenge 2: Verify safety of raw-pointer intrinsics with Kani

  Challenge
  #668·v3risec opened Sep 1, 2026·

  ·
  1

  1

• Challenge 21 (partial): bounded Kani PROBE of shipped TwoWaySearcher::next_back short-period arms

  Challenge
  #664·ivmat opened Aug 29, 2026·

  ·
  2

• Add proof harnesses for unchecked_disjoint_bitor on unsigned integer …

  Maintenance
  #662·Tianshu-Huang opened Aug 27, 2026·

  ·
  4

  

• Challenge 26: Verify the safety of Rc and Weak in alloc::rc

  Challenge
  #661·kasimte opened Aug 27, 2026·

  ·
  1

• Strengthen Duration::from_secs contract to exclude fractional seconds

  Challenge
  #658·Adkid-Zephyr opened Aug 27, 2026·

  ·
  2

• Challenge 17: Verify slice safety with Kani

  Challenge
  #657·v3risec opened Aug 27, 2026·

  ·
  1

• Add Kani harnesses for Challenge 18: slice iter functions

  Challenge
  #651·MavenRain opened Aug 21, 2026·

  ·
  1

  3

• Challenge 2: memory safety of raw-pointer intrinsics

  Accepted SolutionChallenge
  #649·stefanzetzsche opened Aug 20, 2026·

  ·
  1

• Challenge 29: Kani contracts for Box, convert, and ThinBox

  Challenge
  #639·sankalpsthakur opened Aug 20, 2026·

  ·
  1

  4

• Challenge 13: safety of CStr

  Accepted SolutionChallenge
  #638·stefanzetzsche opened Aug 20, 2026·

  ·
  2

  

• Challenge 16: Verify safety of iterator adapter functions with Kani

  Challenge
  #632·v3risec opened Aug 13, 2026·

  ·
  1

• Challenge 21: Verify safety of StrSearcher with Kani

  Challenge
  #621·v3risec opened Aug 3, 2026·

  ·
  1

  6

  

• Challenge 20: Verify Char Searcher with Kani

  Challenge
  #620·v3risec opened Aug 2, 2026·

  ·
  1

  11

  

• Challenge 28: Verify flt2dec safety with Kani

  Challenge
  #606·v3risec opened Jul 2, 2026·

  ·
  1

  4