正式政策与反统一的语义差异分析

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