Machine-checking deployed post-quantum signature code (ML-DSA / FIPS 204) against its specification, from the arithmetic up through an eSIM attestation protocol and a capability layer for agent delegation.