Wavelet is an experimental compiler from a Rust-based DSL to asynchronous dataflow circuits, with its core passes formally verified in the Lean theorem prover.
Currently supported backends include the handshake dialect from LLVM CIRCT
and tagless/ordered CGRAs such as RipTide.
Read more about Wavelet in our PLDI 2026 paper:
@article{wavelet,
author = {Lin, Zhengyao and Cai, Yi and Surbatovich, Milijana},
title = {Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow},
year = {2026},
issue_date = {June 2026},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {10},
number = {PLDI},
url = {https://doi.org/10.1145/3808263},
doi = {10.1145/3808263},
journal = {Proc. ACM Program. Lang.},
month = jun,
articleno = {185},
numpages = {25}
}
Please first install the following dependencies:
Then simply run
cargo build
which will produce the CLI binary at target/debug/wavelet.
Example source programs can be found in integration-tests/tests/*/test.rs.
To compile a simple example to the handshake MLIR dialect, run:
target/debug/wavelet compile integration-tests/tests/simple/test.rs \
| target/debug/wavelet handshake
All of the Lean formalization can be found in wavelet-core/lean,
and by default, the cargo build command above does not check any proofs.
To actually verify all proofs:
cd wavelet-core/lean
lake exec cache get
lake build Thm