rebuilding site Mon Aug 19 11:55:52 CEST 2024

post/fospqc/index.html

@@ -260,7 +260,7 @@ <h2 class="display-1 fw-bold text-center text-primary pb-3">Formally Verified Po
 <p>At Cryspen, we have been developing formally verified open-source implementations of post-quantum cryptographic algorithms in Rust using the <a href="https://cryspen.com/hax/">hax toolchain</a>. Our implementations are verified to be <a href="https://cryspen.com/post/ml-kem-verification/">panic free, functionally correct, and secret independent</a>. Indeed, our verification of Kyber already <a href="https://cryspen.com/post/ml-kem-implementation/">uncovered vulnerabilities</a> that were found to be present and <a href="https://eprint.iacr.org/2024/1049">exploitable</a> in multiple Kyber implementations.</p>
 <p>We have been working with Mozilla to upstream our verified implementations into the NSS cryptographic library.
 We are also contributing our Rust code to the <a href="https://github.com/pq-code-package">PQCP project</a> hosted by the <a href="https://pqca.org/">Post Quantum Crypto Alliance</a>.</p>
-<p>And now, we are happy to announce that we are also <a href="https://bughunters.google.com/blog">partnering with Google</a> to develop formally verified open-source implementations of the NIST standards that can be consumed not only by organizations like Google, but by anyone needing to embrace the imminent PQC transition.</p>
+<p>And now, we are happy to announce that we are also <a href="https://bughunters.google.com/blog/6038863069184000/formally-verified-post-quantum-algorithms">partnering with Google</a> to develop formally verified open-source implementations of the NIST standards that can be consumed not only by organizations like Google, but by anyone needing to embrace the imminent PQC transition.</p>
 <p>Cryspen provides open source high-performance, high-assurance implementations of ML-KEM (FIPS 203) and ML-DSA (FIPS 204).
 They will be available as Rust crates, as well as C code packages.
 Other versions, including those optimized for IoT devices, can be licensed on request.</p>