AI is rapidly becoming the primary author of the world's software. Today's models generate code at a speed no human can match — but how can we trust code we did not write ourselves? Formal verification offers a path to mathematically guaranteed correctness, yet combining it with AI-based code generation raises deep and largely unsolved challenges. As a postdoctoral researcher, you will tackle exactly this question: h…