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 для юридических текстов.