Simplicity has a bunch of Coq proofs actually. And Cardano probably has some formal stuff too, but I am not into proof-of-stake.