While I think Coq is usually used for mathematical proofs rather than program verification, I know there are a number of formally verified data structures writt

While I think Coq is usually used for mathematical proofs rather than program verification, I know there are a number of formally verified data structures written in Coq that have also been directly translated to other languages. See e.g. https://www.cs.princeton.edu/~appel/papers/redblack.pdf https://www.cs.princeton.edu/~appel/papers/redblack.pdf