When a certifying solver claims that a solution is optimal or that a problem is unsatisfiable, it demonstrates this convincingly by giving a proof log which can be checked by an independent (and ideally formally-verified) proof checker. Such an approach should also be viable for enumeration problems ("I have listed all solutions explicitly") and counting problems ("there are exactly 42 solutions"), but the currently most popular proof logging systems contain several vital features which are incompatible with this goal. We explain how the VeriPB system can be modified for enumeration and counting proofs whilst retaining as much as possible of its powerful "strengthening" and "deletion" features. We implement this extension both inside VeriPB's user-friendly proof checker and elaborator, and the formally verified CakePB backend, and use this to obtain formally verified enumerations of solutions for a range of constraint solving and graph problem instances.