Comment by bcjdjsndon

> With Verus, however, developers can mathematically prove the safety of their unsafe Rust code, re-establishing machine-checked safety guarantees

Why then does rust even need the unsafe keyword?