F*: a linguagem orientada a provas que redefine a verificação formal de software

A linguagem de programação orientada a provas F* (pronunciada F star), desenvolvida em parceria colaborativa pela Microsoft Research, pelo instituto de pesquisa francês Inria e por uma comunidade ativa de código aberto no GitHub, estabeleceu-se como uma das infraestruturas mais robustas da ciência da computação para a criação de sistemas com garantias matemáticas de correção e segurança funcional.

Concebida como uma linguagem de propósito geral, a F* oferece suporte simultâneo à programação funcional pura e ao desenvolvimento imperativo baseado em efeitos, combinando a alta capacidade expressiva de seu sistema de tipos dependentes com mecanismos modernos de automação de provas apoiados em resolvedores SMT (Satisfiability Modulo Theories) e demonstração interativa ancorada em táticas.

Distribuída sob os termos da licença livre Apache 2.0, a ferramenta conta com suporte de compilação por padrão direcionado à linguagem OCaml, além de permitir que fragmentos do seu código sejam extraídos diretamente para ambientes de execução em F#, para linguagens de baixo nível como C e WebAssembly, ou para código de montagem via conjunto de ferramentas especializado.

Arquitetura e conceitos centrais

O pilar fundamental da F* reside no uso de tipos dependentes, uma estrutura lógica que permite que tipos de dados façam referência direta a valores e propriedades computacionais, permitindo que especificações formais complexas sejam anexadas diretamente às assinaturas de funções e rotinas do programa.

Para evitar a necessidade de construção manual de cada etapa da prova de verificação, a F* traduz automaticamente as obrigações de verificação geradas pelo código-fonte em consultas para resolvedores de teorias SMT, automatizando a checagem de propriedades lógicas sem demandar intervenção contínua do desenvolvedor.

Nos cenários em que a automação via SMT atinge limites computacionais de complexidade, a linguagem disponibiliza um ecossistema interno de metaprogramação e táticas operacionais, permitindo que pesquisadores e engenheiros explicitem estratégias de prova interativas para resolver teoremas matemáticos desafiadores.

A própria linguagem F* é estruturada de forma auto-hospedada (bootstrapped), sendo seu próprio compilador implementado em F* e refinado a partir do suporte de compilação da linguagem OCaml para gerar os binários executáveis do sistema.

Compilação e ecossistema de ferramentas

Durante a esteira habitual de desenvolvimento na F*, o código verificado é traduzido por padrão para a linguagem OCaml, garantindo portabilidade para ambientes funcionais e facilitando a integração com ferramentas de análise estática pré-existentes na biblioteca acadêmica.

Quando a aplicação exige execução nativa sem sobrecarga de coleta de lixo, a linguagem utiliza a ferramenta chamada KaRaMeL, um utilitário projetado para transformar trechos verificados da F* em código-fonte legível nas linguagens C e WebAssembly (Wasm).

Para atender aos cenários de desenvolvimento que exigem controle direto sobre registradores e instruções do processador, o ecossistema incorpora a ferramenta Vale, que atua na verificação formal de linguagens de montagem (Assembly) diretamente embutidas na estrutura lógica da F*.

A distribuição e instalação da F* são mantidas atualizadas por meio de pacotes binários pré-compilados lançados de forma regular para os sistemas operacionais Windows, Linux e macOS diretamente na página oficial de lançamentos da plataforma GitHub.

Os engenheiros de software podem integrar a F* às suas estações de trabalho utilizando o gerenciador de pacotes OPAM, ambientes isolados via containers Docker, definições do gerenciador Nix ou mediante o processo de compilação local descrito no arquivo de instruções INSTALL.md.

Aplicações industriais e de produção

A utilidade prática do ecossistema da F* estende-se para além dos laboratórios de pesquisa, sendo a base de engenharia do Project Everest, uma iniciativa guarda-chuva dedicada ao desenvolvimento de softwares de comunicação com garantias totais de segurança matemática e imunidade a falhas.

Como fruto direto do Project Everest, a biblioteca HACL* disponibiliza um acervo completo de primitivas criptográficas desenvolvidas e verificadas formalmente na F*, que são extraídas para código C de alto desempenho livre de vulnerabilidades de estouro de memória.

Complementando o ecossistema criptográfico, o projeto ValeCrypt fornece implementações de primitivas de segurança otimizadas em nível de linguagem Assembly, cujas provas formais são validadas pela arquitetura da ferramenta Vale embarcada na F*.

A integração entre a biblioteca HACL* e o projeto ValeCrypt resultou no surgimento do EverCrypt, um provedor criptográfico unificado de alta performance cujos módulos verificados operam em produção dentro do navegador Mozilla Firefox e no próprio núcleo do sistema operacional Linux.

