I'm reminded of Asimov'sThree Laws of Robotics [1]. It's a nice idea but it immediately comes up against Godel's incompleteness theorems [2]. Formal proofs have limits in software but what robots (or, now, LLMs) are doing is so general that I think there's no way to guarantee limits to what the LLM can do. In short, it's a security nightmare (like you say).