Overview
We are looking for applicants for a Postdoc position on the
Development of an EasyCrypt compatible Lean library (AI-supported)
at the Chair for Quantum Information Systems under the supervision of Dominique Unruh.
Computer-verified cryptographic proofs (e.g., in tools such as EasyCrypt) give us high assurance that a cryptographic scheme is secure. But the tools themselves are large and complex, and a bug in the tool can invalidate the proofs it checks. A way around this is a foundational approach: the whole proof is ultimately reduced to a small, trusted logical core (a kernel) that can be scrutinized and trusted on its own, with everything else producing certificates the kernel re-checks.
The focus of this position is the implementation of such a core cryptographic logic in Lean 4: formalizing the ambient and program logics that underlie cryptographic reasoning (e.g., probabilistic relational Hoare logic with adversaries and oracles), proving them sound, and building the machinery that checks cryptographic proof artifacts against this kernel, as well as the development/transfer of actual cryptographic proofs. We expect massive AI use for developing the proofs, but human oversight/verification of all critical components/definitions. This is one part of a larger, international effort to put cryptographic verification on a foundational footing, and you would work closely with EasyCrypt developers driving the other parts of that process.
How to apply?
Deadline for applications is Aug 15, 2026. (Earlier is better, and later applications may be considered as long as this webpage is up.)
Please see the general application instructions for Postdocs.
Required profile
Candidates must have (or soon obtain) a PhD in Computer Science, Mathematics, or a related area, and have completed their studies with excellent grades. Experience with an interactive theorem prover (ideally Lean, but Rocq/Coq, Isabelle, or similar also count), and/or with the semantics of program logics or formal cryptographic verification, is strongly desirable. Experience with using AI in proof development is also strongly desirable.
You should have interest in performing original, highly competitive scientific research, publishing your results in top conferences and scientific journals. Self-motivation and the ability to work both independently and as a team player in local and international research groups are expected. Fluency in English is required; it is the main language of communication at the group.
Duration
The position is fixed-term until November 2027, with the possibility of extension through follow-up projects.
What do we offer? We offer a stimulating international research environment, the possibility to participate in highly competitive and interdisciplinary research and the opportunity to involve students in your research through project work. Postdoctoral researchers have a status as full-time employee with a salary according to the German federal employee scale TV-L E13; the exact salary is subject to your family situation. (Inofficial description of this scale)
RWTH Aachen University offers excellent facilities for professional and personal development.
RWTH Aachen University is certified as a “Family-Friendly University”. We particularly welcome and encourage applications from women, non-binary persons, disabled persons and ethnic minority groups, recognizing they are underrepresented across RWTH Aachen University. The principles of fair and open competition apply and appointments will be made on merit.