1. Introduction
  2. General Rules
    1. Challenge Template
    2. Tool Application Template
  4. Verification Tools
    1. Kani
  8. Challenges
    1. 1: Verify core transmuting methods
    2. 2: Verify the memory safety of core intrinsics using raw pointers
    3. 3: Verifying Raw Pointer Arithmetic Operations
    4. 4: Memory safety of BTreeMap's btree::node module
    5. 5: Verify functions iterating over inductive data type: linked_list
    6. 6: Safety of NonNull
    7. 7: Safety of Methods for Atomic Types & Atomic Intrinsics
    8. 8: Contracts for SmallSort
    9. 9: Safe abstractions for core::time::Duration
    10. 10: Memory safety of String
    11. 11: Safety of Methods for Numeric Primitive Types
    12. 12: Safety of NonZero
    13. 13: Safety of CStr
    14. 14: Safety of Primitive Conversions