I tried building a benchmark for formally verifying popular Rust OSS. Along the way, I ended up finding real security vulnerabilities.In my previous article, I introduced h5i, an Axum-based Rust web framework that allows developers to translate application logic into Lean 4 and formally verify properties such as authorization, data isolation, and business rules.The core idea of h5i is pretty simple: instead of relying on unit tests alone to check whether an application behaves correctly, we want...