Secure and Verifiable at Full Speed: ExeQuantum’s Hardened and Verified ML-DSA Implementations

The cryptographic community is entering a new phase. With NIST finalising post-quantum cryptography (PQC) standards such as ML-KEM and ML-DSA, the big question is no longer which algorithms to adopt, but how to implement them in ways that are fast, trustworthy, and ready for deployment at scale.

‍At ExeQuantum, we’ve built our entire approach around that challenge. Our guiding framework is STAC — Sovereign, Transparent, Agile, and Compliant — and it underpins everything we develop. Sovereign means our cryptography can be deployed under national or enterprise control. Transparent means we don’t ask customers to trust a black box, but instead provide verifiable assurance. Agile means speed, integration, and adaptability. And Compliant means we align with emerging international standards while being flexible to local regulation.

This month, we are unveiling a milestone: hardened Jasmin implementations of ML-DSA (Dilithium) that are both competitive in performance and formally safety-verified.

There has long been an assumption that hardened cryptographic code must run slower. Our benchmarks show that’s simply not true. Across ML-DSA parameter sets, our hardened implementations perform on par with the reference C code, and in signing operations, they are sometimes faster.

This data tells a clear story. Key generation and verification remain close to baseline speeds, while signing operations see measurable gains. Rather than trading speed for security, our hardened code demonstrates that careful engineering can achieve both.

Of course, speed alone is not enough. Cryptography is only trustworthy if it can be shown to be safe. That is why our Jasmin implementations undergo formal safety verification. This process mathematically analyzes core routines for memory safety issues and similar low-level vulnerabilities that can otherwise hide in plain sight.

For ML-DSA, every critical function, from polynomial arithmetic and norm checks to SHA-3 absorb and squeeze routines, passed with no safety violations detected. To our knowledge, this is among the first times in the PQC field that hardened, production-ready implementations have also been formally validated in this way.

For governments, enterprises, and critical infrastructure operators, PQC adoption isn’t just about compliance. It is about trust. Regulators want assurance that algorithms are implemented safely. Enterprises need performance that won’t slow down their systems. Sovereign adopters demand transparency rather than black-box cryptography.

By pairing performance benchmarks with formal verification, ExeQuantum demonstrates that these needs don’t have to be in conflict. PQC can be fast, safe, and transparent all at once.

This article is only a preview. We will be releasing a full technical white paper in the coming weeks, covering methodology, detailed results across ML-DSA and ML-KEM, and how STAC principles provide a foundation for deployment in finance, cloud, Web3, and government sectors.

The world is walking a tightrope between sovereignty and standardisation. Governments require sovereign assurance. Enterprises need global interoperability. Both demand verifiable trust.

ExeQuantum’s hardened and verified Jasmin implementations of ML-DSA show that this balance is achievable. The post-quantum future will not be defined solely by new algorithms, but by the way they are delivered. With this work, we are setting a higher standard: secure, transparent, and ready for the real world.