August 2026 · AWS
Formal policy refinement for AI safety & security ships in Amazon Bedrock
Some of my science work in formal policy refinement for AI safety and security shipped in Amazon Bedrock's Automated Reasoning checks, announced on the AWS Machine Learning Blog in a post I co-authored with Nafi Diallo and Fernando Galves. The methods reduce a quiet safety and security risk: a policy that a model can read two ways.
Opinions expressed in this post are my own and do not necessarily reflect the views of my employer. Information here is limited to what has been publicly announced by AWS.
An Automated Reasoning policy is a formal translation of a customer's written rules; a chatbot's answers are checked against it by a solver rather than scored by another model. Writing the policy is the hard part, and until now the diagnose-and-fix loop was manual. The new feature automates it in two modes. Iterative Refinement proposes rule or variable changes when saved tests fail because the logic is wrong. Ambiguous Variable Refinement rewrites or merges variable descriptions when tests come back translation ambiguous. Both run as build workflows that simulate candidate changes against the test suite until they converge, then present a diff with per-test before-and-after outcomes. You approve every change, and a Fidelity Report checks the result for drift from the source document.
The ambiguity problem is the one I worked on, and it is a security problem before it is a usability one. When a policy's variable names and descriptions are vague or overlapping, language models cannot agree on which variable a piece of text refers to, and they produce competing formal translations. A guardrail built on the wrong reading can wave through an answer the policy was written to forbid, and the mistake is invisible because every individual translation looks plausible. Our neuro-symbolic approach uses a theorem prover to judge whether candidate translations are semantically equivalent, quantifies the disagreement with formal semantic entropy, and applies symbolic compression to pinpoint exactly which variables cause the confusion. The system ranks the ambiguities by how much disagreement they cause and resolves the most problematic variables first, while keeping every rule grounded in the source text.
It is the same principle as the redundant-formalization step in Automated Reasoning checks, turned into a repair tool: where independent translations agree, trust the backbone; where they diverge, that is where the policy needs a human's attention.