I have also found that equivalent rewrites are one of the best applications for formal. Other examples can be things like vectorizing code while proving the vec

I have also found that equivalent rewrites are one of the best applications for formal. Other examples can be things like vectorizing code while proving the vectorized version is formally identical, refactoring types or objects, or select classes of performance optimization that are not expected to change the output.