Rust has risen in prominence as a systems programming language in large part due to its focus on reliability. The language’s advanced type system and borrow checker eliminate certain classes of memory safety violations. But for critical pieces of code, teams need assurance beyond what the type checker alone can provide. At Amazon Web Services, we are implementing a model checker for Rust that can verify other properties, from memory faults in unsafe Rust code to user-defined correctness assertions. This paper particularly focuses on the challenges in reasoning about Rust’s dynamic trait objects, a feature that provides dynamic dispatch for function abstractions. While the explicit dyn keyword that denotes dynamic dispatch is used in 37% of the 500 most-downloaded Rust libraries (crates), dynamic dispatch is implicitly linked into 70%. To our knowledge, our open-source Rust Model Checker (RMC) is the first symbolic modeling checking tool for Rust that can verify correctness while supporting the breadth of dynamic trait objects, including dynamic closures. We show how our system uses semantic trait information from Rust’s Mid-level Intermediate Representation (an advantage over targeting a language-agnostic level such as LLVM) to improve verification performance by 5%–15X for examples from open-source virtualization software. Finally, we share an open-source suite of verification test cases for dynamic trait objects.