i agree, i wrote a z3 skills for claude and generate a proof before writing code