An artificial language used to represent a software requirement. The resulting formal requirements can be proven "correct" through proof-of-correctness methods. Also known as verifiable requirements language.