Na computação , incluindo o método formal , a segurança (em inglês : safety ) é para um programa não sair de um conjunto de estados. Em particular, excluímos a saída de um conjunto de estados “seguros” (os outros indicam erros).
É com vivacidade uma das duas propriedades teóricas fundamentais dos programas de computador.
Na lógica temporal linear (LTL), ao representar qualquer execução por uma palavra (potencialmente infinita), uma propriedade de segurança é associada a "prefixos ruins" que são palavras finitas que a violam, ou seja, qualquer palavra que comece com tal prefixo viola o dito propriedade. Uma propriedade de segurança é assim caracterizada.