Trojan horses are the most devastating weapons to attack a computing system. Traditional operating systems are easily defeated when attacked by means of Trojan horses. Multi-level security (MLS) has been proposed as an alternative security model which can show a much better level of resistance against these attacks. However, MLS models and implementations severely affect the level of usability of the operating system. GIDISS Trusted Linux (GTL) is a project which main goal is to find a way to implement a very usable MLS Linux. In this talk, GTL security model will be presented as well as how it was developed. Also, I will talk about our experience in applying formal methods in the GTL development.