Abstract: Linear Temporal Logic (LTL) is a formal language that can be used to specify robot behaviors and goal states. We extend LTL to enable the specification of complex cooperative behaviors in a large multi-agent system (MAS). The extended language, TeamingLTL, models features commonly present in MAS such as partial observability and cooperation between agents. This enables a user to specify behaviors or goals while deferring the realization of those states to a separate, automated task planning and allocation system. We show how to specify the behavior of a MAS using TeamingLTL and use this formulation in program verification and the creation of correct-by-design controllers.