FAVA usa um solver SMT para barrar em tempo real ações perigosas de agentes de IA
Pesquisadores propõem o FAVA, um framework que substitui listas estáticas de permissão por autorização verificada em tempo de execução para agentes de LLM. Tarefas em linguagem natural são traduzidas para um grafo de permissões rastreável, que um solver SMT confere contra políticas de segurança antes de qualquer ação com efeito real ser executada. Em benchmarks como OpenAgentSafety, OctoBench e ActPlane, o sistema atingiu 90,5% de conformidade nas decisões, interceptando ações que violavam a política dinamicamente.
O artigo ataca um problema conhecido de quem opera agentes de IA em produção: permissões estáticas por ferramenta ("pode usar a API de e-mail", "não pode usar a de pagamentos") não capturam o contexto real de uma ação — o mesmo "enviar e-mail" pode ser inofensivo ou um vazamento de dados dependendo do destinatário, do conteúdo e do histórico da tarefa. O FAVA propõe autorizar cada ação avaliando o estado dinâmico da execução, não apenas o nome da ferramenta chamada.
Tecnicamente, o pipeline tem três estágios: primeiro, uma "Permission Intermediate Representation" guiada por LLM converte a tarefa ambígua em linguagem natural em restrições estruturadas; em seguida, um passo de "lowering" determinístico transforma essa representação em um grafo de permissões que rastreia explicitamente fluxo de dados, dependências e rótulos de contexto entre as etapas da tarefa; por fim, antes de qualquer ação com efeito colateral, um autorizador baseado em SMT (Satisfiability Modulo Theories) verifica matematicamente se o grafo atual satisfaz as políticas de segurança definidas. Um gateway de runtime aplica o veredito do solver, autorizando a execução ou bloqueando-a e devolvendo um contraexemplo preciso — ou seja, aponta exatamente qual trecho do plano viola a política.
Isso importa na prática porque a alternativa mais comum hoje — confiar no próprio modelo para se autolimitar via prompt de sistema, ou aplicar allowlists rígidas de ferramentas — falha justamente nos casos mais perigosos: cadeias de ação legítimas isoladamente, mas que compõem um resultado não autorizado. Formalizar a checagem com um solver dá uma garantia mais forte que "o modelo geralmente se comporta bem", com prova (ou contraexemplo) a cada decisão.
A ressalva fica nos números: 90,5% de taxa de conformidade agregada significa que quase 1 em cada 10 decisões nos cenários avaliados ainda escapou do controle pretendido, o que é relevante para qualquer equipe pensando em usar esse tipo de arquitetura como única linha de defesa para agentes com acesso a sistemas sensíveis. Ainda assim, é um passo concreto na direção de dar aos agentes autônomos um equivalente a controle de acesso com garantias verificáveis, em vez de heurística.