要点
- Formal policies can look wildly different in a text diff after a reordering or an equivalent predicate, while a real change in meaning, such as Or where the requirement says and, gets lost in the noise.
- The engine computes a most specific common pattern of two expressions, Plotkin's 1970 anti-unification, over an e-graph that records equalities from algebraic laws and domain rules.
- In the worked policy example, a unified diff marked 18 of 28 lines changed. After canonizing associative and commutative operators and adding a domain rewrite for approved Regions, the remaining disagreements were an And that became Or, and Lte that became Lt.
- The code is Apache-2.0 at github.com/yaspar-org/semi-persistent. On the worked example, 3,000 random trials of the default search reproduced the exact solver's best result.
- A Verus-verified container layer reports 1,703 verified conditions and 0 errors for snapshot restore. The full solver does not yet have an end-to-end refinement proof, and logged justifications are not independently replay-checked certificates.
On 11 November 2026, AWS AI Labs published a method for comparing formal policies by meaning rather than by text. The immediate use is autoformalization, turning a requirements document into a formal artifact with a language model. A second run may produce a different formalization, with no ground truth sitting beside it. The model writes the artifact. It plays no part in computing the diff. The review problem is to see where two candidates agree, and where they diverge in behavior.
[1][2]How a semantic policy diff works
A semantic diff shows what two policies have in common and where they disagree. The engine finds a most specific common pattern of two expressions. That is the classical formulation of anti-unification from Plotkin in 1970. It works over an e-graph, a structure that stores a term together with everything it is known to equal. The team supplies algebraic laws and domain rules, for example treating an external destination as equal to one that is not internal. Shared structure is printed once. Each real disagreement is kept as a Variants node with both readings. If nothing remains, the policies are equivalent under those laws and rules. If the rules or the search are incomplete, a remaining difference might be an equivalence the engine has not found. That limit is in the post, and it should stay attached to every use.
The implementation choices are concrete. Associativity, commutativity, and idempotence are properties of the data structure, not rewrite rules that would flood the graph with equivalent copies. An exact dynamic-programming solver can find an optimum relative to its size-first objective and the current graph. The default is an anytime Monte Carlo graph search. Semi-persistent snapshots let the engine compare many candidates without copying the full graph each time.
The intended artifacts include SMT-LIB, the standard input for solvers such as Z3, as well as Cedar and Dogwood authorization policies, OpenShell sandbox rules for an agent's filesystem and network access, and CEL expressions embedded in applications.
[1][2]A worked example, not a scored corpus
The clearest evidence is a small, inspectable case, not a large benchmark. Two encodings of a policy differ in five textual ways. Three are presentational: conjuncts reordered, equality arguments swapped, and an approvedRegion predicate expanded into us-east-1 and eu-west-1. Two change operators: And became Or in a confidential-object clause, and Lte became Lt at a size threshold. A unified text diff marked 18 of their 28 lines as changed and did not say which of the five differences change meaning.
The semantic diff dropped the reordering and the swapped equality, because those are equivalent under the declared laws. After a domain rewrite stating that the approved Regions are exactly those two, the Region difference also disappeared. What remained was the confidential clause, in which the second encoding accepts either same-account or encryption and therefore allows cross-account replication of confidential objects, and the strictness of the size threshold. That is the review a human actually needed.
The post also walks through Cedar, Dogwood, OpenShell, and CEL examples, including disagreements about requiring ownership and approval versus accepting either, and about the scope of an agent's network access. Those are illustrations of the same comparison, not a scored set of labeled policy pairs.
[1][2]What is verified, and what is not
The repository is public, and the post asks readers to build a pinned revision from pull request 103. On the worked example, 3,000 random trials of the default search reproduced the exact best result. The e-graph's container layer is verified in Verus, a verifier for Rust. The claimed property is that restore reproduces the state at the matching snapshot push, with 1,703 verified conditions and 0 errors. The anti-unification crate proves objective-order and lower-bound lemmas, but there is not yet a proof that the whole solver matches its specification. The engine can log a justification for every derived equivalence. Those records are not yet independently replay-checked certificates. The authors point to a claims inventory in the repository. That limit belongs in any write-up of a tool that may be used on authorization policy.
[1][2]A fair objection
The method does not tell you which formalization matches the original prose, or the world. It tells you where two formalizations differ once you have stated the equalities you believe in. If you omit a domain fact, a harmless vocabulary difference looks like a bug. If your rules are too strong, a real disagreement can be rewritten away. There is no reported precision or recall on a large set of policy pairs with known labels. Subsecond queries are described as practical after native canonization of associative and commutative operators, but the post does not publish a timing table across policy sizes. A skeptical editor should treat the worked examples as existence proofs, and wait for a labeled evaluation before calling this a standard review gate.
[1][2]What to watch in the next six months
The useful test is whether autoformalization pipelines start to cluster equivalent candidates with this engine, or a similar one, and send only the recurring disagreements to a human or a solver. Watch for a public evaluation on Cedar policies or agent sandbox rules, with counts of equivalent rewrites correctly ignored and meaning changes correctly kept. If that evaluation does not appear, the tool remains a carefully built laboratory example. If it does, pasting two model outputs into a text diff should look as inadequate as comparing 3,000-line files by eye, which is how the post begins.
[1][2]