I am aware that AWS is using OCaml in their verified cryptography project, s2n-bignum.
https://github.com/awslabs/s2n-bignum is a collection of high-performance assembly subroutines that are used by AWS-LC, an OpenSSL-equivalent project (https://github.com/aws/aws-lc).
The proofs of s2n-bignum are written in HOL Light (https://github.com/jrh13/hol-light), which is an OCaml program.
I am aware that AWS is using OCaml in their verified cryptography project, s2n-bignum.
https://github.com/awslabs/s2n-bignum is a collection of high-performance assembly subroutines that are used by AWS-LC, an OpenSSL-equivalent project (https://github.com/aws/aws-lc).
The proofs of s2n-bignum are written in HOL Light (https://github.com/jrh13/hol-light), which is an OCaml program.