Can't speak for crypto projects. I used it to verify some incredibly complicated security fixes I made; you can find my models here: https://gitlab.com/xen-pr

Can't speak for crypto projects. I used it to verify some incredibly complicated security fixes I made; you can find my models here: https://gitlab.com/xen-project/people/gdunlap/tla https://gitlab.com/xen-project/people/gdunlap/tla And the security advisory here: https://xenbits.xenproject.org/xsa/advisory-299.txt https://xenbits.xenproject.org/xsa/advisory-299.txt A description of the issue, sketches of the attacks, and the fixes can be found in the individual patches. TLA+ was obviously very powerful, but it is incredibly quirky in so many ways. The scoping of variable in PlusCal is really strange: it looks like you can make variables with local scope, but then they turn out to have global scope. You have to fight the tool to be able to use it outside of its special-purpose IDE or make it something that could be sensibly collaborated on over git. (See some of the makefile runes in the above repo to see the kind of thing I did.) Getting it to do parallel searches was difficult.