Semantic diffing of formal policies with anti-unification

The post describes an open source engine that computes semantic diffs of formal policies by anti-unification over an e-graph, using declared algebraic laws and domain rewrites so that shared structure appears once and each genuine disagreement is kept as a Variants node. Worked examples cover SMT-LIB-style rules, Cedar and Dogwood authorization policies, and OpenShell and CEL encodings, showing how presentational differences are absorbed while real bugs such as a weakened conjunction or a dropped guard remain visible. The engine builds from source with a pinned Rust toolchain and reads a single S-expression file.