We stress the need for formal object modeling languages for the design of large and complex sofware artefacts. We study one such language, Daniel Jackson's Alloy (MIT) in detail. In presenting Alloy, we will discuss the aspects and trade-offs of its design decisions. We then use Alloy to formally model current software designs in the realm of mobility, security, and (possibly) wireless computing. Time permitting we may compare Alloy to two other modelling languages: UML and Z.