If it is formal, you don't need LLM.

If you need LLM, it is not formal.

Formal software are not LLMs.

LLMs/agents can use formal software.

The limit of formal software is the formal model itself, roughly speaking the binary specification is designed by humans. If the formal model is "wrong", bravo, you have formally proven a "wrong" model...