Tony Zhang

Tony Zhang

Distributed sytems,
and the verification thereof

Welcome to Tony's personal website

I’m a software engineer at Databricks, building our next-gen declarative ETL framework.

I complete my PhD at the University of Michigan at Ann Arbor, advised by Manos Kapritsos. My PhD thesis focused on enabling practical automated reasoning for systems software, and I was awarded the 2024 MongoDB PhD Fellowship for my research.

These days, I think about how LLMs can drive the practicality and adoption of formal methods, and how formal methods can enable more reliable LLM reasoning.

Outside of verification, I am broadly interested in all facets of distributed systems. For instance, I designed a leaderless multi-partition transaction protocol for Apache Cassandra, and contributed to a PODC paper proving that Lamport’s interpretation of the Paxos algorithm was strictly stronger than necessary. Additionally, I worked with Mysten Labs to build a distributed execution engine for the Sui blockchain.

Publications and Technical Reports

  • Tony Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, Bryan Parno. Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. In Proceedings of the 19th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2025) [link]. Awarded Best Paper!
  • Tony Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, Bryan Parno. Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Systems Proofs. In Proceedings of the 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI 2024) [link]
  • Quentin Kniep, Lefteris Kokoris-Kogias, Alberto Sonnino, Igor Zablotchi, Tony Zhang. Pilotfish: Distributed Transaction Execution for Lazy Blockchains. Tech Report (2024) [link]
  • Tony Zhang, Upamanyu Sharma, Manos Kapritsos. Performal: Formal Verification of Latency Properties for Distributed Systems. In Proceedings of the 44th ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI 2023) [pdf]
  • Benedict Elliott Smith, Tony Zhang, Blake Eggleston, Scott Andreas. CEP-15: Fast General Purpose Transactions. Cassandra Enhancement Proposal Whitepaper (2021) [link]
  • Eli Goldweber, Tony Zhang, Manos Kapritsos. Brief Announcement: On the Significance of Consecutive Ballots in Paxos. 39th ACM Symposium on Principles of Distributed Computing (PODC 2020) [link]

Random

Current leisure pursuits:

  • 🏂 Snowboarding
  • 🏎 Sim racing and watching F1
  • 🏸 Badminton

Profile last updated Aug 2025