F* existed before Project Everest, but Everest did power a lot of its development. We have built verified systems and components in the TLS ecosystem, includin

F* existed before Project Everest, but Everest did power a lot of its development. We have built verified systems and components in the TLS ecosystem, including parts of TLS, QUIC and related protocols, and continue to do so: https://project-everest.github.io/ https://project-everest.github.io/ Some of it is deployed in production systems: * Verified parsers in the Windows kernel and elsewhere: https://www.microsoft.com/en-us/research/blog/everparse-hardening-critical-attack-surfaces-with-formally-proven-message-parsers/ https://www.microsoft.com/en-us/research/blog/everparse-hard... * Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star https://github.com/hacl-star/hacl-star