데이터플로우 (Dataflow) 아키텍처는 전력 효율성과 성능 사이의 균형 덕분에 다시금 관심을 받고 있습니다. (공간적 (spatial)) 데이터플로우 아키텍처에서 프로그램은 비동기 채널을 통해 통신하는, 완전히 분산되고 동적으로 스케줄링되는 데이터플로우 연산자 (operators) 세트로 표현되며, 이는 데이터 지역성 (data locality)과 병렬성 (parallelism)을 크게 향상시킵니다. 그러나 파이프라이닝 (pipelining)을 가능하게 하면서 결정론 (determinacy)을 유지하기 위해 데이터플로우 아키텍처로 컴파일하는 과정은 여전히 오류가 발생하기 쉬운 프로세스로 남아 있습니다. 결정론이란 데이터플로우 프로그램의 결과가 결정론적이며 연산자 실행 스케줄과 무관함을 의미하며, 파이프라이닝은 루프 반복 (loop iterations) 간의 병렬성을 가능하게 하는 공간적 데이터플로우에서의 중요한 최적화 기법입니다. 본 연구에서는 비동기 데이터플로우를 위한 컴파일러를 형식적으로 검증 (formally verify)하려는 최초의 시도인 Wavelet을 제시합니다. 우리는 이 목표를 달성하기 위해 다양한 기술을 혼합하여 사용합니다. 우리의 프론트엔드 (frontend)는 충돌하는 메모리 접근을 동기화하고 파이프라이닝을 가능하게 하는 펜스 (fences)를 포함한 새로운 역량 타입 시스템 (capability type system)을 사용합니다. 그런 다음, 타입 체커 (type checker)로부터 정교화된 프로그램 (elaborated programs)을 데이터플로우 그래프 (dataflow graphs)로 변환하는 우리 컴파일러의 두 가지 핵심 패스 (passes)에 대한 Lean 형식화 (formalization)를 검증하여, 전방 시뮬레이션 (forward simulation) 및 결정론에 관한 중요한 속성들을 증명합니다. 특히, 우리의 형식화는 프론트엔드 타입 시스템의 건전성 (soundness) 보장을 의미론적으로 전파하여, 시뮬레이션과 결정론 증명 사이의 모듈성 (modularity)을 보장합니다. 평가를 통해, 우리는 Wavelet에 의해 컴파일된 데이터플로우 그래프가 RipTide 공간적 데이터플로우 아키텍처를 위한 검증되지 않은 최적화 컴파일러가 생성한 그래프와 유사한 크기를 가짐을 보여줍니다.