Sweeet! The beginnings of a formal model of the Zcash Crosslink protocol in TLA* by 0xarbitrage!

https://github.com/oxarbitrage/crosslink2

This is the kind of thing that can provide stronger safety of software than the current state of the art of safety in software! 🎉