[clarus]

Formal Land | Proof Engineer | Remote or Paris, France | https://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.

Open roles:

* Coq proof engineer: https://formal.land/assets/files/formal-verification-ocaml-f...

Tech Stack: Coq, OCaml, Haskell, Rust, TypeScript

Twitter: https://twitter.com/LandFoobar

Thanks.