Brief Announcement: On the Significance of Consecutive Ballots in Paxos. - Eli Goldweber; Nuda Zhang; Manos Kapritsos (PODC, 2020)

On the Significance of Consecutive Ballots in Paxos. - Eli Goldweber; Nuda Zhang; Manos Kapritsos (CoRR, 2020)

Performal: Formal Verification of Latency Properties for Distributed Systems. - Tony Nuda Zhang; Upamanyu Sharma; Manos Kapritsos (Proc. ACM Program. Lang., 2023)

Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs. - Tony Nuda Zhang; Travis Hance; Manos Kapritsos; Tej Chajed; Bryan Parno (OSDI, 2024)

Pilotfish: Distributed Transaction Execution for Lazy Blockchains. - Quentin Kniep; Lefteris Kokoris-Kogias; Alberto Sonnino; Igor Zablotchi; Nuda Zhang (CoRR, 2024)

Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols. - Tony Nuda Zhang; Keshav Singh; Tej Chajed; Manos Kapritsos; Bryan Parno (OSDI, 2025)