Formal Land | Proof Engineer | Remote or Paris, France | https://formal.land/ https://formal.land/ At Formal Land we apply formal verification to everyday-lif

Formal Land | Proof Engineer | Remote or Paris, France | https://formal.land/ 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/ 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-formal-land-137af30dc6ed50e7555a7bd3e7d584c7.pdf https://formal.land/assets/files/formal-verification-ocaml-f... Tech Stack: Coq, OCaml, Haskell, Rust, TypeScript Twitter: https://twitter.com/LandFoobar https://twitter.com/LandFoobar Thanks.