No. They have a verificator that can show that two (sub-)programs (more accurately; that an applied transformation preserves semantics) are semantically identic

No. They have a verificator that can show that two (sub-)programs (more accurately; that an applied transformation preserves semantics) are semantically identical. This is a bit like a P-verificator for the solution to a NP-hard problem using a certificate. It can only help you prove that the solution is right, not find new solutions.