A formally verified security module for AMD confidential VMs - View it on GitHub