Nate Foster

EPFL’s Networked Systems Abstractions Lab (LASeR) is seeking a postdoctoral researcher to work on the design, semantics, implementation, and verification of abstractions for networked systems. The lab’s research sits at the intersection of programming languages, formal methods, and networking, with a focus on making network programming and reasoning more expressive, more precise, and more practical. The successful candidate will contribute to research on one or more of several directions highlighted by the lab: languages and semantics for specifying network behavior, including the NetKAT family and possible quantitative or probabilistic extensions; scalable verification techniques, including symbolic automata and related decision procedures; routing algebras as composable representations of distributed routing protocols and their compilation/verification; formal abstractions for packet scheduling and compilation to programmable hardware; AI-based cybersecurity, including learning from security logs, validating protocol models, and verified defensive controllers. The role is embedded in a collaborative research environment at EPFL, with opportunities to interact with academic and industrial partners and to contribute to open-source tools and artefacts developed in the lab. The position also includes participation in the supervision of PhD and master students and the opportunity to build a strong research network across the programming languages, verification, and networking communities. The lab emphasizes research that connects theory with practical implementation, especially in systems where high-level abstractions must be made efficient enough for real-world use. EPFL offers an international environment with strong support for research and interaction with experts in programming languages, verification, and systems.

The Keystone project at EPFL focuses on building a formally verified ML inference engine at the intersection of formal methods and high-performance systems. The work combines interactive theorem proving with secure computer systems and ML infrastructure, aiming to make verified systems competitive with unverified ones in development effort, features, and performance. The postdoctoral researcher will contribute to the design and construction of a machine-verified LLM inference engine . Possible research directions include formalizing GPU kernel semantics such as PTX or Triton in a proof assistant, verifying high-performance inference kernels, implementing and verifying the inference coordination layer in Rocq or Lean, and developing agentic AI workflows for specification autoformalization, proof generation, and proof repair. The position is part of an ARIA-funded collaboration between EPFL and Imperial College London. The successful candidate will work in a distributed, multi-institution environment with close collaboration with the Imperial team, regular visits to London, engagement with open-source releases of proofs and specifications, and participation in programme activities including red/blue team exercises and sprint reviews. The role is hosted at EPFL and connects to the LASER group, with access to frontier AI models and high-performance compute for proof-assistant workloads. The advert emphasizes a strong research environment in formal verification, systems, and ML infrastructure, plus collaboration with internationally renowned experts and a team of postdoctoral researchers and PhD students.