Real Vector Spaces and the Cauchy-Schwarz Inequality in ACL2(r). - Carl Kwan; Mark R. Greenstreet (ACL2, 2018)

Convex Functions in ACL2(r). - Carl Kwan; Mark R. Greenstreet (ACL2, 2018)

Towards Formalized Matrix Analysis and Algorithms. - Carl Kwan (ISAIM, 2022)

Automatic Verification of Right-Greedy Numerical Linear Algebra Algorithms. - Carl Kwan; Warren A. Hunt Jr. (FMCAD, 2024)

Formalizing the Cholesky Factorization Theorem. - Carl Kwan; Warren A. Hunt Jr. (ITP, 2024)

Verifying Jolt zkVM Lookup Semantics. - Carl Kwan; Quang Dao; Justin Thaler (IACR Cryptol. ePrint Arch., 2024)

RV32I in ACL2. - Carl Kwan (CoRR, 2025)