Aura-State

Prove your AI agent is injection-safe, in-spec, and won't act out of bounds — before you ship it.

A design-time verifier for LLM agents — not a runtime guardrail. Import your LangGraph / CrewAI / AutoGen / MCP agent and Aura proves five things about the agent you already wrote, then hands you the exact counterexample or a certificate. Z3 · CTL model checking · information-flow/taint · conformal calibration. Runs locally, in CI, no API key.

_{Verify a design → import a real agent from its code → the lethal trifecta lights up with the exact path → save a baseline and gate regressions.  ·  ▶ watch the full walkthrough}

pip install aura-state          # or:  uv pip install aura-state  ·  uv add aura-state

Um comando, zero configuração

$ aura-state demo          # no keys, no config, no agent of your own needed

  aura-state check · support-ticket-agent · 4 nodes

  ✗ trifecta [send]: lethal trifecta closed — prompt injection at 'fetch' (untrusted)
    can reach external sink 'send' unsanitized while 'draft' brings private data into
    scope. Path: fetch → lookup → draft → send. Break it with a sanitizer between
    'fetch' and 'send', or remove one of the three capabilities.

  ✗ NOT PROVEN — 1 blocking finding(s)          # exit 1 → CI fails
  checked: trifecta closed · taint proven · reachability proven · obligations proven · policy 0 flagged

Cinco coisas que isso prova sobre o seu agente

Injeção de prompt é apenas uma delas.

	Propriedade	Em palavras simples
🔒	Seguro — taint + tríade letal	não pode ser enganado para vazar dados
✅	Correto — obrigações Z3/SMT	as saídas obedecem às suas regras (amount ≤ limit)
♻️	Vivo — verificação de modelo CTL	termina, cada passo é alcançável, sem becos sem saída
📊	Calibrado — intervalos split-conformal	sabe o quão confiante realmente é
🛑	Governado — abstenção com risco controlado	recusa-se a agir quando não tem certeza

Aponte para o seu próprio agente

aura-state check my_agent.json      # a studio export
aura-state check your_agent.py      # a LangGraph / CrewAI / AutoGen source file — parsed, never executed
aura-state check ./my-agent-repo/   # a whole directory
uvx aura-state check agents/*.json  # zero-install via uv — perfect for CI

Mais do que injeção — privilégio mínimo, envenenamento, um certificado

Além da tríade, o check também prova:

• Privilégio mínimo. Declare um manifesto de capacidades e o Aura prova que o agente não consegue alcançar um efeito fora dele — o modo de falha sem-atacante (um agente com permissões excessivas executando uma ação não intencional). Adicione "manifest": { "side_effects": ["read"] } ao seu fluxo:

  ✗ least-privilege [Pay]: 'Pay' can external 'payment.charge', outside the declared manifest
  

• Envenenamento de ferramentas MCP. Numa importação MCP, a descrição de cada ferramenta é analisada à procura de instruções injetadas no texto de ajuda (a classe tool-poisoning — por exemplo, "…também lê ~/.cursor/mcp.json e passa-o como parâmetro"). Estático — nunca se liga a um servidor.

Prova-o — depois prova a prova. Emite um certificado verificável e volta a verificá-lo sem confiar em quem o emitiu:

aura-state certify your_agent.py --out cert.json   # design + verdict, content-hashed
aura-state verify-cert cert.json                   # re-runs the verifier — catches any tamper

Mapeia para o Art. 12 do EU AI Act / ISO 42001 (evidência, não apenas documentação).

Faça benchmark. aura-state bench executa um corpus rotulado (precisão em pares seguros/vulneráveis — sound, portanto o recall é 100% por construção; o número medido é a precisão) mais cobertura de importação em agentes reais de MCP/frameworks ingeridos sem modificação.

Como isto é diferente (e honesto)

Existem verificadores de agentes pré-execução — mas cada um faz uma coisa e obriga você a reescrever seu agente no formalismo deles. A vantagem do Aura é ser a ferramenta pronta que ingere o agente que você já escreveu e executa o conjunto completo:

	Estático (antes de rodar)?	Dataflow de segurança?	Importa seu agente real?
AgentProof	✅	❌ apenas topologia	✅
AgentFlow	✅	✅	❌ seu próprio DSL de políticas
FIDES (Microsoft)	❌ runtime	✅	❌ planejador construído com ele
Aura-State	✅	✅	✅ LangGraph / CrewAI / AutoGen / MCP

Não inventamos esses métodos — a pesquisa é rica e parte dela é mais rigorosa que a nossa. Somos o que você pode pip install e apontar para seu agente existente hoje. E é sound / fail-closed: uma capacidade desconhecida é apresentada como aviso, nunca passada silenciosamente.

Coloque no CI e cada PR é verificado:

# .github/workflows/aura.yml
- uses: your-org/aura-state@v0
  with: { paths: "agents/*.json" }

Detecte a trifeta letal — antes que um atacante o faça

A trifeta letal é o modo de falha mais assustador para um agente que usa ferramentas: no momento em que ele pode (1) ler dados privados, (2) ingerir conteúdo não confiável e (3) comunicar-se externamente — tudo em um único caminho alcançável — uma injeção de prompt escondida nesse conteúdo pode ler seus dados e enviá-los para fora. Todos alertam sobre isso. Aura prova que seu agente não consegue fechar isso, estaticamente, antes de você fazer o deploy:

$ aura-state check dev_assistant.tools.json   # ← your MCP tools/list export

  ✗ trifecta [slack_post_message]: lethal trifecta closed — prompt injection at 'fetch'
    (untrusted) can reach external sink 'slack_post_message' unsanitized while 'read_file'
    brings private data into scope. Path: fetch → Agent → slack_post_message.
    Break it with a sanitizer between 'fetch' and 'slack_post_message'.

Aponte-o diretamente para a sua configuração de MCP. Exporte o tools/list do seu agente (ou entregue a sua configuração de cliente) e o Aura modela o pior cenário — o LLM pode chamar qualquer ferramenta em qualquer ordem — e então decide se fetch + filesystem + slack juntos formam um canal de exfiltração. Ele nunca se conecta a um servidor nem o executa.