Il processo di utilizzo di prove formali per dimostrare la consistenza (verifica progettuale) tra una specifica formale di un sistema e un modello di politica di sicurezza formale o (verifica dell'attuazione) tra la specifica formale e la sua attuazione del programma.