It is a modeling language based on relations and constraints. It is very friendly and feels like writing SQL schemas or classes. Given a model and its constraints Alloy can use a SAT solver to find valid instances. This is used to check model properties.

It can be used to model not only algorithms but principally concepts.

I always use Alloy before starting a new design.