Formal Land

A searchable index of Hacker News “Who is hiring?” job postings.

← All postings · February 2022 thread

Proof Engineer

Company	Formal Land
Website	formal.land ↗
Roles	Proof Engineer Coq proof engineer
Role taxonomy	Software Engineering
Specialties	Software Engineering
Location	Remote
Salary	—
Apply via	Application link — https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/
Hiring notes	—
Tech	TypeScript Rust
Posted by	clarus
Posted	Feb 1, 2022
Source	View on Hacker News ↗

Original posting

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.