When reviewing code, you start with a diff. You wouldn’t compare two 3,000-line files by eye and hope to spot every change. Formal policies can be even harder to compare because a textual diff often highlights syntactic changes that don’t affect meaning. Reorder two conjuncts, swap the arguments of an equality, or use an equivalent predicate, and much of the file might appear changed. A real change in behavior, such as an Or where the requirement says and, can get lost in that noise.
A semantic diff shows what two policies have in common and where they disagree. The open source engine used in this post computes this diff using anti-unification, which finds a most specific common pattern for two expressions. Plotkin’s 1970 paper gives the classical formulation. The engine works over an e-graph, which keeps track of expressions known to be equal. We supply the algebraic laws and domain rules that justify those equalities, such as equating an external destination with one that isn’t internal. The result shows the shared parts once and keeps both versions of each differing part for review. If no differences remain, the policies are equivalent under those laws and rules. When the rules or the search are incomplete, a remaining difference might reflect an equivalence the engine has not found.
One use case is autoformalization. Autoformalization translates natural language into a formal language. Suppose you want to turn requirements into SMT-LIB, the standard input language for satisfiability modulo theories (SMT) solvers such as Z3 and cvc5, or into Cedar or Dogwood to control authorization in your software system. A large language model (LLM) generates the formal artifact from the prose. The model writes the artifact. It plays no part in computing the diff. Run the model twice, and it might produce two different formalizations, with no ground truth to identify the correct one. A semantic diff shows where they agree and where they differ. Generate more candidates by varying the model, prompt, or sampling temperature. Comparing them shows which parts stay the same and which vary. Review the varying parts first.
Requirements can also become OpenShell sandbox policies or Common Expression Language (CEL) expressions. OpenShell uses YAML to describe an agent’s filesystem and network access. CEL is embedded in applications to evaluate expressions, including policy conditions. These languages and formats differ in what they express, but translations into any of them can disagree about a condition, a scope, or an event. The following table gives illustrative disagreements:
| Language or format | Policy focus | Example disagreement |
| Cedar | Who can perform an action on a resource, under which conditions. | One translation requires ownership and approval. Another accepts either. |
| Dogwood | Authorization involving the current request and recent event history. | One translation checks a successful prior response. Another checks a request event. |
| OpenShell policies | An agent’s filesystem and network access, including rules for particular binaries. | One translation permits repository-scoped GET. Another permits organization-scoped POST. |
| CEL | Conditions evaluated over inputs supplied by a host application. | One translation requires production for both allowed ports. Another requires it for only one. |
In each worked example, we compare translations of the same requirement within one policy context. We encode the relevant syntax as terms and declare the equalities used in the comparison. The engine reads these encodings. It doesn’t import native policies from the four formats.
The idea is a formal-methods analogue of semantic entropy, described by Farquhar et al. in Nature (2024). That approach samples several natural-language answers, clusters those that entail one another, and reports a single number. For formal outputs, anti-unification preserves more information. It identifies the shared structure and each divergence instead of returning only a score.
Counterexamples help explain the consequences of a disagreement. An SMT solver can find a concrete assignment that satisfies one formula and violates the other. A reviewer can then trace that assignment through the formulas to understand the conflicting decisions. The anti-unifier gives a different view: it organizes the shared structure and the fragments that differ, without issuing an SMT query. A solver or policy validator can help resolve those fragments. We assume you can read S-expression syntax, as in SMT-LIB, and know what an authorization policy is. E-graphs and anti-unification are explained as they come up.
When several translations agree on part of a requirement, the diff shows that part once. Where they disagree, it keeps the alternatives visible for review.
How semantic diffing represents disagreement
Say a policy-generation pipeline hands you two candidate rules for this requirement: sensitive data sent to an external destination must be encrypted.
| Rule A | Rule B |
| sensitive(data) ∧ external(dst) → encrypted | ¬internal(dst) ∧ sensitive(data) → audited |
Whether these are the same rule isn’t obvious. The conditions are reordered, external is expressed indirectly as not internal, and the conclusions do not match. The engine computes a most specific anti-unifier for these terms. In its input language, the two rules are S-expressions.
The complete program first declares the vocabulary:
It then adds one function line for each predicate (sensitive, external, internal) and constant (data, dst, encrypted, audited). Here, And is declared associative, commutative, and idempotent, as the next section explains:
The engine answers with a single term:
The reordering doesn’t appear in the result because And is declared associative, commutative, and idempotent. Two Variants nodes remain, each marking a place where the inputs disagree, and only one of them is a difference in meaning. The difference between (external dst) and (Not (internal dst)) is a difference in vocabulary. Both express the same domain fact. The engine can’t infer that from syntax alone. State the domain fact as a rewrite, run it to saturation (until no rule adds a new equality), and diff again:
After saturation, the engine answers:
One Variants node remains: Rule B audits where the requirement demands encryption. A textbook presentation would put a fresh variable at that spot. The engine instead writes (Variants encrypted audited): a node that holds both readings. Select the first child of every Variants node and you reconstruct rule A, up to the declared algebra and rewrites. Select the second child and you get rule B. The anti-unifier is a lossless merge of both terms: Shared structure appears once, and every genuine disagreement is a localized, reviewable node.
Three fields describe the result: :size, :cr, and :completion. The :size field counts the concrete nodes (a Variants marker itself isn’t counted, but both of its children are, so structure can’t hide inside one).
The :cr field reports the compression ratio (s - a) / b, where s is the result size and a and b are the smaller and larger input sizes. For each input, we use its smallest known equivalent form in the current e-graph. A score of 0 means full agreement under the declared equalities.
After the preceding rewrite, both inputs have seven nodes and the result has eight, giving (8 - 7) / 7, or approximately 0.1429. Keeping both complete policies in a single Variants node would use fourteen nodes, giving (14 - 7) / 7 = 1. This is the reference value for no sharing.
A score of 1 is a reference value, not an upper bound. The search might use larger equivalent forms than the smallest known inputs. A result larger than their combined sizes therefore scores above 1. For example, if both smallest input forms have ten nodes and a result has twenty-three, the ratio is (23 - 10) / 10 = 1.3.
The :completion field reports exact when the search space was exhausted and budget when the default anytime search (a Monte Carlo search, described in the implementation section) reached its playout limit before exhausting the search space.
A low :cr means the inputs share more structure under the declared equalities. It doesn’t establish correctness: two candidates can share the same mistake. An entropy score summarizes variation in one number. The full semantic diff also identifies where the candidates disagree and retains both alternatives in Variants nodes.
A semantic diff ignores only the differences covered by the declared equalities. A plain syntactic anti-unifier would also have reported the reordering in this example. The next three sections show how to declare the algebra and add domain identities.
The anti-unifier stores shared structure once and marks each disagreement with a Variants node. Selecting one side of every node reconstructs the corresponding input, modulo the declared equalities.
Run a semantic diff in 5 minutes
The engine requires only a pinned Rust toolchain to build from source. Its formal-verification annotations, covered in the implementation section, compile away under plain rustc. These commands pin the revision used for the worked examples:
It prints a single (anti-unify ...) term.
The command-line interpreter reads one S-expression file (.egg by convention). You declare sorts and operators, define two terms with let, optionally add rewrite rules and run them to saturation, and issue antiunify. Two mechanisms tell the engine which syntactic changes do not affect meaning: annotations that assign algebraic properties such as associativity, commutativity, and idempotence to operators, and explicit rewrite rules for everything else. Here is the algebraic part of the signature used in the worked example:
And and Or are variadic, associative, commutative, and idempotent, and each has a Boolean neutral element. Eq is commutative. Every reordering, regrouping, and duplication of conjuncts therefore counts as the same term. Nothing else is assumed: Only the stated laws hold, and any further identities must be written as explicit rewrites. The :identity element is what lets the diff align a conjunct that one input has and the other lacks: The missing conjunct is paired with (Lit true) rather than causing the entire And expression to fail to align. Both case studies rely on this identity alignment.
:assoc-comm-idem makes reordered, regrouped, and duplicate operands equivalent. :identity lets the diff align a missing operand with the operator’s neutral element.
Worked example with two policy bugs
The running example ships with the repository as egraph/examples/au_policy_divergence.egg. Consider one policy sentence:
A cross-Region replication request is permitted only if the source bucket has versioning enabled and the destination bucket lies in an approved Region. If the object is tagged confidential, the destination and source accounts must be the same and server-side encryption with a customer managed key must be in effect. Objects up to the multipart threshold are copied directly. Larger objects require a multipart copy.
Two people, or two independent runs of the same model, produced formalizations of it (formulaA and formulaB in the file):
| Encoding A | Encoding B |
Five things differ textually. Three are presentational: The conjuncts are reordered, the Eq arguments are swapped, and approvedRegion is explicitly expanded into two AWS Regions (us-east-1 and eu-west-1). Two involve different operators: An And became an Or in the confidential clause, and Lte became Lt at the size threshold. A unified diff of the two encodings marks 18 of their 28 lines as changed (Figure 1, textual-diff pane) and gives no indication of which of the five differences change meaning. The exact anti-unifier of the two encodings follows:
Two of the five differences disappear. The conjunct reordering is absorbed because And is declared associative, commutative, and idempotent (ACI). The swapped Eq arguments have the same printed order in both readings because :comm canonized them. Neither changes meaning, so neither is reported.
The confidential clause uses Or where the requirement says and. Encoding A requires both the same-account check and server-side encryption with a customer managed key. Encoding B accepts either. The engine aligns A’s conjunction with B’s disjunction through their neutral elements, so the disagreement surfaces as two adjacent Variants nodes. Choose the first child at each node to reconstruct A: The Or collapses onto the plain equality, and sseCmk remains a mandatory conjunct. Choose the second child at each node to reconstruct B: The mandatory sseCmk weakens to (Lit true) and survives only as an alternative inside the Or. Together, the two Variants nodes show that encoding B accepts server-side encryption alone and therefore admits cross-account replication of confidential objects.
You might have expected sseCmk to be shared rather than repeated. However, a first-order anti-unifier can’t generalize the connective itself, so And versus Or forces the split into two alignments. Identity alignment still shares the five-node equality once. The exact solver’s exhaustive search finds no smaller form, and the printed result is one node smaller than holding both clauses whole in a single Variants.
Add the domain rewrite and run the diff again. The Variants node for the Region is not a bug. It reflects missing domain knowledge: In this deployment, the approved Regions are exactly those two. State that as a rewrite, saturate, and diff again:
The Region difference moves into the shared backbone, and :cr drops from 0.5862 to 0.4000. The full result is the semantic-diff pane of Figure 1. Exactly two disagreements remain: the weakened confidential clause and the threshold. B’s Lt is strict, so an object exactly at multipartThreshold is copied directly under A and takes the multipart path under B. The divergence is confined to the Ite condition. Both branches sit in the shared backbone. Both surviving differences are genuine bugs that an authorization reviewer must resolve. The algebra and one domain rewrite account for the other differences. The same file also runs the anytime search, (antiunify formulaA formulaB :algorithm uct :playouts 3000), which returns the identical size-35 term. The whole program completes in well under 100 ms on an Apple M3 Pro laptop (50–60 ms after the binary is warm). That covers parsing, declarations, saturation, five anti-unification queries with their regression checks, and process startup. We measured the wall-clock time of ./target/release/semi-persistent egraph/examples/au_policy_divergence.egg using a release build at Rust 1.97.1 and the shell’s time command over five warm runs. The Get started section shows the same command.
| textual diff: 18 of 28 lines flagged | semantic diff: two disagreements, localized |
Figure 1: The same pair of encodings under diff and anti-unification. On the left, the textual diff flags 18 of 28 lines (removed, added). On the right, one domain rewrite moves the shared structure into the gray backbone, and the highlighted Variants confine the remaining differences to the weakened confidential clause and the strict threshold. The semantic-diff pane wraps one long line to fit
After applying the declared algebra and one domain rewrite, the five textual differences reduce to two semantic disagreements: the weakened confidential clause and the strict size threshold.
Semantic diffing for Cedar and Dogwood policies
In an authorization policy, a dropped guard widens what is permitted and can cause the policy to fail open. Cedar is the open source authorization policy language behind Amazon Verified Permissions. Dogwood extends Cedar authorization policies with temporal conditions for runtime verification of AI agents. Its temporal sublanguage uses recorded event history to guard an action. The engine doesn’t evaluate Dogwood policies. It diffs their abstract syntax modulo a declared algebra. Validation (schema checking) and replay (evaluating a policy against a recorded event history) remain Dogwood’s job. The engine’s user guide has a worked chapter that diffs two independently produced Dogwood candidates for one requirement:
The agent may POST to /deploy, but only if a health check has already come back 200 in the last 15 minutes.
Candidate A keeps both request guards (method and path) but reads the status code from a request event, an event kind that carries no such field. Candidate B uses the correct response event but drops the /deploy path guard. After any matching health check, B also permits a POST to /admin/purge-all. The candidates differ in six additional presentational ways, all of which the declared algebra or a three-rule comparison theory absorbs:
| Presentational difference | Absorbed by |
| Cedar condition order | eAnd :assoc-comm-idem |
| temporal conjunction order | tAnd :assoc-comm-idem |
| predicate field order | args :assoc-comm-idem |
method == "POST" versus "POST" == method | eEq :comm |
15m versus 900s | unit rewrite + constant fold |
count >= 1 versus 1 <= count | (birewrite (tLte a b) (tGte b a)) |
The comparison theory consists of three visible rewrites, not a hidden normalization pass:
The anti-unifier of the two candidates (doc/book/examples/20-dogwood-simple.egg in the repository) has size 61, :cr 0.1864, and exactly two disagreements in an otherwise shared policy backbone:
Use the simplest available check for each disagreement. Two binary disagreements give four candidate completions. Dogwood validation resolves the first without human review by rejecting both request completions (“predicate … mentions field output.status_code, which is not declared on that event”). The second disagreement is an identity alignment: Candidate A’s path guard pairs against eTrue, showing that candidate B omitted the guard. The requirement resolves it (keep the guard), and a replay covering two decision points shows the consequence: After a health check, candidate B allows the off-target POST, whereas the repaired policy denies it. Combining B’s event kind with A’s guard produces a policy that neither candidate wrote. Choosing between the candidates would have kept one of the two bugs.
Commutativity has a side condition, and the engine doesn’t check it. Cedar’s && short-circuits, so commuting it is sound only when neither operand can raise an error. The comparison therefore relies on validation to rule out order-dependent errors, such as an attribute access that is safe only behind a has guard. The engine doesn’t re-check that condition.
A canonical printer can remove the presentational differences, but it can’t recover a dropped guard. A canonizing printer plus textual diff can absorb most, arguably all, of the six differences in the table more cheaply. No normalizer can align a two-conjunct condition against a three-conjunct one inside an otherwise matched term. Matching modulo the identity element aligns them by pairing the dropped conjunct with eTrue. In a permit condition, that dropped conjunct exposes the widening that makes the policy fail open.
For the Dogwood candidates, the algebra and three rewrites remove six presentational differences. The remaining disagreements expose a schema error and a dropped guard. Combining the correct choices produces a policy that neither candidate supplied.
Comparing policy translations: OpenShell and CEL
The next two examples adapt predicates from the OpenShell and CEL articles. For each, we construct candidate translations of the same requirement. These are illustrative encodings, not recorded LLM samples.
OpenShell: Method and path scope. The OpenShell example models network permissions as predicates over a binary, host, port, layer, method, and path. We adapt the article’s reduced SMT-LIB model, whose path condition is a prefix test. We use that vocabulary for this requirement:
Allow inspected REST requests made by /usr/bin/gh to api.github.com on port 443 when the method is GET and the path begins with /repos/NVIDIA/OpenShell/issues/. Deny all other requests.
Candidate A requires GET and the repository’s issues prefix. Candidate B uses POST and the broader /repos/NVIDIA/ prefix. The other checks appear in a different order. In the encoding, gh, github, and https name the binary, host, and port shown earlier. The names issuePrefix and orgPrefix identify the two prefixes. The exact solver returns:
The binary, host, port, and layer checks are shared. Their ordering disappears because And is declared associative, commutative, and idempotent. Two Variants nodes identify the conflicting readings: the permitted operation and the path scope. The requirement settles both choices here. For an ambiguous requirement, the same nodes would give its owner two specific alternatives to resolve.
CEL: The scope of a shared condition. The CEL example exposes a production check lost during refactoring. We reuse the expressions as candidate translations of this requirement:
Allow a request exactly when it is in production and its port is either 80 or 443.
CEL’s && binds more tightly than ||, so candidate B applies the production check only to port 80. We encode the expressions with supplied Boolean and integer inputs, using isProd, port80, and port443 for the corresponding input and literals:
The port-80 branch is shared. In the port-443 branch, (Variants isProd (Lit true)) shows the missing production condition. At is_prod = false and port = 443, A denies the request and B allows it. The diff directs the review to one part of the sentence: whether “in production” applies to both alternatives.
This example assumes that is_prod is supplied as a Boolean and port as an integer. Under these assumptions, neither expression raises an error. The encoding doesn’t model CEL errors or unknown values, and the engine doesn’t check these input assumptions.
CEL-Java’s verification framework can check equivalence and policy invariants with Z3. Such checks can provide evidence when resolving a disagreement. The anti-unifier itself doesn’t decide which translation matches the requirement, and a mistake shared by both candidates would remain shared.
Implementation and performance
The algorithm runs over an e-graph, a data structure that stores a term together with everything it is known to equal. E-graphs (equivalence graphs) come from congruence-closure procedures in theorem provers and were popularized for compiler optimization by equality saturation, as described by Willsey et al. in “egg: Fast and Extensible Equality Saturation” (POPL 2021). This engine’s e-graph adds native canonization for associative and commutative operators.
Anti-unification over e-graphs is also used for abstraction learning and program compression in babble (Cao et al., POPL 2023). Earlier implementations didn’t scale beyond small examples. Our saturation-based prototype also stalled there. Native AC canonization, AC-aware matching over distinct children, and direct search made subsecond queries practical. Semi-persistence reduced the cost of repeated queries.
Native AC canonization. Associativity, commutativity, and idempotence are not rewrite rules in this engine. They are properties of the data structure. Associative-commutative (AC) operators store their children as canonical sorted multisets (...
