Scratch와 같은 블록 기반 최종 사용자 언어는 수천만 개의 프로그램을 실행합니다. 기존 도구들은 검증된 보장 없이 프로그램 분석과 테스트를 통해 동작 보존을 확립합니다. 우리는 최적화를 인증서를 동반한 소스 대 소스 (source-to-source) 재작성으로 전환합니다. 신뢰할 수 없는 최적화 도구(optimizer)가 재작성을 제안하면, 신뢰할 수 있는, 실패 시 차단되는(fail-closed) 검사기(checker)가 명시적인 관찰 렌즈(observation lens) 하에서 재작성의 동작 보존이 의존하는 모든 부수 조건(side condition)을 재계산한 후에만 이를 수락합니다. 검사기가 유일한 권위입니다. 올바른 검사기와 명시적으로 기술된 작은 모델-VM 가정 집합이 주어지면, 최적화 도구의 버그가 부정확한 수락을 만들어낼 수 없습니다. 관찰 렌즈는 매개변수이며, 핵심적인 건전성 논거는 협력 프레임 정교화 정리(cooperative-frame refinement theorem)입니다: 어떤 스레드도 관찰하기 전에, 그리고 어떤 스레드도 양보하지 않는 창(window) 내에서 덮어쓰여진 쓰기는 제거될 수 있습니다. 우리는 Lean에서 이 정리를 기계화하였으며, 하나의 매개변수화된 문장이 가변 상태(variable state)와 렌더러 상태(renderer state)로 인스턴스화된 두 가지 구체적인 재작성 제품군을 포괄함을 보여줍니다. 우리는 6개의 재작성 제품군에 대한 검사기를 구축하고 300개의 실제 Scratch 프로젝트에서 이를 평가했습니다. 검사기는 프로젝트의 94.3%(300개 중 283개)에서 동작을 보존하는 재작성을 수락했습니다. 인증 비용은 프로젝트당 1/10초 미만이며, 4,278개의 섭동된(perturbed) 재작성으로 구성된 제품군 간 적대적 캠페인은 0개의 잘못된 수락(false accepts)을 생성했습니다. 감사 결과, 제품군별 테스트 스위트가 놓친 8개의 잘못된 수락을 발견했으며, 현재는 각각 거부됩니다. 분석과 테스트만 남기고 의미론적 부수 조건을 제거한 절제 연구(ablation)에서는 가상 머신이 동작 변화를 확인하는 재작성을 배포하지만, 전체 검사기는 모든 것을 거부합니다. 이 결과는 동시적이고 이벤트 기반인 최종 사용자 언어에 대해 어떻게 동작 보존 보장을 제공할 수 있는지를 보여줍니다. 검사기는 최적화 도구의 주장을 신뢰하는 대신 필요한 모든 조건을 재계산하여 신뢰 기반(trusted base)을 작게 유지합니다.