v0.7.0 — a proof tier (Z3)

Sampling says "no counterexample found over N inputs"; a solver says "no counterexample exists". This adds the second.

Added

• prove_equiv claim (Z3): proves two integer expressions equal for all inputs over bit-vector logic, or refutes with a distinguishing input — verifying MBA deobfuscation. (x^y)+2*(x&y) is proven equal to x+y for every 64-bit input; x^y==x+y is refuted with a counterexample.
• Z3 as an optional backend: pip install "reverify[z3]" (or [full]); INCONCLUSIVE without it.

Honest strength ladder: proven > tested > observed. 176 tests. pip install -U reverify