9 posts
AutoVerus utiliza uma rede de agents LLM para gerar proofs de correção Verus para código Rust, automatizando mais de 90% das proof obligations por meio de um loop gerar-reparar-discharge impulsionado pelo feedback do solver SMT.
A parte mais difícil da verificação formal nunca foi o verificador. É escrever o proof. Dê a um engenheiro sênior de Rust o Verus, o verificador baseado em SMT…
Grandes modelos de linguagem escrevem código Rust surpreendentemente bom, mas quando você pede uma prova formal, eles alucinam invariantes e inventam sintaxe que nenhum verificador aceita. Veja o que eles realmente acertam, onde falham e como usá-los mesmo assim.
LLMs conseguem escrever Rust que compila e até passa em . O que não conseguem fazer de forma confiável é escrever uma prova formal de que o código está correto…
Ferramentas de model checking como Kani permitem verificar propriedades de Rust com assertions em vez de provas formais. O problema é o que acontece quando seus loops não têm limites pequenos.
Você pode provar que seu código Rust está correto sem escrever uma única prova. A ferramenta que faz isso se chama model checker, e para Rust o mais prático no…
A biblioteca padrão do Rust concede autoridade de sistema de arquivos ambiente a toda dependência. cap-std a substitui por APIs baseadas em capabilities que forçam o código a provar que tem direito de acessar um caminho antes de abri-lo.
Qualquer crate na sua árvore de dependências pode abrir , escrever no seu diretório ou enumerar todos os arquivos do seu projeto. A biblioteca padrão do Rust…
Exceções lançadas escondem caminhos de falha do seu sistema de tipos. Veja por que retornos de erro explícitos tornam seu código mais honesto, e como adotá-los sem odiar sua vida.
A assinatura da sua função diz que retorna um . Não retorna. Ela retorna um ou explode. O sistema de tipos simplesmente não sabe sobre o segundo branch. Esta é…
Uma struct wrapper de campo único captura bugs de mistura de unidades e confusão de tipos sem adicionar um único byte de overhead.
Passe um user ID para uma função que espera um order ID, e Rust não vai reclamar. Ambos são . O compiler vê tipos idênticos, então não pode te ajudar. Você…
cargo-mutants encontra os testes que apenas fingem verificar seu código. Veja como mutation testing funciona para Rust, o que ele captura e se o custo de tempo de compilação vale a pena.
Você tem 100% de cobertura de linhas. Cada branch é executada. Cada função é chamada. Aí alguém muda um para na sua lógica de precificação, executa os testes e…
Testes baseados em exemplos cobrem apenas as entradas que você imaginou. Testes baseados em propriedades geram dados aleatórios, verificam invariantes e reduzem falhas aos contraexemplos mínimos.
Você escreveu uma função . Testou com e . Passou. Enviou para produção. Um usuário passa um slice de um único elemento. Sua função o ignora silenciosamente.…
Rust remove debug assertions automaticamente, mas design-by-contract de verdade precisa de mais do que debug_assert!. Veja como construir contratos de runtime com custo zero que desaparecem do seu binário de release.
Rust pode impor contratos de runtime em desenvolvimento e apagá-los completamente das builds de release. A ressalva é que a linguagem não trata contracts como…