Formal techniques applied to computer security, including formal specification language for security properties, security analysis utilities, domain-specific security concerns, and case studies of formally verified secure systems.