Algorithms are usually shown to be correct on paper, but bugs in their
implementations can still lead to incorrect results. In the case of
classical planning, it is fortunately straightforward to check whether
a computed plan is correct. For optimal planning, however, plans are
additionally required to have minimal cost, which is significantly more
difficult to verify. While some domain-specific approaches exists, we
lack a general tool to verify optimality for arbitrary problems. We
bridge this gap and introduce two approaches based on the principle of
certifying algorithms, which provide a computer-verifiable certificate
of correctness alongside their answer. We show that both approaches are
sound and complete, analyze whether they can be generated and verified
efficiently, and show how to apply them to concrete planning
algorithms. The experimental evaluation shows that verifying optimality
comes with a cost, but is still practically feasible. Furthermore, it
confirms that the tested planner configurations provide optimal plans
on the given instances, as all certificates were verified successfully.
