F*: el lenguaje de programación orientado a pruebas que verifica criptografía en Firefox, Linux y Azure

F*: A general-purpose proof-oriented programming language

F* es un lenguaje de programación de propósito general orientado a pruebas, que combina tipos dependientes con automatización de pruebas basada en SMT y tácticas interactivas. Compila a OCaml, F#, C, Wasm y ensamblador, y se utiliza en proyectos como Project Everest, HACL*, ValeCrypt y EverCrypt. Sus implementaciones verificadas de criptografía se usan en producción en Mozilla Firefox, el kernel de Linux, Python, mbedTLS, la blockchain Tezos, ElectionGuard y Wireguard. EverParse, un generador de analizadores sintácticos verificado, se usa en Windows Hyper-V para validar cada paquete de red en Azure.