>We need some form of behavioral verification/auditing with guarantees that any input is proven to not produce any number of specific forbidden outputs.
You want the impossible. The domain LLMs operate on is inherently ambiguous, thus you can't formally specify your outputs correctly or formally prove them being correct. (and yes, this doesn't have anything to do with determinism either, it's about correctness)
You just have to accept the ambiguousness, and bring errors or deviation to the rates low enough to trust the system. That's inherent to any intelligence, machine or human.