Cryspen is a company that build high assurance security-critical software using formal verification. We develop the hax verification toolchain for Rust and apply it to develop cryptographic software used by prominent software companies and projects. We firmly believe that privacy and end-to-end security are the cornerstones of a modern, open society. Our mission is to build usable and effective verification tools that any developer can use to build provably safe and secure applications.

We are currently seeking a Compiler and Verification Tools engineer to join our team. In this role, you will help us extend and improve hax, notably the compilation of Rust to various backend provers like Lean and ProVerif. You will also have the opportunity to apply the toolchain on high-impact codebases as part of various Cryspen projects.

Locations: France, Germany

Tasks

* Maintain the link between the hax toolchain and the rustc compiler

* Implement code transformations for Rust, enabling translations to Lean and ProVerif

* Build usable tools around hax to help users verify real-world software

* Apply and test hax on a variety of prominent Rust projects

Requirements

* Experience in writing and maintaining language compilers and translations

* Proficient in Rust; knowledge of other languages like OCaml is a plus

* Knowledge of formal verification tools and processes is not required, but is a plus

Benefits

• Room to grow personally and professionally
• Work on high-impact projects
• Shape your own role
• Flexible working hours
• Family-friendly work environment

Application Process

We will try to get back to you as soon as possible after sending in your application. After the first screening call, there will be several interviews (video calls) covering technical aspects as well as making sure we are aligned on the core values.