lambdanik

Not just marketing ...

About the name: https://fstar-lang.org/tutorial/book/intro.html#a-bit-of-f-h...

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/

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-hard...

* Verified crypto in Linux, Firefox, Python, ... https://github.com/hacl-star/hacl-star

Have you seen https://github.com/FStarLang/fstar-vscode-assistant? Copilot & F* works pretty nicely.

We've also had a pretty nice emacs mode for a while: https://github.com/FStarLang/fstar-mode.el