Além do núcleo do sistema operacional e do navegador da fundação Mozilla, componentes derivados do EverCrypt alimentam a segurança de ecossistemas como a linguagem de programação Python, a biblioteca de segurança mbedTLS, a rede blockchain Tezos, o kit de desenvolvimento de votação eletrônica ElectionGuard e o protocolo de VPN Wireguard.

Outro marco de aplicação industrial é a ferramenta EverParse, um gerador automatizado de parsers para formatos binários que extrai programas em linguagem C comprovadamente corretos a partir de especificações formais escritas em F*.

Os parsers gerados pelo EverParse desempenham um papel crítico na nuvem da Microsoft, operando no hipervisor Windows Hyper-V, onde cada pacote de dados de rede que trafega pela infraestrutura global do Microsoft Azure é verificado por código originado na F* antes de ser processado.

O uso do gerador EverParse também alcançou a comunidade de sistemas abertos por meio do projeto ebpf-for-windows, garantindo que programas eBPF em nível de kernel passem por uma verificação rígida de integridade de formato binário antes do processamento.

Avanços teóricos em linguagens científicas

A arquitetura fundamental da linguagem e o modelo formal de seus tipos dependentes foram introduzidos na conferência acadêmica POPL 2016 no artigo seminal intitulado "Dependent Types and Multi-monadic Effects in F*", estabelecendo o documento de referência do sistema.

Para viabilizar a verificação formal de programas imperativos de baixo nível com garantias de conversão para o código imperativo tradicional, a conferência ICFP 2017 apresentou a sublinguagem Low*, que abstrai o desenvolvimento imperativo e possibilita a extração para C via KaRaMeL.

A capacidade de automação e personalização do sistema de tipos da linguagem avançou na conferência ESOP 2019 com o estudo da ferramenta Meta-F*, um arcabouço de metaprogramação que permite a implementação de táticas customizadas e suporte nativo a classes de tipos.

O detalhamento formal do núcleo lógico da linguagem e o suporte à criação de efeitos personalizados definidos pelos usuários foram consolidados no estudo de 2021 sob o título "Programming and Proving with Indexed Effects".

No campo do raciocínio concorrente para programas imperativos, o artigo apresentado na ICFP 2021 lançou a linguagem embarcada Steel, que introduziu a programação orientada a provas ancorada no cálculo da lógica de separação concorrente com tipos dependentes.

Tratamento de efeitos e verificação relacional

A base conceitual para o tratamento rigoroso de computações com efeitos na F* remonta à conferência PLDI 2013, no qual os pesquisadores introduziram a estrutura teórica conhecida como Dijkstra Monad para fundamentar a especificação de pré e pós-condições.

O aprimoramento dessa teoria foi demonstrado na conferência POPL 2017 no artigo "Dijkstra Monads for Free", que provou como derivações monádicas para verificação de código podem ser obtidas de forma automatizada por meio de transformações baseadas em passagem de continuação.

A expansão da capacidade de análise para além do escopo de um único programa ocorreu na conferência CPP 2018, que apresentou uma estrutura para verificação relacional usada na prova de equivalência entre códigos e na análise formal de segurança da informação.

A generalização do modelo monádico atingiu maturidade na conferência ICFP 2019 com o estudo "Dijkstra Monads for All", demonstrando o uso de morfismos monádicos para conectar monads computacionais a monads de especificação matemática.

Para garantir o raciocínio formal sobre programas cujo estado interno evolui apenas de forma acumulativa ou incremental, o conceito de Monotonic State foi estabelecido na POPL 2018, tornando-se o pilar de verificação de memória para as linguagens Low* e Steel.

Evolução em lógica de separação

A necessidade de apoiar a escrita de programas concorrentes complexos motivou a criação do arcabouço SteelCore, publicado na conferência ICFP 2020 como uma lógica de separação concorrente extensível que serve de sustentação para a linguagem Steel.

Na mesma linha de evolução teórica, a linguagem recebeu o arcabouço USSL (Universe-Stratified, Predicative Concurrent Separation Logic), uma lógica de separação concorrente rasa e isenta de axiomas que organiza predicados em uma hierarquia de universos para manipular invariantes dinâmicos.

Avançando na fronteira da pesquisa acadêmica, o estudo programado para a conferência PLDI 2025 introduz o sistema PulseCore, uma lógica de separação concorrente impredicativa sem axiomas que suporta créditos posteriores e estados fantasma de alta ordem.

A infraestrutura do PulseCore consolidou-se como o alicerce fundamental para a Pulse, uma nova linguagem embarcada dentro do ambiente da F* direcionada à programação orientada a provas sob lógicas de separação concorrente.

