Research and Development Engineer in Formal Methods

Research and Development Engineer in Formal Methods Download job offer in PDF format Contract type : Fixed-term contract Level of qualifications required : Graduate degree or equivalent Other valued qualifications : Doctorat Fonction : Temporary scientific engineer About the research centre or Inria department Inria is the French National Institute for Research in Digital Science, of which the Inria Côte d'Azur University Center is a part. With strong expertise in computer science and applied mathematics, the research projects of the Inria Côte d'Azur University Center cover all aspects of digital science and technology and generate innovation. Based mainly in Sophia Antipolis, but also in Nice and Montpellier, it brings together 47 research teams and nine support services. It is active in the fields of artificial intelligence, data science, IT system security, robotics, network engineering, natural risk prevention, ecological transition, digital biology, computational neuroscience, health data, and more. The Inria Center at Université Côte d'Azur is a major player in terms of scientific excellence, thanks to the results it has achieved and its collaborations at both European and international level. Context This position is part of the FORMASK project, carried out within a consortium bringing together Inria, PQShield, and CryptoExperts, and supported by the Programme de Transfert au Campus Cyber (PTCC). FORMASK aims to strengthen the security of cryptographic implementations against side-channel attacks (power consumption, electromagnetic radiation, execution time). Masking is currently one of the most effective software countermeasures, but implementing it correctly remains challenging. The project's goal is to develop an open, industrial-grade formal verification toolchain that guarantees both the functional correctness and the physical attack resistance of masked cryptographic implementations. The successful candidate will primarily contribute to the development and extension of the consortium's formal verification tools (the EasyCrypt, Jasmin, and maskVerif frameworks), which form the core technical infrastructure of the project. A significant part of the work will focus on the Jasmin compiler (a low-level language for high-assurance cryptography whose semantics are formalized in Rocq/Coq): extending its formal model, sharing architecture descriptions with EasyCrypt, and improving the associated verification toolchains. This is a highly technical software engineering position at the intersection of programming languages, compiler construction, and formal methods, with developments released as open-source software. Occasional travel (monthly consortium meetings and seminars) is expected. Travel expenses will be reimbursed in accordance with the applicable reimbursement policy. Assignment Main responsibilities: With the support of the project team and under the supervision of Benjamin Grégoire, the successful candidate will be responsible for extending and improving the reliability of the formal verification tools developed within FORMASK. This includes extending proof languages and program logics to support constructs from systems programming languages, sharing hardware architecture descriptions across the consortium's tools, and strengthening the automated verification capabilities for masking countermeasures. Learning resources: A literature review and key scientific references (EasyCrypt, Jasmin, maskVerif, SNI/PINI security properties) will be provided to the successful candidate. These resources are also available through the team's website and the consortium's publications. Collaboration: The successful candidate will work closely with researchers and engineers from all three consortium partners, including the authors and maintainers of EasyCrypt and Jasmin, contributing to the continued development and consolidation of these tools. Ownership: The successful candidate will be responsible for designing, implementing, and validating robust and maintainable software components, while proactively improving the reliability, consistency, and reusability of the resulting tooling. Technical leadership: The successful candidate will independently manage the technical follow-up of their developments, ensure proper documentation, and integrate their contributions into the consortium's shared repositories. Main activities • Design and implement extensions to programming languages and program logics within proof assistants. • Develop compilation and translation components between multiple representations (source languages, intermediate representations, and architecture descriptions). • Strengthen automated verification tools for the security properties of masked implementations. • Test, validate, document, and integrate developments into the project's open-source repositories. • Present progress and technical results to the consortium partners. Additional activities: • Contribute to the maintenance and overall robustness of the shared tooling. • Participate in the dissemination of project results (public documentation, project website). • Engage with the user community of the project's tools. Skills • Strong background in functional programming, ideally using OCaml (the implementation language of EasyCrypt and Jasmin). Required. • Solid knowledge of programming language theory, including semantics, type systems, language design, or compiler construction. Required. • Experience with a proof assistant, particularly Rocq/Coq (the semantics of the Jasmin compiler are formalized in Rocq/Coq). Strongly preferred. • Familiarity with formal methods and verification frameworks (EasyCrypt, maskVerif). Required or strongly preferred. • Knowledge of hardware security, side-channel attacks, and masking techniques. Desirable (training can be provided on the job). • Familiarity with low-level programming (assembly language, instruction set architectures). A plus. Languages: French or English (reading scientific literature and collaborating within an international consortium). Required. Interpersonal skills: autonomy, attention to detail, ability to collaborate with distributed teams, and strong technical communication skills. Additional desirable qualifications: contributions to open-source projects, experience developing research software, publications, or a PhD in a related field. Benefits package • Restauration subventionnée • Transports publics remboursés partiellement • Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement) • Possibilité de télétravail (après 6 mois d'ancienneté) et aménagement du temps de travail • Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.) • Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria) • Accès à la formation professionnelle • Sécurité sociale Remuneration From 2692 € gross monthly (according to degree and experience) Apply for this position Share • Facebook • Linkedin • Twitter • Email General Information • Theme/Domain : Security and Confidentiality Software engineering (BAP E) • Town/city : Sophia Antipolis • Inria Center : Centre Inria d'Université Côte d'Azur • Starting date : 2026-12-01 • Duration of contract : 2 years • Deadline to apply : 2026-08-30 Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed. Instruction to apply Defence Security : This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment. Recruitment Policy : As part of its diversity policy, all Inria positions are accessible to people with disabilities. Contacts • Inria Team : SPLITS • Recruiter : Grégoire Benjamin / Benjamin.Gregoire@inria.fr The keys to success We are looking for an experienced R&D engineer who is equally comfortable with high-quality software engineering and research-oriented development. The ideal candidate enjoys working with complex codebases, designing reliable and well-structured tools, and continuously learning in a scientifically demanding environment. Rigor, autonomy, curiosity, and the ability to collaborate effectively within a multidisciplinary consortium are essential. A PhD in a related field (formal methods, programming languages, cryptography, or compiler construction) is a strong asset but is not required. About Inria Inria, the French national institute for research in digital science and technology, supports the French government in national research and innovation strategies in the digital field, acting as Digital Programs Agency. Inria leads over 300 research and innovation projects with its 3,500 scientists, engineers, and support staff, in partnership with universities and the digital ecosystem (businesses, entrepreneurs, and public stakeholders). Together, we explore strategic fields such as artificial intelligence, cybersecurity, quantum computing, cloud technologies, digital transformation in healthcare, digital twins, and digital technologies for defence. We develop practical solutions such as software, tech startups, partnerships with national companies, and cutting-edge training programmes. Our goal is to drive scientific, technological, and industrial excellence to ensure France’s digital sovereignty.