1 · What this service does, and what it does not claim

Stalwart builds agents that act for a business, and checks the rules those agents act under. This chapter says what each product does, in plain words, and then the things none of them proves. Every later chapter is written against that second half.

The products

The Bot Builder is how a team builds its own agent. The team declares the agent in one file: its tools, its rules, which writes undo which, and which agent it may hand a conversation to. A component inside it, the selector, reads each turn and decides, by a named rule and with no model call, which tool the turn asks for, what to ask the user, or that the turn is refused. Every tool call is then checked before it runs, whoever chose it. Part I of this guide is the Bot Builder, and Part II is the selector underneath it.

The safety and testing tools check the rules around an agent, and the models it relies on:

• Agent Graph Verification checks every route through an agent before it goes live: each tool reached without its check, its confirmation or its order rule is a finding with the route that reaches it (chapter 47).
• The Guardrail Bug Hunter finds every way through a team's guardrails to a forbidden action, shows each one happening, and hands the team a fix it has checked by scanning again (chapter 28).
• Guardrail Verification decides whether one action can fire without its safety context, or a whole table of such questions, and returns a counterexample with a repair, or a certificate.
• Guardrail Writing drafts a policy from a rule in prose, on the customer's own model, then verifies and repairs the draft (chapter 13).
• Random Forest Verification checks a trained random forest against robustness, monotonicity, fairness and reachability properties (chapter 14).

The hunter and the selector are used together. A guardrail can make every tool action wait for the selector's decision; the hunter then proves that no path reaches a tool without that decision, and fails the pull request that adds one (chapter 29).

Language support

The selector understands turns written in English. Portuguese is its next grammar, and has not shipped yet; until it does, a turn written in Portuguese is not read as Portuguese.

The engine underneath

Beneath the verification products is one engine. You name an outcome that must never happen, such as a transfer executes for a user who is not signed in, and the engine decides whether the policy lets it happen. It compiles the policy and your question into equations over the two values 0 and 1, and asks whether they have a solution.

• If they have none, the outcome is impossible over every combination of inputs at once, not over a sample, and the engine can hand you a certificate that proves it.
• If they have one, the outcome is reachable, and the solution names the exact situation that reaches it.
• Either way, where the outcome is reachable or could not be ruled out, the engine proposes the least disruptive repair it can find, written as a condition in your own policy's words, and proves that the repaired policy closes the hole.

The bug hunter, agent graph verification and guardrail writing all ask this engine their questions. The selector does not: it is a reader of language with its own rules, and its decisions are not proofs (chapter 20).

What it does not claim

Four things none of this proves. Each comes back, under a heading of its own, in the chapter that makes the claim it limits.

1. It proves the questions you asked, and no others. One verification run proves one proposition: that this action cannot fire without that context, under these conditions. It says nothing about any other action, any other context, or any outcome you did not name. A policy is only as verified as your list of unwanted outcomes is complete, and making that list is a judgement about your business, not a calculation (chapter 4).
2. A certificate establishes a derivation, not that its premises are your policy. Checking a certificate shows that the equations it starts from have no common solution. It does not show that those equations are a faithful compilation of your policy file. Closing that second step needs the policy compiled again and compared, which a certificate does not carry (chapter 7).
3. A verdict over a policy with parse diagnostics is not a verdict. A line the compiler could not read is a rule the equations do not have, and a missing rule reads as a bypass, or as a pass, that means nothing. Such a verdict is marked void, and must not be quoted (chapter 6).
4. A patch is proved to close the hole, and only sometimes proved not to over-block. Every repair comes with a proof that the repaired policy rules the outcome out. Whether it also turns away situations your policy should allow is a separate question with its own answer, and only one of that answer's four values, proved_free, says it does not (chapter 8).

And one about standards: a mapping to the OWASP Top 10 lists or to the NIST AI Risk Management Framework is not a certification, an audit or a statement of compliance with either. The hunter's OWASP coverage is at the policy level: it covers the part of each risk the rules a team wrote control, and nothing about a model's weights or training data (chapter 39).

None of the products, and not the agent either, is a proof that an agent is safe. Each proves, or checks, the specific thing its chapter says, and its limits heading says where that stops.