Formal methods & programming languages

Research

I work on theorem proving, compiler and operating-system verification, and programming languages.

Research interests

I am interested in theorem proving with Rocq, Isabelle/HOL, and Lean4, compiler/OS formal verification, and programming languages. In particular, my interests include eBPF-related verification and Rust contract specification.

Current research

Compiler implementation & verification

From Rocq to C [CAV'22], and from Isabelle/HOL to Rust [repository].
Just-in-time (JIT) compilation [CAV'24].
EVM ahead-of-time (AOT) compiler (TBC).

OS/VM verification

RIOT-OS rBPF virtual machine [MIDDLEWARE'22] and bootloader [MEMOCODE'21].
Solana blockchain virtual machine [OOPSLA'25].
Linux eBPF [OOPSLA'26].

Model-driven development

AADL / synchronous languages [SCP'21].
AADL2Rust [compiler prototype].

From research to practice

Our research should make real-world software better by finding issues and developing solutions. See my projects and open-source contributions for work on Linux eBPF and Solana, and the publications page for selected papers.