Semantic diffing of formal policies with anti-unification

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:

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.

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:

(sort Formula)
(sort Data)
(sort Dest)
(function Lit (bool) Formula)
(function And (Formula) Formula :assoc-comm-idem :identity (Lit true))
(function Implies (Formula Formula) Formula)
(function Not (Formula) Formula)

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:

(let ruleA (Implies (And (sensitive (data)) (external (dst)))
                    (encrypted)))
(let ruleB (Implies (And (Not (internal (dst))) (sensitive (data)))
                    (audited)))

(antiunify ruleA ruleB :algorithm exact)

The engine answers with a single term:

(anti-unify :size 11 :cr 0.5000 :completion exact
  (Implies
    (And (sensitive data) (Variants (external dst) (Not (internal dst))))
    (Variants encrypted audited)))

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:

(rewrite (external d) (Not (internal d)))
(run 2)
(antiunify ruleA ruleB :algorithm exact)

After saturation, the engine answers:

(anti-unify :size 8 :cr 0.1429 :completion exact
  (Implies (And (sensitive data) (external dst)) (Variants encrypted audited)))

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:

git clone https://github.com/yaspar-org/semi-persistent.git
cd semi-persistent
git fetch origin 5a7969ae4ea88117a64faac4f42af5c358e213e2
git checkout --detach FETCH_HEAD
cargo build --release
./target/release/semi-persistent doc/book/examples/12-first-au.egg

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:

(function Lit (bool) Formula)
(function And (Formula) Formula :assoc-comm-idem :identity (Lit true))
(function Or  (Formula) Formula :assoc-comm-idem :identity (Lit false))
(function Eq  (Account Account) Formula :comm)

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):

(Implies (permit)
  (And
    (versioningOn (src))
    (approvedRegion (regionOf (dst)))
    (Implies
      (taggedConfidential (obj))
      (And
        (Eq (accountOf (dst)) (accountOf (src)))
        (sseCmk)))
    (Ite
      (Lte (sizeOf (obj)) (multipartThreshold))
      (directCopy)
      (multipartCopy))))

(Implies (permit)
  (And
    (Ite
      (Lt (sizeOf (obj)) (multipartThreshold))
      (directCopy)
      (multipartCopy))
    (Implies
      (taggedConfidential (obj))
      (Or
        (Eq (accountOf (src)) (accountOf (dst)))
        (sseCmk)))
    (Or
      (usEast1 (regionOf (dst)))
      (euWest1 (regionOf (dst))))
    (versioningOn (src))))

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:

(anti-unify :size 42 :cr 0.5862 :completion exact
  (Implies
    permit
    (And
      (Implies
        (taggedConfidential obj)
        (And
          (Or (Eq (accountOf dst) (accountOf src)) (Variants (Lit false) sseCmk))
          (Variants sseCmk (Lit true))))
      (Ite
        (Variants
          (Lte (sizeOf obj) multipartThreshold)
          (Lt (sizeOf obj) multipartThreshold))
        directCopy
        multipartCopy)
      (versioningOn src)
      (Variants
        (approvedRegion (regionOf dst))
        (Or (usEast1 (regionOf dst))
            (euWest1 (regionOf dst)))))))

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:

(rewrite (approvedRegion r) (Or (usEast1 r) (euWest1 r)))
(run 3)
(antiunify formulaA formulaB :algorithm exact)

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.

 (Implies (permit)
   (And
-    (versioningOn (src))
-    (approvedRegion (regionOf (dst)))
+    (Ite
+      (Lt (sizeOf (obj)) (multipartThreshold))
+      (directCopy)
+      (multipartCopy))
     (Implies
       (taggedConfidential (obj))
-      (And
-        (Eq (accountOf (dst)) (accountOf (src)))
+      (Or
+        (Eq (accountOf (src)) (accountOf (dst)))
         (sseCmk)))
-    (Ite
-      (Lte (sizeOf (obj)) (multipartThreshold))
-      (directCopy)
-      (multipartCopy))))
+    (Or
+      (usEast1 (regionOf (dst)))
+      (euWest1 (regionOf (dst))))
+    (versioningOn (src))))

