I really like Z3 for showing that my weird bitwise hacks (e.g. [0]) are correct -- it's especially useful that I can show not only that a function is correct, but also that it approximates the correct answer to within whatever bounds I like. Plus, I can put it in a script, and shove it into the docs and tests easily. (Showing that the code actually corresponds to the Z3 equations needs symbolic execution, which I haven't set up yet though...)
[0]: https://doc.stahlos.com/kernel/notebooks/hashtables.html#est...