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).

[1]: https://en.wikipedia.org/wiki/Three_Laws_of_Robotics

[2]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...