尽管大型语言模型（LLMs）具有令人印象深刻的适应性，但在确保其安全性、透明度和可解释性方面仍然存在挑战。鉴于其容易受到对抗性攻击的影响，LLMs 需要通过对抗性训练和护栏的不断组合来防御。然而，管理用于持续确保鲁棒性的隐性和异构知识是困难的。我们提出了一种基于形式化论证的 LLM 对抗鲁棒性保证新方法。利用本体进行形式化，我们构建了最先进的攻击和防御，便于创建可被人理解的保证案例和可被机器理解的表示。我们通过英语语言和代码翻译任务中的示例演示了其应用，并通过针对工程师、数据科学家、用户和审计员，为理论和实践提供了启示。