<title of image as alt>

Tobias Rothmann

I am a master’s student in computer science at TUM, interested in formal methods, cryptography, and especially their intersection.

I just finished my internship at the Ethereum Foundation, where I worked with the team on (almost) end-to-end formal verification of post-quantum lattice-based polynomial commitments (from Rust to security proofs).

During my undergraduate studies, I was fortunate to be supervised by Prof. Tobias Nipkow (co-author of the Isabelle proof assistant). I worked on ArkLib in Lean at EPFL in the lab of Alessandro Chiesa (with Christian Knabenhans) and I have also worked on the cryptography team at Arcium.
Publications Talks Projects Hackathons Events

Publications

“On the Formal Verification of Polynomial Commitments: two KZG constructions and the Algebraic Group Model”.
Tobias Rothmann.
ESORICS 2026 (Best Paper Award Nominee). Available at: IACR eprints | AFP entry | slides

“Formal Verification of the Kate-Zaverucha-Goldberg Polynomial Commitment Scheme”.
Tobias Rothmann, Katharina Heidler (b. Kreuzer).
IEEE FCS2024 Workshop. Available at: FCS Workshop

Talks

“Functional Commitments and the KZG in ArkLib/Lean”.
ZKProof 8 slides | recording

“On the Formal Verification of Polynomial Commitment Schemes: the KZG and beyond”.
ZKProof 7. slides | recording

“Formally Verifying the KZG Polynomial Commitment Scheme”.
0xCastle. slides

Projects

Verified-zkEVM/ArkLib on GitHub
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.
tobias-rothmann/Polynomial-Commitment-Schemes on GitHub
First formalization of polynomial commitments, the AGM, and the KZG. See the related ESORICS publication under publications.

We might have met at..

2026

2025

2024

2023