O artigo ataca um problema especifico de agentes de IA que controlam carteiras on-chain: como eles leem conteudo potencialmente controlado por atacantes, podem ser induzidos a propor transacoes danosas, e as verificacoes usuais checam o estado da blockchain no momento da checagem, nao no momento da execucao -- uma janela que um atacante pode explorar via front-running ou mudancas de contrato. A defesa proposta, Proof-Gated Signing, simula a transacao, extrai seus efeitos e usa um solver SMT para provar que uma politica declarativa se mantem valida sob toda uma faixa de incerteza de preco, bloqueando no proprio contrato de carteira qualquer execucao que viole as pos-condicoes provadas; em 260 cenarios de teste, preveniu 93,6% dos ataques, contra 57,9% da simulacao isolada e 71,4% da allowlist estatica.
Fonte ↗Pesquisadores propõem o MAGS, um framework multiagente que traduz código gerado por agentes de IA para Dafny, uma linguagem com verificação formal, a fim de provar matematicamente que certas propriedades de segurança são respeitadas. O sistema atingiu 100% de sucesso na verificação formal contra especificações congeladas em 220 casos testados, mas avaliações independentes revelaram que a garantia formal nem sempre corresponde a segurança ou funcionalidade real quando a formalização não captura todo o comportamento relevante.
Fonte ↗CaMeLoT estende a defesa CaMeL contra injeção de prompt adicionando uma camada de verificação estática: o plano gerado por um agente LLM é traduzido em um sistema de transição de estados finitos, rotulado com informação de proveniência e taint, e checado contra políticas temporais expressas em lógica CTL usando o model checker nuXmv antes de qualquer ferramenta ser de fato chamada. Planos reprovados geram um contraexemplo que serve de retroalimentação para o agente corrigir o plano, sem gastar chamadas de LLM ou de ferramenta nem precisar desfazer efeitos colaterais.
Fonte ↗Pesquisadores formalizaram em Tamarin quatro protocolos emergentes de pagamento para agentes de IA (x402, MPP, ACP e AP2) e, a partir de 86 casos de verificação, encontraram 40 achados de inconsistência formal não documentados anteriormente, além de reproduzir 46 problemas já conhecidos. Dez desses achados foram validados com provas de conceito em implementações reais do x402.
Fonte ↗