Note that this is the same author who worked on formally verifying Rust's type system via RustBelt (https://www.ralfj.de/blog/2017/07/08/rustbelt.html), which has managed to find a few bugs in the standard library (https://www.ralfj.de/blog/2017/06/09/mutexguard-sync.html and https://www.ralfj.de/blog/2018/07/13/arc-synchronization.htm...), and also hopefully provides (by the nature of formal proofs) some small comfort regarding the quantity of other latent bugs. :P