  In this paper I discuss how can lightweight formal methods be used to specify
and verify software with complex configurations (for example, distributed
protocols that work on specific network configurations). More specifically, I
briefly present two popular formal methods - TLA+ and Alloy - and discuss the
pros and cons of both in this particular context.
