I haven't even used TLA+ yet and now it's got derivatives... My understanding is: TLA+ but like C, functional, and typed.