rust

9 artigos

9 de jul. de 2026

AutoVerus transforma 40 horas de escrita de proof em 3 chamadas de LLM. O truque é saber quando desistir.

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.

8 de jul. de 2026

LLMs conseguem gerar código Rust. Provas formais são um problema completamente diferente.

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.

model-checking llm rust formal-proofs

5 de jul. de 2026

Você pode provar que seu código Rust está correto sem escrever uma única prova, mas o espaço de estados é a conta

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.

model-checking rust verification formal-methods

26 de jun. de 2026

Suas dependências podem ler qualquer arquivo no disco. cap-std faz com que elas peçam permissão.

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.

capability-based-security rust cap-std sandboxing

22 de jun. de 2026

Pare de Lançar Erros que o Seu Verificador de Tipos Não Vê

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.

type-level-correctness error-handling typescript rust

21 de jun. de 2026

Newtypes em Rust eliminam estados errados em tempo de compilação, sem custo

Uma struct wrapper de campo único captura bugs de mistura de unidades e confusão de tipos sem adicionar um único byte de overhead.

type-level-correctness rust newtypes zero-cost-abstractions

28 de mai. de 2026

Mutation Testing em Rust Funciona, mas Seus Tempos de Compilação Vão Odiar 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.

deep-dives mutation-testing rust cargo-mutants test-quality

23 de mai. de 2026

Testes Baseados em Propriedades em Rust Encontram os Bugs que Seus unit tests Deixam Passar

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.

deep-dives rust property-based-testing quickcheck proptest

21 de mai. de 2026

Contratos de Runtime em Rust Podem Ser Gratuitos em Builds de Release, mas o compiler Não Vai Fazer Isso por Você

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.

deep-dives rust runtime-contracts performance