TL;DR: A lisp and peano arithmetic implemented with rust types and traits. Reverse engineer some, lift to z3, pray.
[Full writeup](https://org.anize.rs/dicectf-2022/rev/typed)