The project examined formal verification methods for autonomous systems. Our specific contribution was designing an architecture for robots that evaluated possible actions against a code of ethics and selected the most appropriate according to that code. The architecture implementation was designed in such a way as to be able to be formally verified, as well as experimentally validated.