Comment by sevenoftwelve

Author here: No, symbolic verification does not protect from buffer overflows. Writing the implementation in Rust does

We are investigating ways how to do more formal verification for the implementation itself.