Let's not forget the security kernel in Guttman's cryptlib. It's like a lightweight variant of formal verification that justs makes sure things interface correctly.
Which is interating here since F* can extract to OCaml. I wonder how hard it would be to wire up a test harness to compare the two with randomized tests.
OCaml has more runtime requirements. Can someone comment on how invasive those requirements are, and whether that would limit adoption of the OCaml version compared with C or rust?
How much does formal verification matter/increase confidence?
Is the rust version easier to integrate with other stacks?
https://mirage.io/blog/why-ocaml-tls