R&D Engineer — Formal Methods & Rust Tooling

Inria; Paris; Sur place; EUR 27 338 - 32 746; Plein temps

Avantages offerts par ce poste

Partial reimbursement of public travel

Leave: 7 weeks annual leave + RTT days

Teleworking after 6 months

Professional equipment

Social, cultural and sports events

Vocational training

Social security coverage

Résumé du poste

Inria is seeking an experienced Research and Development Engineer to join the FORMASK project, focusing on formal verification of cryptographic implementations. The role emphasizes extending Rust tooling, translating Rust to a proof assistant, and building reusable libraries for cryptographic components.

The candidate will work with EasyCrypt, Jasmin, OCaml, and SMT solvers, contributing to open-source tooling and ensuring high-quality software engineering within a multidisciplinary consortium.

Qualifications

• PhD in formal methods, programming languages, cryptography, or related field preferred.
• Strong proficiency in Rust and OCaml.
• Experience with a proof assistant (EasyCrypt, Coq, Why3) desirable.
• Knowledge of SMT solvers (CVC5, Z3) and side-channel security desirable.

Responsabilités

• Extend and improve reliability of formal verification tools (EasyCrypt, Jasmin).
• Translate and verify Rust code within a transpilation pipeline.
• Develop reusable libraries of cryptographic components.
• Present progress to consortium partners.
• Document and integrate developments into open-source repositories.

Connaissances

Rust programming

OCaml

Formal methods

Proof engineering

Formation

Graduate degree

PhD preferred

Outils

EasyCrypt

Jasmin

Coq/Why3

SMT solvers

Rust tooling

Description du poste

Inria is seeking an experienced Research and Development Engineer to join the FORMASK project, focusing on formal verification of cryptographic implementations. The role emphasizes extending Rust tooling, translating Rust to a proof assistant, and building reusable libraries for cryptographic components.

The candidate will work with EasyCrypt, Jasmin, OCaml, and SMT solvers, contributing to open-source tooling and ensuring high-quality software engineering within a multidisciplinary consortium.