Postdoc: Keystone Project (Machine-Verified LLM Inference)

This postdoctoral position at EPFL is for the Keystone Project, focused on formally verifying large language model (LLM) inference engines. Responsibilities include research on machine-checked verification of systems software, GPU kernel semantics, and AI-assisted proof engineering. Candidates require a PhD in computer science or a related field, with expertise in formal verification, programming languages, systems, or ML.

• Independent, creative, and solution-oriented
• Excellent written and oral communication skills in English
• 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
• 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
• 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
• 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