Keinotekoinen kieli edustaa software vaatimus. Tuloksena virallisten vaatimusten voidaan osoittaa "oikea" todistus oikeellisuudesta menetelmin. Tunnetaan myös nimellä todennettavissa vaatimukset kieli.