We study open multi-agent systems in which countably many agents may leave and join the system at run-time. We introduce a semantics, based on interpreted systems, to capture the openness of the system and show how an indexed variant of temporal-epistemic logic can be used to express specifications on them. We define the verification problem and show it is undecidable. We isolate one decidable class of open multi-agent systems and give a partial decision procedure for another one. We introduce MCMAS-OP, an open-source toolkit implementing the verification procedures. We present the results obtained using our tool on two examples.