Both can deal with time, but Alloy is a high level language to describe structures, their relationships, constraints and feels like writing SQL schemas and prop

Both can deal with time, but Alloy is a high level language to describe structures, their relationships, constraints and feels like writing SQL schemas and property tests. It is easy to use. With Alloy, you can very quickly iterate over software designs. TLA is more heavy weight and geared toward verifying concurrent systems, including algorithms and such. It is much harder to learn. With TLA, you can verify concurrent systems and algorithms.