두 개의 Scratch 프로그램은 변수 이름 변경, 스크립트 분할, 사용자 정의 블록 추출 또는 초기화 순서 변경 등으로 인해 구문론적(syntactically)으로 매우 멀리 떨어져 있을 수 있지만, 여전히 동일하게 동작할 수 있습니다. 차단형 방송(blocking broadcast)을 비동기형(asynchronous)으로 교체하는 것과 같은 단일 블록 편집은 특정 스케줄 하에서만 나타나는 차이를 만들 수 있습니다. 행동 동등성(behavioral equivalence)을 결정하는 것은 자동 피드백, 채점 지원 및 복구 검증의 핵심이지만, 트리 차이 분석(tree differencing)은 너무 엄격하며, 단일 실행 동적 비교(single-run dynamic comparison)는 병행성(concurrent), 무작위성(random), 그리고 타이밍 의존적(timing-dependent) 동작에 대해 건전하지(unsound) 않습니다. 우리는 블록 기반 프로그램의 동등성이 렌즈-매개변수적(lens-parametric)이라는 점을 관찰했습니다. 즉, 최종 상태(final state), 프레임 추적(frame traces), 모니터(monitors), 이벤트 인과관계(event causality), 그리고 디버그 추적(debug traces)이 서로 다른 관찰 관계(observation relations)를 유도합니다. ScratchLens는 인과적 발산(causal divergence) 현상과 관찰 렌즈(observation lenses)의 분류 체계를 통해 이를 명시적으로 만듭니다. 이 시스템은 Scratch 프로젝트를 타입화된 리소스(typed resources)와 의미론적 트랜잭션(semantic transactions)의 인과적 IR(causal IR)로 컴파일하고, 이름 변경(renamings), 가드(guards), 프로시저 본문(procedure bodies)을 정규화(canonicalizes)하며, Mazurkiewicz trace normal forms를 통해 동일 트리거 병행성(same-trigger concurrency)을 몫집합화(quotients)하고, 프로그램 순서(program order)를 레이스(races)와 분리하며, SMT 의무(SMT obligations)와 VM 기반의 반례 유도 정제(counterexample-guided refinement)를 통해 잔여 프런티어(residual frontiers)를 처리합니다. 최종 판결은 증거를 수반합니다: 전단사(bijection) 및 추적 몫집합(trace quotient)에 의한 동등성, 타입화된 증인(typed witness)에 의한 차이, 그리고 해결되지 않은 사례는 미정(unknown)으로 남습니다. 실제 Scratch 프로젝트에서 가져온 VM 증명 변이 코퍼스(VM-witnessed mutation corpus)에 대해, ScratchLens는 검증된 444개 쌍을 모두 결정하였으며, 엄격한 채점 기준 하에서 증명된 차이 쌍에 대해 158개 중 0개의 잘못된 동등성(false-equivalence) 주장을 했습니다. 구조적(structural), 동적 전용(dynamic-only), 그리고 LLM 베이스라인은 분류 체계에 의해 예측된 클래스들에서 실패했습니다. 절제 연구(ablations)를 통해 부분 순서 감소(partial-order reduction)와 렌즈 매개변수성(lens parametricity)의 기여도를 정량화하였으며, 타겟 시나리오를 통해 무작위 테스트에서 놓치는 모호한 변이 발산(ambiguous-mutant divergences)을 드러냈습니다.