Un langage de spécification avec des constructions spéciales et, parfois, des protocoles de vérification, permettant de développer, analyser et documenter les exigences matérielles ou logicielles.