Help us build the next generation of verification tools by bringing cutting-edge proof assistant technology to bear on real-world Rust programs.
Job description
Software is at the core of modern society — from communication networks and financial systems to medical devices and transport infrastructure — and ensuring that it behaves correctly is both essential and notoriously difficult. Proof assistants such as Agda and Rocq (formerly Coq) make it possible to construct mathematically rigorous, machine-checked guarantees about software behaviour, but applying them to programs written in mainstream languages remains a significant challenge. This is especially true for software that exhibits cyclic behaviour: programs with loops, recursive data, or continuous interaction with their environment, which require a careful interplay of inductive and coinductive reasoning to verify.
In this postdoc position, you will work at the intersection of proof assistants and modern systems programming. Your central task is to design and prototype a way to verify Rust programs — and in particular programs with cyclic structures — by translating them, together with logical annotations supplied by the developer, into a proof assistant where their correctness can be machine-checked. The aim is not to build yet another verification tool from scratch, but to make state-of-the-art research on inductive-coinductive type theory genuinely usable for Rust developers. You will work closely with a parallel PhD project on first-class coinduction in proof assistants, helping to refine the underlying type theory and putting it to the test on realistic Rust programs.
This position is part of the NWO-XL consortium project Cyclic Structures in Programs and Proofs: New Harmonies in Software Correctness by Construction, a collaboration between five Dutch universities (TU Delft, Groningen, Leiden, Nijmegen, and Twente) which brings together expertise in formal logic, programming language theory, concurrency, and proof assistants. You will be based at TU Delft in the Programming Languages group, supervised by Jesper Cockx, and will collaborate closely with the other PhD students, postdocs, and senior researchers in the consortium. Within the wider project, your work forms a bridge between foundational research on coinductive reasoning and its practical application to real programs, and as such will play a key role in demonstrating that the consortium's theoretical advances translate into concrete tools that practitioners can use.
You will have significant freedom to shape the technical agenda, publish your findings at leading venues (such as POPL, ICFP, OOPSLA, ITP, and CPP), and contribute to the open-source tools developed within the consortium. You will also be encouraged to spend time at one of the partner universities and to engage with the broader national and international research community via the NetTCS network and consortium-organised workshops and schools.
Job requirements
- A PhD in computer science, mathematics, or a closely related discipline (obtained or expected to be obtained before the starting date)
- Solid experience using a proof assistant such as Agda, Rocq, or Lean, ideally for non-trivial formalisations or for research on the proof assistant itself
- A strong background in type theory and/or programming language theory, including familiarity with topics such as dependent types, type systems for program verification, or operational/denotational semantics
- The ability to conduct independent research, demonstrated by peer-reviewed publications at relevant international venues
- Good written and spoken English, and the communication skills needed to collaborate effectively within a multi-site consortium
TU Delft (Delft University of Technology)
Delft University of Technology is built on strong foundations. As creators of the world-famous Dutch waterworks and pioneers in biotech, TU Delft is a top international university combining science, engineering and design. It delivers world class results in education, research and innovation to address challenges in the areas of energy, climate, mobility, health and digital society. For generations, our engineers have proven to be entrepreneurial problem-solvers, both in business and in a social context.
At TU Delft we embrace diversity as one of our core values and we actively engage to be a university where you feel at home and can flourish. We value different perspectives and qualities. We believe this makes our work more innovative, the TU Delft community more vibrant and the world more just. Together, we imagine, invent and create solutions using technology to have a positive impact on a global scale. That is why we invite you to apply. Your application will receive fair consideration.
Challenge. Change. Impact!
Faculty of Electrical Engineering, Mathematics and Computer Science
The Faculty of Electrical Engineering, Mathematics and Computer Science (EEMCS) brings together three scientific disciplines. Combined, they reinforce each other and are the driving force behind the technology we all use in our daily lives. Technology such as the electricity grid, which our faculty is helping to make completely sustainable and future-proof. At the same time, we are developing the chips and sensors of the future, whilst also setting the foundations for the software technologies to run on this new generation of equipment – which of course includes AI. Meanwhile we are pushing the limits of applied mathematics, for example mapping out disease processes using single cell data, and using mathematics to simulate gigantic ash plumes after a volcanic eruption. In other words: there is plenty of room at the faculty for ground-breaking research. We educate innovative engineers and have excellent labs and facilities that underline our strong international position. In total, more than 1000 employees and 4,000 students work and study in this innovative environment.
, Mathematics and Computer Science.
Conditions of employment
- Duration of contract is 2 years Temporary
- A job of 36-40 hours per week.
- Salary and benefits are in accordance with the Collective Labour Agreement for Dutch Universities.
- An excellent pension scheme via the ABP.
- The possibility to compile an individual employment package every year.
- Discount with health insurers on supplemental packages.
- Flexible working week.
- Every year, 232 leave hours (at 38 hours). You can also sell or buy additional leave hours via the individual choice budget.
- Plenty of opportunities for education, training and courses.
- Partially paid parental leave
- Attention for working healthy and energetically with the vitality program.
Will you need to relocate to the Netherlands for this job? TU Delft is committed to make your move as smooth as possible! The HR unit, Coming to Delft Service, offers information on their website to help you prepare your relocation. In addition, Coming to Delft Service organises events to help you settle in the Netherlands, and expand your (social) network in Delft. A Dual Career Programme is available, to support your accompanying partner with their job search in the Netherlands. .
Additional information
If you would like more information about this vacancy or the selection procedure, please contact Jesper Cockx, via [email protected].
Application procedure
Are you interested in this vacancy? Please apply no later than 1 July 2026 upload the following documents:
You can address your application to Jesper Cockx.
Please note:
- You can apply online. We will not process applications sent by email and/or post.
- As part of knowledge security, TU Delft conducts a risk assessment during the recruitment of personnel. We do this, among other things, to prevent the unwanted transfer of sensitive knowledge and technology. The assessment is based on information provided by the candidates themselves, such as their motivation letter and CV, and takes place at the final stages of the selection process. When the outcome of the assessment is negative, the candidate will be informed. The processing of personal data in the context of the risk assessment is carried out on the legal basis of the GDPR: performing a public task in the public interest. You can find more information about this assessment on our website about knowledge security.
- Please do not contact us for unsolicited services.
