Formal Land

At Formal Land we apply formal verification to everyday-life programs. Our key technique is to translate programming code into similar formal Coq code, and do our formal specifications/proofs directly on it. As our main customer, we are formally verifying the implementation of the cryptocurrency Tezos: https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/ This amounts to the verification of around 50,000 lines of code.