Verify Rust Std Lib Introduction General Rules Challenge Template Tool application Verification Tools Kani Challenges Core Transmutation Memory safety of core intrinsics Pointer Arithmetic Memory safety of BTreeMap's btree::node module Inductive data type Contracts for SmallSort