Comment by Animats

> I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code.

This result is exactly the opposite. They're verifying at the machine code level, which is totally imperative.