WormSpace: A Modular Foundation for Simple, Verifiable Distributed Systems. - Ji-Yong Shin; Jieung Kim; Wolf Honoré; Hernán Vanzetto; Srihari Radhakrishnan; Mahesh Balakrishnan 001; Zhong Shao 001 (SoCC, 2019)

From C to interaction trees: specifying, verifying, and testing a networked server. - Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; Wolf Honoré; William Mansky; Benjamin C. Pierce; Steve Zdancewic (CPP, 2019)

Connecting Higher-Order Separation Logic to a First-Order Outside World. - William Mansky; Wolf Honoré; Andrew W. Appel (ESOP, 2020)

Verifying an HTTP Key-Value Server with Interaction Trees and VST. - Hengchu Zhang; Wolf Honoré; Nicolas Koh; Yao Li 004; Yishuai Li; Li-yao Xia; Lennart Beringer; William Mansky; Benjamin C. Pierce; Steve Zdancewic (ITP, 2021)

Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems. - Wolf Honoré; Jieung Kim; Ji-Yong Shin; Zhong Shao 001 (Proc. ACM Program. Lang., 2021)

Adore: atomic distributed objects with certified reconfiguration. - Wolf Honoré; Ji-Yong Shin; Jieung Kim; Zhong Shao 001 (PLDI, 2022)

AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. - Wolf Honoré; Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. - Longfei Qiu; Yoonseung Kim; Ji-Yong Shin; Jieung Kim; Wolf Honoré; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)