IIRC there was another paper recently, with similar methodology about computing xAx. These papers produce algorithms which aren't empirically correct, but provably correct. They do this by operating on a graph data structure, which describes the algorithm and then verifying the algebraic equality to the correct result.

There is a substantial difference here. And I think utilizing algorithms which only are empirically correct can be dangerous.