Certifying Zero-Knowledge Circuits with Refinement Types. - Junrui Liu; Ian Kretz; Hanzhi Liu; Bryan Tan; Jonathan Wang; Yi Sun; Luke Pearson; Anders Miltner; Isil Dillig; Yu Feng 001 (IACR Cryptol. ePrint Arch., 2023)

FORAY: Towards Effective Attack Synthesis against Deep Logical Vulnerabilities in DeFi Protocols. - Hongbo Wen; Hanzhi Liu; Jiaxin Song; Yanju Chen; Wenbo Guo 002; Yu Feng 001 (CCS, 2024)

Scutum: Temporal Verification for Cross-Rollup Bridges via Goal-Driven Reduction. - Yanju Chen; Juson Xia; Bo Wen; Kyle Charbonnet; Hongbo Wen; Hanzhi Liu; Luke Pearson; Yu Feng 001 (IACR Cryptol. ePrint Arch., 2024)

Push-Button Verification for BitVM Implementations. - Hanzhi Liu; Jingyu Ke; Hongbo Wen; Robin Linus; Lukas George; Manish Bista; Hakan Karakus; Domo; Junrui Liu; Yanju Chen; Yu Feng 001 (IACR Cryptol. ePrint Arch., 2024)

Modular Indexer: Fully User-Verified Execution Layer for Meta-Protocols on Bitcoin. - Hongbo Wen; Hanzhi Liu; Shuyang Tang; Shuhan Cao; Domo; Yu Feng 001 (IACR Cryptol. ePrint Arch., 2024)

Understanding the Linux Kernel, Visually. - Hanzhi Liu; Yanyan Jiang 001; Chang Xu 001 (EuroSys, 2025)

Thunderbolt: A Formally Verified Protocol for Off-Chain Bitcoin Transfers. - Hongbo Wen; Hanzhi Liu; Jingyu Ke; Yanju Chen; Dahlia Malkhi; Yu Feng 001 (IACR Cryptol. ePrint Arch., 2025)