Verifying OpenTitan Signature Validation Implementations: C implementation Decrypto implementation Decrypto spec OTBN implementation OTBN spec Calling Convention Research Aspects: Proof Triaging Proof Generation Proposal Related Work