A kind of nice talk about using F* language to verify crypto code that ends being compiled to C (some parts of it are in Firefox57):
I hope we'll see some of this proved for Rust.