Intel Trust Domain Extensions (TDX) is the next-generation confidential computing offering of Intel. One of the most critical processes of Intel TDX is the remote attestation mechanism. Since remote attestation bootstraps trust in remote applications, any vulnerability in the attestation mechanism can therefore impact the security of an application. Hence, we investigate the use of formal methods to ensure the correctness of the attestation mechanisms. The symbolic security analysis of remote attestation protocol in Intel TDX reveals a number of subtle inconsistencies found in the specification of Intel TDX that could potentially lead to design and implementation errors as well as attacks. These inconsistencies have been reported to Intel and Intel is in process of updating the specifications. We also explain how formal specification and verification using ProVerif could help avoid these flaws and attacks.