即使证明经过自动检查，人们仍需要知道：检查程序本身会不会接受错误对象。10 月 15 日，Leonardo de Moura 介绍 Lean v4.35.0 随工具链提供的独立检查路径：lake check 导出项目的声明，让去掉大量外围功能的官方 leanchecker 在沙箱中重新检查；使用更严格的模式，还能调用 nanoda、lean4lean、con-leche、con-ron 等不同实现。这样做把复杂的交互、编译和证明生成流程，与最终接受证明的检查工作进一步分开。
其中 con-leche 用 Lean 实现，并在集合论模型假设下证明其接受对象的一致性；con-ron 是 Rust 实现，借助 Aeneas 对检查算法建立对应的精化证明。项目同时使用不同语言和工具链，降低所有实现撞上同一类编译器或运行时问题的机会。作者披露 AI 在实现和证明过程中发挥了很大作用，同时强调 Joachim Breitner 的持续指导。这里有两层不能混淆：模型参与写出检查器，不意味着模型本身成了最终裁判；形式化证明也仍有其公理、模型和执行环境的信任前提。