形式化验证

使用 TLA+ 或 Lean 4 对目标函数进行形式化验证，检查不变量并复现反例。该插件由 /engineer.harden 并行调度，不自动创建 PR。