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.

My current work focuses on distributed systems refinement, a technique for formally verifying that real-world system implementations satisfy their intended designs. Instead of proving correctness directly on complex production code, we (1) verify a simpler abstraction of the system, and (2) prove that the implementation does not exhibit behaviors that are disallowed by the abstraction (i.e., the implementation matches the abstraction). Step (2) is known as refinement. I study how programming language techniques can help refine real-world implementations and how to design abstractions that can be systematically developed into low-level, high-performance, production-ready distributed systems.

I have also worked on causality (causal ordering), an important safety property in distributed systems. In this work, I modified the buffer protocol to improve message delivery efficiency and reduce unnecessary delays between message sending and delivery.

I had an internship 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