How can we provide guarantees of behaviour for autonomous systems? In this talk I will explain how autonomous systems can be programmed in ways that make them amenable to formal verification. I will discuss how cognitive agent programming can be used to provide a transparent and verifiable decision-making core and show how properties of the system can then be checked – including properties related to ethical behaviour.