model-checking/verify-rust-std

Issues

• Challenge 1: Verify `core` transmuting methods

  #19 opened 6 months ago by tautschnig
  4

• Challenge 13: Safety of `CStr`

  #150 opened a month ago by celinval
  0

• Draft for tool proposal (goto-transcoder)

  #108 opened 2 months ago by rafaelsamenezes
  5

• Challenge 11: Safety of Methods for Numeric Primitive Types

  #59 opened 3 months ago by carolynzech
  11

• Challenge 3: Verifying Raw Pointer Arithmetic Operations

  #76 opened 3 months ago by feliperodri
  8

• Challenge 9: Safe abstractions for `core::time::Duration`

  #72 opened 3 months ago by feliperodri
  1

• Challenge 6: Safety of `NonNull`

  #53 opened 4 months ago by tautschnig
  31

• Update contract syntax to include contract forms as proposed in the MCP

  #44 opened 4 months ago by celinval
  1

• Challenge 12: Safety of `NonZero`

  #71 opened 3 months ago by carolynzech
  6

• [Challenge 6 Safety of NonNull] Verify contracts and proofs within the library source file

  #84 opened 3 months ago by QinyuanWu
  3

• Challenge 7: Safety of Methods for Atomic Types and `ReentrantLock`

  #83 opened 3 months ago by carolynzech
  0

• Tracking issue: Verifying raw pointer arithmetic

  #21 opened 3 months ago by celinval
  2

• Tracking issue for verifying the memory safety of the `alloc::collections::btree::node` module

  #25 opened 3 months ago by zhassan-aws
  2

• Challenge 10: Memory safety of String

  #61 opened 3 months ago by zhassan-aws
  0

• Challenge 8: Contracts for `SmallSort`

  #56 opened 3 months ago by qinheping
  0

• Challenge 5: Verify functions iterating over inductive data type: `linked_list`

  #29 opened 5 months ago by qinheping
  0

• Challenge 4: Memory safety of BTreeMap's `btree::node` module

  #77 opened 3 months ago by feliperodri
  0

• Challenge 2: Verify the memory safery of core intrinsics using raw pointers

  #16 opened 6 months ago by jaisnan
  1

• Fix library/ subtree and update folder from upstream

  #39 opened 4 months ago by celinval
  1

• Add format checker and clippy to CI

  #38 opened 5 months ago by celinval
  0

• Add runtime implementation of requires and ensures

  #17 opened 6 months ago by celinval
  0