What we haven't done yet is formal verification with dudect or ctgrind — that's planned for the security audit we're coordinating through OSTIF. Side-channel properties of the PQC lattice ops (ML-KEM, ML-DSA) are also still an open area for us
Thank you for the interest.
PIN comparison uses subtle::ConstantTimeEq, RSA signing has randomized blinding, ECDSA goes through constant-time point multiplication in p256/p384, all key material is ZeroizeOnDrop + mlock'd for its lifetime, and AES uses hardware AES-NI when available (bitsliced fallback to avoid cache-timing on lookup tables).