В работе рассмотрена архитектура транслятора из Scheme в JavaScript, которая облегчает его формальную верификацию. Систематизируются общепринятые практики проектирования оперирующего над исходным кодом в качестве данных программного обеспечения, используемые для проведения верификации алгоритмов. На примере более узкой задачи трансляции из Scheme в JavaScript рассмотрены конкретные проблемы, связанные с трудностью верификации транслятора, составленного эвристически, а также их решения. На основе проведённого исследования представляется возможным выделить принципы построения широкого класса верифицированных утилит для работы с исходным кодом программ.