Keystone Project (Machine-Verified LLM Inference)

Mission

The Keystone project seeks to advance knowledge in the following domains:

• Formal verification and interactive theorem proving (Rocq, Lean)

• Secure and high-performance computer systems, including ML infrastructure

We seek outstanding candidates working in formal methods and/or computer systems with interests in one or more of the following areas: machine-checked verification of systems software, GPU kernel semantics and verification, and AI-assisted proof engineering.

The position is part of an ARIA-funded collaboration between EPFL and Imperial College London whose goal is to build a formally-verified ML inference engine, demonstrating that AI can help make verified systems competitive with unverified systems  in terms of development effort, features, and performance.

Main duties and responsibilities

• Conducting research related to the Keystone project, including contributing to the design and construction of a machine-verified LLM inference engine. The precise focus will be discussed with the successful candidate depending on their background, expertise and affinities. Possible directions include:

  • Formalizing GPU kernel semantics (e.g., PTX/Triton) in a proof assistant and verifying high-performance inference kernels (numerical accuracy, memory safety, data race freedom, functional correctness)

  • Implementing and verifying the inference coordination layer (batching, KV-cache management, scheduling) in Rocq/Lean, with extraction to executable code

  • Developing agentic AI workflows for specification autoformalization, proof generation, and proof repair

• Build a strong network in the fields of formal verification, systems, and ML infrastructure, including close collaboration with the Imperial College London team (regular visits to London are expected)

• Contribute to open-source releases of specifications, proofs, and verified artefacts

• Engage with the ARIA programme, including red/blue team exercises and sprint reviews

Profile

• PhD (or nearing completion of) in computer science or a closely related field

• Background in formal verification, programming languages, systems, or ML

• Research experience in one or more of: interactive theorem proving (Rocq, Lean, HOL, Isabelle, or similar), GPU programming or semantics, compilers, concurrency, or ML systems (e.g., vLLM, SGLang, or similar inference engines)

• Strong computational and analytical skills, including solid software engineering ability across multiple languages (e.g., Python, C++, OCaml, functional languages)

• Experience using or evaluating LLM-based tools for code or proof generation is a plus

• Publication record (relative to your career stage) in internationally leading journals and conferences

• Independent, creative, and solution-oriented

• Excellent written and oral communication skills in English

• Strong motivation to explore new research domains at the intersection of AI and formal methods

• Good team spirit and enthusiasm for working in a distributed, multi-institution team

We offer

• A stimulating and international working environment

• Excellent working conditions 

• Opportunity to perform state-of-the-art research in one of the most dynamic scientific institutions in Europe, within a high-profile ARIA-funded project

• Opportunity to interact with internationally renowned experts at EPFL and Imperial College London, and with a strong team of postdoctoral researchers and PhD students

• Generous access to frontier AI models and high-performance compute for proof-assistant workloads

• Funded travel for collaboration between Lausanne and London, and for conferences

Informations

Only applications submitted through the online platform are considered. You are asked to supply:

• A brief cover letter (pdf, up to 2 pages).

And in one PDF:

• A CV with a publication list.

• A research statement (pdf, up to 3 pages).

• Contact details for 3 referees.

For any further information, please contact: Nate Foster (nate.foster@epfl.ch). 

More information can be found on https://laser.epfl.ch/.

Contract Start Date : 01.12.2026, or to be determined 

Activity Rate : 100.00 

Contract Type: CDD

Duration: 1 year, renewable (project duration permitting) 

Reference: 2476