Translation of Rust's core and alloc crates to Coq for formal verification(formal.land)
327 points by p4bl0 | 103 comments
Formal Land blog post describing a best-effort translation of Rust's core and alloc crates into Coq using their coq-of-rust tool for formal verification.