En kunstig sprog bruges til at repræsentere et software krav. Den resulterende formelle krav kan bevises "rigtige" gennem bevis for rigtigheden metoder. Også kendt som kontrollerbare krav sprog.