F* — язык программирования, заточенный под доказательство свойств программ. Он соединяет выразительность зависимых типов с автоматизацией доказательств через SMT-решатели и интерактивное доказательство теорем. По умолчанию код на F* компилируется в OCaml. Отдельные фрагменты можно извлекать в F#, C или Wasm с помощью утилиты KaRaMeL, а также в ассемблер через инструментарий Vale. Сам F* написан на F* и загружается через OCaml.
Исходники лежат на GitHub. Разработкой занимаются Microsoft Research, Inria и сообщество. Язык распространяется под лицензией Apache 2.0. Готовые бинарники для Windows, Linux и Mac OS X регулярно появляются на GitHub. Поставить F* можно через OPAM, Docker, Nix или собрать из исходников.
Для обучения есть онлайн-книга Proof-oriented Programming In F. Отдельный учебник рассказывает про Low — низкоуровневое подмножество F*, которое KaRaMeL компилирует в C.
На F* построено несколько крупных проектов. Project Everest развивает высоконадёжное защищённое сетевое ПО. Библиотека HACL* даёт верифицированные криптографические примитивы на C. ValeCrypt добавляет формально доказанные ассемблерные реализации через фреймворк Vale. EverCrypt объединяет их в единый криптопровайдер. Код из этих проектов работает в Mozilla Firefox, Linux kernel, Python, mbedTLS, блокчейне Tezos, SDK для электронного голосования ElectionGuard и в Wireguard.
Ещё один инструмент — EverParse, генератор парсеров бинарных форматов. Сгенерированные им парсеры применяются в Windows Hyper-V: каждый сетевой пакет, проходящий через Azure, проверяется кодом EverParse. EverParse также используется в ebpf-for-windows.
Вокруг F* много исследований. В основе системы эффектов лежит Dijkstra monad. На ней построена логика разделения SteelCore, а затем DSL Steel для верификации конкурентного кода. Для анализа безопасности криптопротоколов есть фреймворк DY. Среди заметных результатов — реализация TLS 1.3 record layer, библиотека Noise для защищённых каналов, TreeSync для MLS, а также Bert13 — реализация TLS-1.3 на Rust с постквантовой криптографией, доказанная с использованием F*. Есть верифицированный аллокатор памяти StarMalloc и компилятор Catala для юридических текстов.