I think the two bullet points they listed for their project (other than using Rust) are often overlooked: - Leaving out less commonly used features so as to reduce attack surface - Developing an extensive test suite which even managed to find bugs in the original sudo Which are the most important aspects when writing any safety-critical code, even moreso than rewriting in Rust!
- Proven with Coq, a formal proof management system: https://coq.inria.fr/
See in the real world: https://aws.amazon.com/security/provable-security/
And check out Computer-Aided Verification (CAV).