Lean 4 library for computable succinct arguments. Did most of the work on commitments (functional and ordinary). Formalized computable lattcies (cyclotomic ring and other lattice primitives) and the notions of special soundness, cooridnate-wise special soundness (CWSS) and the underlying state-tree data structure. Formalized the Ajtai commitment, the KZG and currently formalizing the Hachi PCS.
First formalization of polynomial commitments, the AGM, and the KZG.
See the related ESORICS publication under publications.