Cryptographic performance pressure produces many different cryptographic specifications, and a much larger number of pieces of software trying to make those cryptographic functions run quickly invarious environments. The pre-quantum software ecosystem is already large and complicated but the post-quantum software ecosystem is rapidly shaping up to be much more complicated. We’ve already seen the post-quantum optimization process producing disastrous mistakes that weren’t caught by tests, and at this point we have only a limited understanding of what further mistakes to expect. Fortunately, there are tools to verify that optimizations work for all possible inputs, and there are some cases where these tools have been successfully applied to post-quantum software. This talk will look at what these tools mean for the post-quantum software engineer.