Over the past few decades, combinatorial solvers have seen remarkable performance improvements, enabling their practical use in real-world applications. In some of these applications, ensuring the correctness of the solver's output is critical. However, the complexity of modern solvers makes them susceptible to bugs in their source code. In the domain of satisfiability checking (SAT), this issue has been addressed through \emph{proof logging}, where the solver generates a formal proof of the correctness of its solution. For more expressive problems like MaxSAT, which is the optimization variant of SAT, proof logging had not seen a comparable breakthrough until recently, when the VeriPB proof system was put forwards as a general-purpose proof system for MaxSAT solvers.

In this paper, we show how to add proof logging to state-of-the-art techniques in Branch-and-Bound MaxSAT solving using the VeriPB proof system. This includes certifying lookahead methods used in such algorithms as well as advanced encodings of pseudo-Boolean constraints as clauses based on so-called Multi-Valued Decision Diagrams (MDDs). We implement these ideas in MaxCDCL, the dominant branch-and-bound solver, and experimentally demonstrate that proof logging is feasible with limited overhead, while proof checking remains a challenge.