<b>Our work on Formally Certified Approximate Model Counting</a> has been accepted to <a href="http://www.i-cav.org/2024/">CAV 2024</a>.</b> <br> We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm&apos;s PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC&apos;s calls to an external CNF-XOR solver using proof certificates. <br> Authors: Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel<br>