陈霄泓 · Xiaohong Chen

• ✉
• 𝕏
• ✈
• in

Welcome. My current direction is certifying AI: how AI systems can produce computational results with independently checkable certificates, rather than asking people to trust the model alone.

This direction is grounded in formal methods — logic, programming languages, formal semantics, formal verification, and proof generation.

I'm the CTO of pi2labs.org and fast.xyz. I also work on FastSet, a protocol for parallel claim settlement, and on high-performance decentralized and distributed systems.

Bio

• 2024–presentCTOpi2labs.org and fast.xyz
• 2023–2024Research EngineerRuntime Verification Inc.
• 2016–2023PhDUniversity of Illinois Urbana-Champaign
• 2015–2016Research AssistantSingapore University of Technology and Design
• 2014–2015Assistant LecturerBirmingham City University
• 2010–2014BScPeking University

Selected Publications

• Matching μ-logic.
  Xiaohong Chen.
  PhD Thesis, University of Illinois Urbana-Champaign, 2023.

• A Unifying Logical Foundation for Initial Algebra Semantics and Induction.
  Xiaohong Chen, Dorel Lucanu, Grigore Rosu.
  Theoretical Computer Science, 2026. [DOI]
• FastSet: Parallel Claim Settlement.
  Xiaohong Chen, Grigore Rosu.
  arXiv preprint, 2025. [arXiv]
• Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier.
  Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu.
  OOPSLA 2023. [DOI]
• Towards a Trustworthy Semantics-Based Language Framework via Proof Generation.
  Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu.
  CAV 2021. [DOI]
• A General Approach to Define Binders Using Matching Logic.
  Xiaohong Chen, Grigore Rosu.
  ICFP 2020. [DOI]
• Towards a Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic.
  Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Rosu.
  OOPSLA 2020. [DOI]
• Matching μ-Logic.
  Xiaohong Chen, Grigore Rosu.
  LICS 2019. [DOI]

View all publications →