From my shallow understanding, formal verification usually proves the given program always satisfies some properties/specifications. It's pretty good when you e

From my shallow understanding, formal verification usually proves the given program always satisfies some properties/specifications. It's pretty good when you expect the software to fully behave in the way you want it to be. However, in terms of security, usually the loopholes come from those parts or in those ways people didn't see them coming - so how do people write specifications about what they don't know?