EPFL (the Swiss Federal Institute of Technology in Lausanne) is inviting applications for an outstanding Postdoctoral Researcher to join the high-profile, ARIA-funded Keystone Project. This collaborative initiative between EPFL and Imperial College London aims to build a formally-verified ML inference engine, proving that artificial intelligence can assist in making verified systems highly competitive with unverified systems in terms of performance, features, and development effort.
This is an exceptional opportunity for researchers at the intersection of formal methods, programming languages, and machine learning infrastructure to conduct state-of-the-art research in a world-class scientific environment.
Job Overview & Key Details
| Designation | Postdoctoral Researcher (Postdoc) |
| Research Area | Formal Verification, Interactive Theorem Proving (Rocq, Lean), GPU Semantics, ML Infrastructure |
| Location | EPFL, Lausanne, Switzerland (with regular travel to London) |
| Contract Type | CDD (Fixed-Term), 100% Activity Rate |
| Duration | 1 year, renewable (subject to project duration) |
| Start Date | December 1, 2026 (or to be determined) |
| Reference Number | 2476 |
Research Area & Project Mission
The Keystone Project focuses on pushing the boundaries of secure and high-performance computer systems through rigorous formal verification. Key areas of interest include:
- Machine-checked verification of systems software.
- GPU kernel semantics and verification.
- AI-assisted proof engineering.
The project aims to demonstrate that AI-driven development and interactive theorem proving (using tools like Rocq or Lean) can produce ML inference systems that are both highly secure and optimized for real-world deployment.
Job Description & Main Responsibilities
The successful candidate will play a pivotal role in the design and construction of a machine-verified LLM inference engine. Specific duties include:
- Core Research & System Verification: Conducting research tailored to the candidate’s background. Possible pathways include:
- Formalizing GPU kernel semantics (e.g., PTX/Triton) in a proof assistant and verifying high-performance kernels for numerical accuracy, memory safety, data race freedom, and functional correctness.
- Implementing and verifying the inference coordination layer (batching, KV-cache management, and scheduling) in Rocq/Lean, with extraction to executable code.
- Developing agentic AI workflows for specification autoformalization, proof generation, and proof repair.
- Collaboration: Collaborating closely with the co-investigators and researchers at Imperial College London (requires regular visits to London).
- Open-Source Contributions: Contributing to open-source releases of specifications, verified artifacts, and proofs.
- Project Engagement: Participating in ARIA program activities, including sprint reviews and red/blue team exercises.
Eligibility & Qualifications
Applicants must meet the following criteria to be considered for the position:
- Education: A PhD (completed or nearing completion) in Computer Science or a closely related field.
- Core Expertise: A strong background in formal verification, programming languages, systems, or machine learning.
- Technical Experience: Research experience in one or more of the following:
- Interactive theorem proving (e.g., Rocq/Coq, Lean, HOL, Isabelle).
- GPU programming or semantics, compilers, concurrency, or ML systems (e.g., vLLM, SGLang, or similar inference engines).
- Software Engineering: Strong computational and analytical skills with proficiency in multiple languages (e.g., Python, C++, OCaml, or functional languages).
- Preferred Skills: Experience using or evaluating LLM-based tools for code/proof generation is highly desirable.
- Soft Skills: Excellent written and oral communication skills in English, a solution-oriented mindset, and a collaborative team spirit.
- Publications: A strong publication record relative to career stage in leading international journals and conferences.
What We Offer
- An internationally competitive salary and excellent working conditions.
- A stimulating research environment at EPFL, one of Europe’s top-ranked universities.
- Generous access to frontier AI models and high-performance computing resources.
- Fully funded travel for research collaboration between Lausanne and London, as well as for international conferences.
- The opportunity to collaborate with world-renowned experts at both EPFL and Imperial College London.
How to Apply
Interested candidates must submit their application online through the official EPFL careers platform. The application should include the following documents:
- A brief Cover Letter (PDF format, up to 2 pages).
- A single consolidated PDF containing:
- An updated Curriculum Vitae (CV) including a full publication list.
- A Research Statement (up to 3 pages).
- Contact details of three academic referees.
For scientific or role-specific inquiries, contact Nate Foster at nate.foster@epfl.ch. For general group information, visit the EPFL LASER Laboratory website.
Last Date to Apply
Applications are reviewed on a rolling basis. Candidates are encouraged to apply as early as possible to ensure full consideration.
