Análise formal encontra falhas em quatro protocolos de pagamento para agentes de IA
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 ↗