The Cedar policy language for authorization, and verification-guided development methodologies for building high-assurance systems.