A Formal Proof of PAC Learnability for Decision Stumps. - Joseph Tassarotti; Jean-Baptiste Tristan; Koundinya Vajjha (CoRR, 2019)

Verification of ML Systems via Reparameterization. - Jean-Baptiste Tristan; Joseph Tassarotti; Koundinya Vajjha; Michael L. Wick; Anindya Banerjee 001 (CoRR, 2020)

A formal proof of PAC learnability for decision stumps. - Joseph Tassarotti; Koundinya Vajjha; Anindya Banerjee 001; Jean-Baptiste Tristan (CPP, 2021)

CertRL: formalizing convergence proofs for value and policy iteration in Coq. - Koundinya Vajjha; Avraham Shinnar; Barry M. Trager; Vasily Pestun; Nathan Fulton (CPP, 2021)

Formalization of a Stochastic Approximation Theorem. - Koundinya Vajjha; Barry M. Trager; Avraham Shinnar; Vasily Pestun (ITP, 2022)