You let the AI generate it. Apparently it becomes quite good at proving things. Here is a some effort: https://www.anthropic.com/research/formal-verification (but this is on generated RISC-V code)