the point I like Alloy is that it allows you to express something like "forall function f such that f is well-define ...", very cool.

I barely know anything about TLA+ though.