Working on formal verification of functional programs using Coq at Formal Land. See for example https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/ to verify the code of the crypto-currency Tezos.
