Formal verification of system properties is crucial to the security of software systems. Combining the design, implementation, and verification of software systems can produce high-assurance systems. This talk will present two research projects where the modeling and verification play a central role in ensuring the security of the software systems.