6 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…
Por que o model checking supera dias de execução em produção para encontrar bugs de concorrência, e como aplicá-lo ao seu próprio código.
Esperar que race conditions surjam em produção não é testar. É esperança disfarçada de diligência. Você pode executar seu app por semanas, monitorar seus…
Bounded model checkers como Kani e relational model finders como Alloy permitem verificar propriedades com assertions e constraints ordinários. Você abre mão de provas de liveness por uma curva de aprendizado medida em horas, não em semanas.
Você não precisa aprender lógica temporal linear para usar um model checker. Ferramentas como Kani, CBMC e Alloy permitem verificar propriedades com assertions…
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…
Bugs distribuídos são caros de corrigir após o deploy. O model checking permite que você os encontre antes de escrever uma única linha de código de implementação. Veja como fazer isso com TLA+.
Você não pode fazer unit test de um protocol distribuído. Um unit test executa um processo em uma máquina em uma ordem. Seu protocol executa dez processos em…