I found that even with LLMs making sure the formal specification covers what you actually want is challenging.
How do you actually know what the LLM proved is what you want?
How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.
How do you know any test is checking what you want? You either review it, and/or you run the test on things you know are good and also things you know are bad.