Ferramenta para verificar formalmente código Rust, checando especificações em todas as execuções possíveis, sem adicionar verificações em tempo de execução.
O Verus permite que desenvolvedores escrevam especificações que descrevem o comportamento esperado do código Rust e, em seguida, verifica estaticamente se o código executável as satisfaz em todas as execuções possíveis. Em vez de inserir asserções em tempo de execução, ele usa solvers automatizados para provar a correção antecipadamente.
O Verus oferece suporte a um subconjunto de Rust e consegue raciocinar sobre código que vai além do sistema de tipos padrão, como código que manipula ponteiros raw. A ferramenta é voltada a código de sistemas de baixo nível, em que garantias de correção são importantes.
O projeto está em desenvolvimento ativo, então alguns recursos podem estar incompletos ou apresentar problemas. Ele inclui um tutorial, a documentação da API da biblioteca padrão (vstd), um playground no navegador e um formatador automático chamado verusfmt.
Experimente o Verus no navegador com o Verus Playground
Siga as instruções de instalação em INSTALL.md para concluir a configuração local
Acompanhe o tutorial e o guia de referência
Resumo gerado por IA a partir do README do projeto. As estatísticas do GitHub são atualizadas diariamente.
O repositório principal do código-fonte da linguagem Rust, com o compilador, a biblioteca padrão e a documentação.
Um mecanismo em Rust para planejar, aplicar e certificar alterações em ontologias OWL/RDF, com relatórios de raio de impacto e provas verificáveis de conclusões derivadas em Lean 4.
Uma linguagem de programação compilada, simples e rápida, para criar software fácil de manter, sem dependências de bibliotecas e com tradução automática de C para V.
Um fluxo de desenvolvimento guiado por especificações para assistentes de programação com IA alinharem propostas, especificações e tarefas antes de qualquer código ser escrito.
Formato aberto e especificação para empacotar instruções, scripts e recursos em pastas SKILL.md que agentes de IA carregam sob demanda.
A especificação, as definições em TypeScript e JSON Schema e a documentação oficial do Model Context Protocol (MCP), um padrão aberto para conectar aplicações de IA a ferramentas e dados externos.