---
title: "Anthropic e Theorem Labs usam Claude para verificar segurança de software"
url: https://dailyjournal.news/news/2026-10-22/anthropic-usa-modelo-claude-para-verificacao-formal-de-software
published: 2026-10-22T22:45:15.897969+00:00
updated: 2026-10-23T12:08:32.718431+00:00
categories: ["technology"]
source_count: 5
outlet_count: 1
language: pt-BR
publisher: "Daily Journal"
---

# Anthropic e Theorem Labs usam Claude para verificar segurança de software

A Anthropic, dos EUA, diz que, com a Theorem Labs, o Claude provou propriedades de segurança em 123 bibliotecas de código aberto no nível de assembly, e que as provas revelaram centenas de bugs.

## Pontos principais

- A Theorem Labs forneceu a semântica das instruções RISC-V e dos processos Linux usada nas provas.
- As provas cobrem 239 pontos de entrada de 123 bibliotecas de código aberto do OSS-Fuzz, no nível de assembly RISC-V.
- Segundo a Anthropic, nenhum desses pontos de entrada apresenta crash, erro de memória ou assertion falha para entradas de até 64 MB.
- As garantias valem para programa single-thread, binário estático, memória fixa, RISC-V com musl e Linux, segundo a Anthropic.
- O trabalho levou algumas semanas e somou cerca de 180 milhões de linhas de Rocq, com prova típica de cerca de 600 mil.
- Ao escrever as provas, o Claude corrigiu os bugs que encontrou; a Anthropic relata centenas de bugs revelados.
- A Anthropic relata que o modelo poderia reescrever o programa para tornar o teorema trivial; a equipe penalizou qualquer patch e auditou todos.
- Em outro caso, o Claude provou no nível binário a zlib do kernel Linux, a partir de uma especificação derivada da RFC 1950.

A Anthropic, dos EUA, anunciou uma parceria com a Theorem Labs para usar o Claude na verificação formal de segurança de software. Segundo a empresa, é o primeiro esforço em larga escala de IA na verificação formal de software de produção, no nível de assembly.

A própria Anthropic ressalva que “formalmente verificado” não significa “sem bugs”. A especificação, os modelos de RISC-V e Linux, o checker Rocq e o hardware seguem na base confiável, e as provas modelam binários RISC-V estáticos com musl, não os x86 ou ARM com glibc dinâmica da maioria dos usuários.

## Fontes

- [Claude e a verificação formal de bibliotecas de produção](https://maccus.fr/en/claude-formal-verification/) (2026-10-23)
- [Anthropic e verificação formal: o que muda para software de código aberto](https://cellcog.ai/blog/anthropic-formal-verification/) (2026-10-23)
- [Verificação formal em escala com o Claude](https://www.anthropic.com/research/formal-verification) (2026-10-23)
- [Anthropic says it partnered with Theorem to use Claude to formally prove security properties at the assembly level across 100+ real-world open-source libraries (Anthropic)](https://www.techmeme.com/261023/p5#a261023p5) — Techmeme (2026-10-23)
- [@AnthropicAI: New on our Frontier Red Team blog: using Claude to formally verify software at large scale.](https://x.com/AnthropicAI/status/2113390212911083894) (2026-10-22)

---

Publicado por Daily Journal. Versão HTML: https://dailyjournal.news/news/2026-10-22/anthropic-usa-modelo-claude-para-verificacao-formal-de-software