Aplicações em criptografia e protocolos

No segmento de computação multipartidária com garantias de privacidade, a sublinguagem WYS* foi apresentada no evento POST 2017 como uma linguagem de domínio específico para escrever protocolos computacionais seguros verificados na F*.

A integridade de protocolos de comunicação na internet teve um avanço significativo no evento IEEE S&P 2017, que exibiu uma implementação formalmente verificada da camada de registro do protocolo TLS 1.3 escrita em Low*.

A biblioteca HACL* foi detalhada formalmente na conferência de segurança CCS 2017, enquanto a implementação LibSignal* — que valida o protocolo de mensagens Signal na F* — foi lançada no S&P 2019 com extração para WebAssembly através do KaRaMeL.

No evento S&P 2020, os pesquisadores demonstraram a eficiência do EverCrypt através da implementação verificada de uma árvore de Merkle de alto desempenho usada nas primeiras versões da infraestrutura Microsoft Azure CCF.

Para otimizar a execução criptográfica em processadores modernos, o artigo HACLxN, apresentado na CCS 2020, aplicou metaprogramação na F* para gerar automaticamente versões vetorializadas com instruções SIMD provadas contra falhas de segurança.

A verificação do transporte de dados no protocolo QUIC da IETF foi publicada no S&P 2021, combinando a implementação da camada de registro em Low* com a lógica de protocolo analisada na ferramenta de verificação formal Dafny.

Em ambientes de microcontroladores e dispositivos embarcados, a biblioteca DICE* provou no evento USENIX Security 2021 a correção e a segurança do protocolo de boot medido DICE utilizando os componentes EverCrypt e EverParse.

A análise de segurança simbólica de protocolos de rede ganhou suporte modular com o framework DY*, apresentado na conferência Euro S&P 2021 e complementado por material instrucional publicado na série LNCS 2021.

A aplicação prática do framework DY* permitiu comprovar, na conferência CCS 2021, a segurança do padrão de gerenciamento de certificados digitais ACME, utilizado globalmente pela infraestrutura da internet.

O ecossistema de canais seguros de comunicação foi estendido com a biblioteca Noise* na S&P 2022, que metaprograma implementações provadamente seguras para uma família de protocolos de canal criptográfico.

Para mensageria segura em grupo, o estudo TreeSync apresentou no USENIX Security 2023 a implementação de referência do padrão MLS (Messaging Layer Security) em F*, com garantias de segurança validadas pelo framework DY*.

As técnicas de abstração sem custo e engenharia de provas desenvolvidas na biblioteca HACL* foram expostas na ICFP 2023, demonstrando como códigos criptográficos especializados em C permitiram a inclusão direta de componentes verificados nas bibliotecas da linguagem Python.

A análise formal de privacidade no tráfego de dados foi impulsionada pela biblioteca Waldo na conferência OOPSLA 2023, permitindo provas formais de indiscutibilidade sobre traços de comunicação em protocolos de rede.

O manuseio preciso de formatos de mensagens binárias recebeu o reforço da biblioteca de parsing Comparse no CCS 2023, fornecendo à ferramenta DY* a capacidade de raciocinar sobre mensagens concretas em nível de bits.

A expansão recente da verificação formal atingiu a linguagem de sistemas Rust no estudo apresentado para o CCS 2025 com a biblioteca Bert13, que implementa o protocolo TLS 1.3 com recursos pós-quânticos e prova sua correção por meio do tradutor Hax.

Formação técnica e comunidade aberta

O aprendizado e a formação de novos desenvolvedores na F* são impulsionados pelo livro online interativo intitulado Proof-oriented Programming In F*, que permite aos estudantes resolver exercícios e testar exemplos de código diretamente no navegador.

Para os profissionais focados em engenharia de sistemas de baixo nível, a equipe do projeto disponibiliza um tutorial focado na linguagem Low*, ensinando como estruturar programas imperativos e realizar a compilação para C via KaRaMeL.

O ensino formal da F* tem sido promovido em escolas internacionais de computação, incluindo a EUTypes Summer School 2018 em Ohrid, na Macedônia, o simpósio ECI 2019 e edições da Oregon Programming Language Summer School nos anos de 2019 e 2021.

A organização da comunidade migrou suas interações cotidianas das antigas instâncias do Slack para um fórum público hospedado na plataforma Zulip, mantendo também o canal GitHub Discussions para anúncios e a lista de transmissões fstar-mailing-list.

O acompanhamento contínuo dos avanços do compilador e de suas aplicações é promovido mensalmente no encontro aberto F* PoP Up Seminar, enquanto dúvidas técnicas diretas e coordenação do repositório são gerenciadas pelo e-mail oficial fstar-maintainers@googlegroups.com.