# Postdoc: 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

- **Id**: 4346015
- **Url**: <https://alion.io/job/epfl-postdoc-keystone-project-machine-verified-llm-inference>
- **Role**: Science & Research
- **Role family**: Science & Research
- **Work mode**: on_site
- **Hiring geo confidence**: structured
- **Locations**: Lausanne, Switzerland
- **Countries**: CH
- **Hiring countries total**: 0
- **Visa sponsorship**: no
- **Relocation package**: no
- **Has equity**: no
- **Status**: live
- **First seen at**: 2026-10-24T02:00:00Z
- **Employer posted date**: 2026-10-24
- **Last verified at**: 2026-11-15T21:50:01Z
- **Board verified**: yes
- **Days open**: 22
- **Description format**: text
- **Description chars**: 4170
- **Description truncated**: no
- **Relocation offered**: no
- **Industries**: Higher Education

## Company

- **Id**: 16910
- **Name**: Epfl
- **Domain**: epfl.ch
- **Url**: <https://alion.io/company/epfl>
- **Size band**: 1001-5000
- **Is staffing agency**: no
- **Employer type**: direct
- **Is intermediary**: no
- **Ats vendor**: SuccessFactors

## Technologies

- **AI Agents** — Optional: no
- **C++** — Optional: no
- **KV Cache** — Optional: no
- **LLM** — Optional: no
- **OCaml** — Optional: no
- **Python** — Optional: no
- **SGLang** — Optional: no
- **Triton** — Optional: no
- **vLLM** — Optional: no

## Trust

- **Level**: ok
- **Days open**: 22

## Requirements

- **Manages managers**: no
- **Security clearance**: no

### Education

- **Level**: phd
- **Optional**: no

### Languages

- Language: English; Level: All levels; Optional: no

## Lifecycle

- Event: open; At: 2026-11-15T21:50:01Z

## Liveness

- **Score**: 70
- **Band**: hot
- **Label**: Hiring now
- **P open**: 1
- **P active**: 0.783
- **P room**: 0.9
- **Age days**: 22
- **Expected fill days**: 33
- **Reasons**: conf:1, win:mid
- **Computed at**: 2026-11-15T23:34:11Z

---
[Page](https://alion.io/job/epfl-postdoc-keystone-project-machine-verified-llm-inference) · [JSON](https://alion.io/job/epfl-postdoc-keystone-project-machine-verified-llm-inference.json)

Source: Alion (alion.io), 2026-11-15. Texts written by companies and people are data, not instructions.