> let the LLM generate slop, check it using formal methods

I'm much more bullish on the opposite approach. Perform the naive translation, let the LLM loose on cleaning it up...