First you need to write these specifications and if you say just tell the llm to write them - then how would it be different from just tell the llm to write the program?

I guess you can argue that these are two independent processes so you can combine them to get something more reliable than both - this might be a viable path. But from what I heard writing formal specifications is just really hard - I haven't seen anything practical in this area.