I'm not really seeing what this system offers over other tools. Haskell with logict and smallcheck, say. Or to go in another direction, Agda with McBride-style indexed monads to express Hoare logic. Maybe typical C programmers aren't familiar with these ideas, but others are. As for a language designer who knows liveness and fairness? Simon Peyton Jones seems a perfect pick. He's written numerous papers about both.
How one can compare logict to TLA+ is beyond my imagination. What's next, Pi calculus? I wonder if the author of this comment wanted to really show alternatives for formal specification or just brag? Have you literally tried it? Looked at the examples (for example specification of 3 phase commit)? Have you seen the expressiveness of it, the temporal formulas you can write with it?
