Welcome to Tony's personal website

I’m a software engineer at Databricks, building Spark Declarative Pipelines.

I complete my PhD at the University of Michigan at Ann Arbor, advised by Manos Kapritsos. My research focused on enabling practical automated reasoning for systems software, and I was awarded the 2024 MongoDB PhD Fellowship, and a Jay Lepreau Best Paper Award at OSDI 2025.

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

  • Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. Tony Zhang, Keshav Singh, Tej Chajed, Manos Kapritsos, Bryan Parno. OSDI 2025 [link]. Awarded Best Paper!
  • Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Systems Proofs. Tony Zhang, Travis Hance, Manos Kapritsos, Tej Chajed, Bryan Parno. OSDI 2024 [link]
  • Pilotfish: Distributed Transaction Execution for Lazy Blockchains. Quentin Kniep, Lefteris Kokoris-Kogias, Alberto Sonnino, Igor Zablotchi, Tony Zhang. Financial Cryptography 2025 [link]
  • Performal: Formal Verification of Latency Properties for Distributed Systems. Tony Zhang, Upamanyu Sharma, Manos Kapritsos. PLDI 2023 [pdf]
  • CEP-15: Fast General Purpose Transactions. Benedict Elliott Smith, Tony Zhang, Blake Eggleston, Scott Andreas. Cassandra Enhancement Proposal Whitepaper 2021 [link]
  • Brief Announcement: On the Significance of Consecutive Ballots in Paxos. Eli Goldweber, Tony Zhang, Manos Kapritsos. PODC 2020 [link]

Random

Current leisure pursuits:

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

Profile last updated Aug 2025