The intrusion field was introduced by the researcher. It was defined as an attempt or a threat to be the potential possibility of a deliberate unauthorized attempt to access information, manipulate information, or render a system unreliable or unusable. Many intrusions came from internal users. This behavior can cause damage without human intervention: viruses, worms, Trojan horses, etc. In this paper, the authors describe their intrusion detection method in Linux/Unix commands using formal verification. The main features of this paper are twofold. It exploits formal method in the intrusion detection field. It presents their tool TLID which can transform Linux code to symbolic model verifier.