  Rust is a modern systems programming language whose type system guarantees
memory safety. For the sake of expressivity and performance it allows
programmers to relax typing rules temporarily, using unsafe code blocks.
However, in unsafe blocks, the burden of making sure that the code does not end
up having undefined behaviour is on the programmer. Even most expert
programmers make mistakes and a memory safety bug in an unsafe block renders
all the type system guarantees void. To address this problem we are trying to
verify soundness of Rust unsafe code applying our Modular Symbolic Execution
algorithm. This text outlines our approach and the progress that has been made
so far.
