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: 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: ( 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 smalles