The paper considers scenarios in which autonomous robots are expected to interact in accordance with certain rules of law or ethics, or any other set of formally expressed constraints. Can an 'observer' actually tell from inspecting a robot's program and interactions whether the robot will always follow the rules it is said to obey in its interactions with other robots? Under reasonable assumptions about robot programming and about an observer's capabilities, no (deterministic) module, algorithmic or otherwise, will enable an observer to do so for all robots in any feasible way. It means that, in general, guarantees about the legal or ethical behaviour of autonomous robots are not verifiable at runtime by any means, given the assumptions made. The result holds for all 'non-trivial' robot interaction properties. Non-triviality also shows what must be avoided when designing artefacts whose behavioural properties have to be verifiable at runtime and that, if ethical or legal properties of robot software are to be verified in practice, one should either eliminate the need of knowing non-trivial properties or limit the extent of the programs that are allowed. The result gives theoretical evidence that formal verification of these properties will be hard, if not impossible, in general, confirming at least partially the claim that full formal verification is likely unrealistic.
Either eliminate the need of knowing non-trivial properties, or limit the extent of the programs that are allowed, as for ordinary programs, so that ethical or legal properties of robot software can be verified in practice.