A description of specific behaviors or security policies using formal languages, thus enabling the correctness of those behaviors/policies to be formally proven.
Sources:
CNSSI 4009-2015