For safety-critical tasks like collision avoidance, formal verification can provide the assurances required to deploy autonomous systems when lives are at stake. Many methods for verifying collision avoidance model a vehicle as a moving point mass, though the real vehicles have nonzero area. Motivated by this gap, our past work proposed a novel algorithm (the ``active corner method'') for verifying collision avoidance for polygonal objects moving in the plane, presented a proof of its correctness, and detailed an automated implementation of the algorithm. This work presents progress towards a certifiable implementation that returns a machine-checkable PVS proof of correctness along with its usual results. This work briefly discusses the proof approach from our original paper, presents a novel approach that leverages simpler geometric intuition, details what we have proven so far in PVS, and lays out our future research goals for this project.