> How to prove the correctness of the mathematical specification? You can show that your specifications satisfy well-accepted criteria like confidentiality and

> How to prove the correctness of the mathematical specification? You can show that your specifications satisfy well-accepted criteria like confidentiality and integrity. This is usually done as the final verification step. For example, AWS just did it for the Nitro hypervisor used by EC2: https://aws.amazon.com/blogs/compute/aws-nitro-isolation-engine-formally-verifying-the-hypervisor-in-the-aws-nitro-system https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng....