Designing secure systems is a very difficult task. Even the smallest issues can have devastating consequences. As designers of these systems we have to do everything in our power to ensure that these systems function as intended. Join Aaron as he demonstrates techniques for formally verifying security systems. These tools demonstrate the power of functional languages as verification systems against both functional and imperative software systems. You will learn how to create functional models and use them to prove the correctness of your security systems.