This talk will be an informal presentation of work in progress on an approach to specifying, verifying and executing populations of agents. I shall present some (very initial) ideas on a language to specify temporal properties of an agent and how this language can be seamlessly linked to logic programs. A set of design features of agents have been formally represented in this temporal language - such features guide the execution of the agent and are useful when proving properties (via a model-checker).