형식 정책의 반단일화 기반 의미적 차이

오픈소스 엔진은 형식 정책 간의 의미적 차이를 반단일화(anti-unification)로 계산한다. 공통 부분은 한 번만 보여 주고, 서로 다른 부분은 양쪽 버전을 모두 남겨 검토할 수 있도록 한다. LLM이 생성한 SMT-LIB나 Cedar 등 여러 후보를 비교하는 용도가 제시되어 있으며, 주어진 대수 법칙과 도메인 규칙으로 동등하다고 판정하지 못하면 차이가 그대로 남는다. 규칙이나 탐색이 불완전한 경우, 남은 차이는 아직 발견되지 않은 동등성을 반영하고 있을 수 있다.