12. F*: язык программирования с формальным доказательством от Microsoft Research
Microsoft Research и Inria развивают F* — proof-oriented язык с зависимыми типами и SMT-решателями. Компилируется в OCaml, C и Wasm. Код на F* используется в Firefox, Linux, Azure Hyper-V для верифицированной криптографии (HACL*, EverCrypt) и парсинга сетевых пакетов (EverParse).