(anti-unify :size 35 :cr 0.4000 :completion exact
  (Implies
    permit
    (And
      (Implies
        (taggedConfidential obj)
        (And
          (Or (Eq (accountOf dst)
                  (accountOf src))
              (Variants (Lit false) sseCmk))
          (Variants sseCmk (Lit true))))
      (Ite
        (Variants
          (Lte (sizeOf obj) multipartThreshold)
          (Lt (sizeOf obj) multipartThreshold))
        directCopy
        multipartCopy)
      (versioningOn src)
      (approvedRegion (regionOf dst)))))

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:

The comparison theory consists of three visible rewrites, not a hidden normalization pass:

(rewrite (mins x) (secsTimes x 60))
(rewrite (secsTimes x y) (secs (IBig::* x y)))
(birewrite (tLte a b) (tGte b a))
(run 4)

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:

(anti-unify :size 61 :cr 0.1864 :completion exact
  (rule
    permit
    (head anyPrincipal (actionEq aHttpRequest) anyResource)
    (eAnd
      (eEq (eCtx (fld fInput (fld fMethod fnil))) (eStr vPOST))
      (temporal
        ...
                  (pred
                    aHttpRequest
                    (Variants request response)
                    ...
      (Variants
        (eEq (eCtx (fld fInput (fld fPath fnil))) (eStr vDeploy))
        eTrue))))

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:

(anti-unify :size 21 :cr 0.1053 :completion exact
  (And
    (EqText binary gh)
    (EqText host github)
    (EqText layer rest)
    (EqText method (Variants GET POST))
    (EqNumber port https)
    (Prefix (Variants issuePrefix orgPrefix) path)))

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.

// Candidate A
(is_prod && port == 80) || (is_prod && port == 443)

// Candidate B
is_prod && port == 80 || port == 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:

(anti-unify :size 13 :cr 0.3636 :completion exact
  (Or
    (And (Eq port port443) (Variants isProd (Lit true)))
    (And isProd (Eq port port80))))

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 (ACI operators as canonical sorted sets) at insertion time. One e-node therefore represents all reassociations and permutations of a term and, for idempotent operators, treats duplicate children as one. Equality modulo the declared laws is structural equality. The rewrite-based alternative floods the e-graph with an exponential family of equivalent copies before real work starts.

AC-aware matching over distinct children. Pattern matching against multiset nodes uses maximum-partition semantics: It branches over the distinct children of a node rather than enumerating multiplicity splits, so heavily repeated arguments do not cause a combinatorial blowup.

Direct search instead of rewriting. Anti-unification itself isn’t encoded as rewrite rules either. An exact dynamic programming solver (:algorithm exact) solves the joint-decomposition problem optimally. Optimal here is relative to its size-first objective, the current e-graph, and the configured cycle policy. An anytime Monte Carlo graph search (:algorithm uct, the default) returns its best answer for any playout budget. On the worked example’s pair, 3,000 playouts reproduce the exact optimum. Both optimize first for result size and then, among equal-size answers, prefer those that retain more structure in the shared backbone.

Semi-persistence. The e-graph supports (push) and (pop) snapshots recorded as sparse diffs rather than deep copies. Restoring a state therefore costs work proportional to what changed because the snapshot, plus the cost of repairing derived indexes. Proportional-cost restore lets the engine compare many candidates over one shared graph. A backtracking search can restore an earlier state without copying the full graph.

A verified core and its scope. The e-graph’s underlying container layer is verified in Verus, a verifier for Rust. The verified property is that restore reproduces the state at the matching (push) (1,703 verified conditions, 0 errors). The anti-unification crate proves its objective-order and lower-bound lemmas, but the full solver doesn’t yet have an end-to-end refinement proof. The engine can log a justification for every equivalence it derives (--proofs). As the repository notes, these records aren’t yet independently replay-checked certificates. All of these claims, with evidence tiers and retractions, are in the repository’s claims inventory (doc/claims.md).

Native canonization avoids materializing equivalent AC terms. Distinct-child matching controls multiplicity, direct solvers avoid encoding anti-unification as rewrites, and semi-persistence reduces the cost of repeated queries.

Using semantic diffing in a pipeline

The same method extends from two candidates to a larger sample. Generate N candidate formalizations of the requirement. Load them into one shared e-graph, saturate under your domain rules, and cluster them using pairwise equality checks. In the user guide’s larger Dogwood study, five samples collapse into three clusters. Candidates that differ only in presentation join the same equivalence classes during construction. Anti-unify the cluster representatives pairwise. Then, in a layer built on top of the engine’s output, group recurring Variants nodes by their position in the shared backbone. In the study, three pairwise diffs reduce to exactly two review items. Use the simplest available check for each item: schema validation, replay, example I/O pairs, or human review.

With (push) and (pop) snapshots, you can test a proposed resolution without rebuilding the graph. Temporarily assert one branch of a Variants node as a domain fact, run the diff again, and roll back. A tool built on top of the engine could select and repair a full candidate against hard and soft constraints, for example with a MaxSMT solver over the variant space. MaxSMT (maximum satisfiability modulo theories) seeks a solution that satisfies all hard constraints while satisfying as many soft constraints as possible, or maximizing their total weight. Section 8 of Programming Z3 describes this form of optimization. That capability is not part of the current engine. Figure 2 summarizes the pipeline.

Figure 2: A pipeline for clustering candidate formalizations, locating recurring disagreements, and routing each disagreement to an appropriate check. Cluster sizes and review-item counts are from the user guide’s larger Dogwood study

Use a semantic-diff budget in continuous integration (CI). The command (checkau A B :max_size N :algorithm exact) prints nothing on success and causes the program to fail when the anti-unifier exceeds the budget. Every printed result in the user guide is pinned this way, so the guide and the engine can’t drift apart. The same command can serve as a regression gate. Set a maximum result size for a reference formalization and a regenerated one, and fail the pipeline when the anti-unifier exceeds it. The binary follows standard shell conventions: Results go to stdout, diagnostics (ok --- N nodes) go to stderr, and the process exits non-zero if any check fails.

The diff can also guide a follow-up prompt or a question to the requirement owner. Mean pairwise :cr across samples gives a disagreement score for each requirement. A Variants node already contains the alternatives needed for a specific clarification, such as “did you mean strictly less than the threshold, or at most?”

With several candidates, cluster equivalent outputs, compare the cluster representatives, and resolve recurring disagreements with validation, replay, examples, or human review.

Get started

Build the engine at the revision used for this post, then run the policy examples. These commands select the revision containing the OpenShell and CEL examples from pull request 103:

git clone https://github.com/yaspar-org/semi-persistent.git
cd semi-persistent
git fetch origin 5a7969ae4ea88117a64faac4f42af5c358e213e2
git checkout --detach FETCH_HEAD
cargo build --release        # toolchain auto-pinned; Verus not required

# The worked example from this post:
./target/release/semi-persistent egraph/examples/au_policy_divergence.egg

# The Dogwood policy-diff example:
./target/release/semi-persistent doc/book/examples/20-dogwood-simple.egg

# The constructed OpenShell and CEL translation examples:
./target/release/semi-persistent egraph/examples/au_openshell_policy.egg
./target/release/semi-persistent egraph/examples/au_cel_policy.egg

# Your own formulas: declare a signature, two terms, and antiunify:
./target/release/semi-persistent MY_PROGRAM.egg

The engine is Apache-2.0 on GitHub. The user guide progresses from basic terms to the policy case studies, and the test suite runs every program in it directly from the repository. Annex B documents the antiunify and checkau commands. If your artifact language has an abstract syntax tree (AST) and an equational theory, you can diff it: Declare the algebra, state the domain identities as rewrites, and ask for the most specific anti-unifier. If your policies are Cedar, whether handwritten or generated for Amazon Verified Permissions, the same recipe applies to them. The OpenShell and CEL examples show how to encode other policy constructs and compare candidate readings of a requirement.

About the authors