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