The seL4 microkernel: https://sel4.systems/ https://sel4.systems/ The CompCert C compiler: https://compcert.org/ https://compcert.org/ TLS implementation in F

The seL4 microkernel: https://sel4.systems/ https://sel4.systems/ The CompCert C compiler: https://compcert.org/ https://compcert.org/ TLS implementation in Firefox: https://blog.mozilla.org/security/2020/07/06/performance-improvements-via-formally-verified-cryptography-in-firefox/ https://blog.mozilla.org/security/2020/07/06/performance-imp... Elasticsearch model checks some of their core algorithms with TLA+: https://youtu.be/qYDcbcOVurc https://youtu.be/qYDcbcOVurc. Amazon is known to apply formal methods in varying forms to services like S3: https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3 https://www.amazon.science/publications/using-lightweight-fo... Many components in airplane software is formally verified in some aspect.