There's a huge difference between "Verus can prove the safety of unsafe code" and "Verus can EASILY prove the safety of unsafe code." And I bet it can't prove everything, like calls to a C ABI.