Yan Tong

About

Welcome! I'm Yan, a PhD student at the University of California, Santa Cruz, advised by Professor Lindsey Kuper in the LSD lab. My research sits at the intersection of distributed systems, programming languages, and formal verification, with the goal of making strong correctness guarantees practical for real-world systems.

I'm currently working on Ironwright, a verification framework for distributed systems in Rust. Developers model and implement distributed systems in a Rust-based shallowly embedded DSL, validate them via explicit-state model checking for rapid iteration, and then “intract” formal specifications from Rust to Lean for rigorous verification. The framework will let developers obtain both verified correctness guarantees and deployable code from the same program.

I previously worked on Cykas (“Can you keep a secret?”), a new protocol for sender-side enforcement of causal delivery that sidesteps the conservativeness of the traditional sender-side approach by allowing eager sending of messages and constraining the behavior of their recipients.

I had an internship at Firebase SQL Connect at Google during the summer of 2026, where I worked on supporting strongly-typed SDKs for native SQL. I also interned at Reality Labs at Meta during the summer of 2022, where I worked on an automated framework for their XR data systems.

Yan Tong

About

Publications

Teaching

Professional Service