Semantic diff for LLM-generated policies: 18 “changed” lines reveal 2 bugs

Code review starts with a diff. Nobody compares two 3,000-line files by eye. Formal policies make things harder: a text diff highlights syntax that leaves the meaning unchanged. Swap two conditions, reverse the arguments of an equality, replace a predicate with an equivalent expression, and half the file looks changed. A real bug, such as Or where the requirement says “and,” can easily get lost in that noise.

The AWS Machine Learning Blog describes an open-source engine that tackles this problem through anti-unification. This is Plotkin’s classic idea from 1970: find the most specific common template for two expressions.

Why this matters when an LLM writes the policies

The main use case here is autoformalization. You take natural-language requirements and ask a model to turn them into SMT-LIB for Z3 or cvc5, Cedar or Dogwood policies, YAML rules for the OpenShell sandbox, or CEL expressions. The model produces the artifact but takes no part in the comparison. There is no reference version. Run the model twice and you get two different formalizations, with no way of knowing which is correct.

A semantic diff shows where the candidates agree and where they diverge. You can generate more versions by changing the model, prompt, or temperature. Common sections recur from run to run and can be checked less frequently. The parts that change deserve attention first.

This is related to semantic entropy, as described by Farquhar and colleagues in Nature (2024). That approach clusters multiple answers and produces a single number. Anti-unification retains more information: it shows the shared structure and every discrepancy, rather than just a score.

How it works in an example

The engine operates on top of an e-graph, a structure that stores expressions known to be equal to one another. You declare those equalities yourself. You specify associativity, commutativity, and idempotence for And and Or. Domain-specific facts, such as “external equals not internal,” are encoded as rewrite rules. The engine treats everything else as a difference.

The result is a single term. Shared content appears once, while each discrepancy sits inside a Variants node containing both versions. Choose the first alternative in every node and you get policy A; choose the second and you get B. The merge is lossless.

The worked example involves a requirement for cross-region replication in S3: versioning, an approved destination region, the same account and encryption with a customer key for confidential objects, and multipart copying for large objects. The two formalizations differ in five places. Three differences are cosmetic: the order of conditions, a reversed Eq, and approvedRegion expanded into us-east-1 and eu-west-1. Two change the meaning. In one version, the condition for confidential objects requires both the account and encryption; in the other, either one is sufficient (And becomes Or). The size threshold uses Lte in one version and Lt in the other.

A conventional unified diff flags 18 of 28 lines without telling you which changes matter. The semantic diff removes the rearrangements and reduces the result to the nodes that need reviewing. For cases like this, there is a metric called cr, the compression ratio. Zero means complete agreement under the declared equalities, while one means there is nothing in common at all. In the example, cr is 0.5862 and the result size is 42.

Limitations and next steps

There are several caveats. The engine does not import native Cedar, Dogwood, OpenShell, or CEL policies. You manually encode the required constructs as terms and manually declare equalities. If rules are missing or the search is incomplete, a remaining difference may be an equivalence the engine failed to discover. A low cr does not prove correctness either: two candidates can make the same mistake. Also, the default search uses a Monte Carlo method, and the :completion field will show budget rather than exact if the limit is reached before all alternatives have been explored.

The practical takeaway for anyone building “requirements → formal policy” pipelines: do not trust a single model output. Generate several candidates, combine them through a semantic diff, and pass only the Variants nodes to a human or an SMT solver. The solver can find a counterexample, meaning a specific assignment under which one formula is true and the other is false, while the anti-unifier shows where to look. You can try it in five minutes: the yaspar-org/semi-persistent repository, a build with cargo build --release, and the 12-first-au.egg example.