Един изкуствен език, използван за представяне софтуер изискване. Резултат формални изисквания може да се докаже "правилно" чрез методи за доказване на коректност. Също така известен като доказуеми изисквания език.