SYSTEM Cited by 2 sources
Bedrock Guardrails — automated reasoning checks¶
What it is¶
A 2025/2026-era capability within Amazon Bedrock Guardrails that lets customers formally verify the correctness of AI outputs against a specification. The customer provides (or imports) a spec; the service mechanically checks model outputs against it; the verdict gates downstream delivery.
Launched in preview 2024-12-04, US West (Oregon) only — the first responsible-AI capability from a major cloud provider that combines safety + privacy + truthfulness (via automated reasoning) in a single product (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations).
This year, we released a capability called automated reasoning checks in Amazon Bedrock Guardrails which enables customers to prove correctness for their own AI outputs. The capability can verify accuracy by up to 99%. — Byron Cook (Source: sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai)
Customer workflow (preview, 2024-12)¶
From the preview-launch post (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations):
- Create an Automated Reasoning policy. Navigate to Safeguards → Automated Reasoning in the Bedrock console; upload an authoritative document (HR policy, airline-ticket policy, operational manual).
- Declare the policy's intent + sample Q/As. Short natural-language statement scoping what the policy covers (e.g. "Airline employees will ask questions about whether customers are allowed to modify their tickets...") plus one or more sample question/answer pairs; elements to exclude (like internal reference numbers) are called out explicitly.
- Bedrock runs the autoformalization pipeline — identify concepts → decompose document into units → translate each unit from natural language to formal logic → validate translations → combine into a comprehensive logical model. Output: a set of typed variables (name + type + natural-language description) and rules (rendered in natural language; stored as formal logic).
- Review + edit the generated structure in the UI. Rules can be edited in natural language; the system automatically re-compiles the logical model.
- Attach the policy to a guardrail. Create a Guardrail, enable Automated Reasoning, select policy + version.
- Iterate in the Test playground. Enter a Q/A, run it through the guardrail, review the verdict + suggestions; refine variable descriptions and rules.
The verdict triple (preview-launch mechanics)¶
Validation produces one of three states (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations):
| Verdict | Meaning | Suggestion shape |
|---|---|---|
| Valid | Answer is consistent with the policy. | Unstated assumptions necessary for the result to hold (e.g. "assumes this is the original ticket; ticket-stock type is eligible for changes"). |
| Invalid | Answer is inconsistent with the policy. | Variable assignments that would make the answer valid (e.g. "submission method must be email for this to be valid"). |
| Mixed results | Some findings valid, some invalid. | List of findings in the API response; typically a signal that the rule set is ambiguous — edit rules, re-test. |
The Valid/Invalid/Mixed triple — each with structured suggestions rather than a scalar confidence score — is distinctive vs. typical ML classifier output. The suggestions expose the reasoner's counterexample (for Invalid) or its model hypotheses (for Valid) in a form a non-specialist can read.
Regenerate-with-feedback loop¶
The reasoner's counterexample is fed back to the LLM as explicit natural-language feedback for regeneration. The preview-launch post publishes a canonical snippet (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations):
for f in findings:
if f.result == "INVALID":
if f.rules is not None:
for r in f.rules:
feedback += f"<feedback>{r.description}</feedback>\n"
new_prompt = (
"The answer you generated is inaccurate. Consider the feedback below within "
f"<feedback> tags and rewrite your answer.\n\n{feedback}"
)
This is the concrete shape of the regenerate-on-CE branch of patterns/post-inference-verification: the reasoner's verdict isn't just a filter — it is a structured corrective signal that the LLM is re-prompted against. The spec stays in natural language in the feedback (the logical form is never exposed).
Accuracy-tuning knob: variable descriptions¶
The iteration loop is on variable descriptions, not on prompts or model weights. Worked example (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations):
- Variable
is_full_timewith description "works more than 20 hours per week" → fails to extract a value when the question says "I'm a full-time employee..." (natural-language mismatch; the extractor reads the description to ground terms). - Extended description: "Works more than 20 hours per week. Users may refer to this as full-time or part-time. The value should be true for full-time and false for part-time." → correctly extracts across colloquial variants.
The natural-language variable description is therefore a first-class spec artifact — it participates in the reasoner's term-grounding pass. See concepts/autoformalization for the broader frame.
The pattern it realizes¶
This is the canonical AWS productization of patterns/post-inference-verification:
- LLM (hosted in Bedrock) generates output
yfor inputx. - Guardrails layer runs concepts/automated-reasoning against
yvs customer-supplied specS. - Verdict gates delivery.
Unlike typical ML-model quality claims, the 99% accuracy figure is a provable lower bound for any output that passes — contingent on the spec being correct and the reasoner terminating. This is qualitatively distinct from benchmark-averaged accuracy numbers.
Named target industries¶
- Finance — accuracy non-negotiable (regulatory, liability).
- Healthcare — accuracy non-negotiable (patient safety).
- Government — accuracy non-negotiable (legal / compliance).
The framing: generative / agentic AI is blocked from production in these domains by trust. Automated reasoning checks is AWS's answer.
What the spec can say¶
Based on Cook's interview, specs range over:
- Numeric / schema constraints (easy: output conforms to JSON schema, values within bound).
- Policy / authorization rules (tractable with SMT: "this response does not assert a permission the user lacks").
- Domain-logic equivalence ("this optimized crypto procedure is semantically equivalent to the reference"; Cook's worked example of AWS cryptography).
- Temporal specs (concepts/temporal-logic-specification) — hardest and most expressive; future expansion.
Cook predicts the user-visible surface will broaden to branching-time vs linear-time logic, past vs future operators, epistemic and causal logics.
Autoformalization as the gating UX problem¶
The bottleneck is not the reasoner; it's the customer-authored spec.
In my opinion the biggest challenges are: 1/ getting autoformalization right, allowing everyone to build and understand specifications without specialist knowledge. That's the domain that tools such as Kiro and Bedrock Guardrails' automated reasoning checks are operating in.
Automated reasoning checks is simultaneously a product and a forcing function on autoformalization: as more customers write specs for it, the product absorbs feedback on natural-language → formal-spec translation. See concepts/specification-driven-development.
Composition with other AWS surfaces¶
- systems/bedrock-agentcore — agent runtime that enforces capability envelopes. Guardrails reasoning checks enforces output correctness. Together they form patterns/envelope-and-verify + patterns/post-inference-verification — the full stack.
- systems/kiro — specification-authoring surface. Specs written for Kiro can feed Guardrails' reasoning checks downstream; the spec is a first-class artifact (concepts/specification-driven-development).
- systems/aws-policy-interpreter / AWS cryptography / AWS networking proofs — the decade of internal AWS automated-reasoning scaffolding is the body of practice behind this customer-facing capability. Guardrails reasoning checks repackages infrastructure that AWS has been using internally for years.
Fundamental limits¶
The automated-reasoning engine underneath inherits: - NP-complete complexity in the easier fragments. - Undecidability in the harder fragments. - Timeouts and false-rejections for specs the reasoner cannot resolve.
The product is not free verification — it is verification up to the reasoner's budget and the expressiveness of the chosen logic. Coarse-grained specs (see patterns/envelope-and-verify on guardrail preference) are generally cheaper to verify than fine-grained ones.
Composability with other Bedrock safeguards¶
Explicitly positioned as complementary, not substitutive to the four other Bedrock Guardrails features (Source: sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations):
- Denied topics / content filters / word filters / PII redaction — content-safety + privacy layers.
- Contextual grounding checks — verifies the answer is supported by the retrieved passage (RAG consistency).
- Automated Reasoning checks — verifies the answer is logically consistent with a structured policy.
Each handles a different failure mode. RAG + contextual grounding get the right passage in front of the model and reject responses that stray from it; Automated Reasoning checks enforce logical consistency with the codified rules of the domain — which cannot be captured just by passage alignment. Prompt engineering / RAG / grounding / automated reasoning form a stack, not alternatives.
Seen in¶
- sources/2024-12-04-aws-automated-reasoning-to-remove-llm-hallucinations — preview-launch announcement (2024-12-04, US West Oregon). Preview workflow: document upload → intent + sample Q/As → autoformalization → variables + rules in UI → Test playground. Three-verdict output (Valid / Invalid / Mixed results) with structured suggestions. Canonical regenerate-with-feedback Python snippet. Variable-description-as-accuracy-tuning-knob worked example (
is_full_time). Named AWS pre-Guardrails automated-reasoning usage: storage, networking, virtualization, identity, cryptography. Positioned as complementary to prompt engineering / RAG / contextual grounding checks — only major-cloud safeguard combining safety + privacy + truthfulness in one product. - sources/2026-02-17-allthingsdistributed-byron-cook-automated-reasoning-trust-ai — up to 99% provable accuracy; finance / healthcare / government target industries; autoformalization named as the UX gating problem; positioned as one of the two flagship AWS spec-driven-development surfaces (with systems/kiro).