Formal methods · Programming languages

About me

I am Shenghao Yuan, a researcher at Zhejiang University. My research focuses on formal verification of compilers, operating systems, and virtual machines.

I work at the State Key Laboratory of Blockchain and Data Security and the Hangzhou High-Tech Zone (Binjiang) Institute of Blockchain and Data Security. I am particularly interested in eBPF-related verification and Rust contract specification.

I received my Ph.D. in Computer Science from Université de Rennes / Inria-Rennes in 2023, advised by Jean-Pierre Talpin and Frédéric Besson.

News

View all news →

Research interests

Explore research →

Compiler implementation & verification — verified compilation and just-in-time compilers.
OS & virtual machine verification — from embedded eBPF to Solana and Linux.
Theorem proving & programming languages — Rocq, Isabelle/HOL, Lean 4, and Rust.

Selected publications

View publication list →

Research in practice

Projects & contributions →

Our research should make real-world software better: finding issues and developing solutions.

My work includes Linux eBPF patches, Solana VM contributions, and formal verification of Rust through the TRust² project.