研究：EVerest 充电调度代码在闰秒后提前一秒重启每日计划

EVerest 是运行充电桩的开源软件，由 Linux Foundation Energy 项目维护。

OCPP（Open Charge Point Protocol，开放充电点协议）是充电桩与管理它的网络通信所遵循的标准。在 1.6 版本中，网络可以向充电桩下发调度计划，限制其输出功率。充电桩会把多个计划合并为每一时刻的一个限值。本研究依据 OCPP 1.6 第 2 版（在新标签页中打开）的第 3.13.1 至 3.13.3 节、3.13.7 节以及 7.8 至 7.14 节展开。

研究将 EVerest 合并调度计划的代码与一个参考模型进行了对比，发现了一处差异：EVerest 会提前一秒重启每日调度计划。

这一结果基于本研究对标准所作的签署解读，出现在其最小的示例中。自调度计划首次启动以来，每经历一个闰秒，这一偏差就增加一秒。研究将其评为低严重度。

每条证据都有五种强度之一：已证明、已测试、由 Harry 判定、假定或尚未达到。「尚未达到」也涵盖尚未完成的证明。术语表对 EVerest 和 OCPP 有更多说明，并附有各自的文档链接。

本研究是《审查证据，而非代码》（在新标签页中打开）一文中论证的一个完整示例。Harry Nicholls（在新标签页中打开）指导了这项研究，并构建了其所用的工具。

该调度计划首次启动于 2016 年 9 月 14 日 11:00:00 UTC。在 2026 年 8 月 13 日 10:59:59 UTC，参考模型给出的限值为 6,543.6 W；而 EVerest 已经重启了该计划，给出的限值为 9,249.9 W。

EVerest 按已流逝的 UTC 秒数计数，其中包含闰秒。参考模型则按时钟时间重启，正如签署解读所述。

对充电的影响很小，但这一差异每次都会以相同方式出现。

EVerest issue #3323 向上游报告了这一发现。该 issue 于 2026-10-29 提交，目前仍处于开放状态。本网站不提交或更新上游 issue。查看已提交的 issue（在新标签页中打开）

Lean 检查了参考模型三条规则的证明，第四条规则的证明尚未完成。这些证明针对的是模型，而非 EVerest。

一个测试框架在每种配置 2,000 个生成用例上运行 EVerest 的调度代码和参考模型，比较二者在每次调度计划变更时刻及其前后一秒的限值。

AI agent 起草了规格说明、Lean 代码、证明尝试和测试工具。Harry 批准了对标准的解读，并决定了证据支持哪些主张。

请从那个修订版本开始，而不是 pull request，后者可能已经变动。环境搭建需要 elan（搭配 Lean v4.28.0）、Python 3、git、curl、C++ 编译器、Boost 和 fmt。

你的编译器、系统头文件和时区数据库仍需与研究中的保持一致，因此环境并未完全固定。

使用较旧调度锚点运行时应当报告失败。这些失败正是该发现的重现，并不意味着安装损坏。

每一项都给出简短回答及其证据。

证明覆盖的是参考模型；研究在生成的输入上将生产代码与之对比。

证明覆盖的是参考模型；测试在尝试过的输入上将 EVerest 与之对比。研究报告了这些结果，本网站并未重新运行它们。

EVerest 在 10:59:59 而非 11:00:00 重启每日调度计划。这出现在研究的最小示例中，基于其对标准的签署解读。

在这一秒内，EVerest 的限值为 9,249.9 W，参考模型的限值为 6,543.6 W。

原因是闰秒。自调度计划首次启动以来，每经历一个闰秒，偏差就增加一秒。

EVerest issue #3323 向上游报告了此问题，目前仍处于开放状态。查看该 issue（在新标签页中打开）

研究将其评为低严重度。在这一秒内，EVerest 的限值过高。

差异很小，但每次都会以相同方式出现。

它还会增长。自调度计划首次启动以来，每经历一个闰秒，重启就再偏移一秒。

EVerest issue #3323 向上游报告了此问题，目前仍处于开放状态。查看该 issue（在新标签页中打开）

研究将其评为低严重度。自调度计划首次启动以来，每日和每周重启会因每个闰秒偏移一秒。

输入包含一个每日默认配置，无持续时间，以及两个时段：从偏移 0 起为 9,249.9 W，从偏移 40,500 秒起为 6,543.6 W。其查询窗口从 2026 年 8 月 13 日 03:00:00 UTC 开始，持续 24 小时。

不是。这些证明针对的是参考模型，而非 EVerest 的 C++ 代码。

研究通过在生成的输入上将 EVerest 与该程序对比来测试 EVerest。

这一发现还取决于研究如何解读标准。措辞允许另一种解读，即每日调度计划按已流逝时间每 24 小时重复一次。EVerest 的做法正是如此。

这一发现取决于你如何解读标准。研究将其解读写入签署版规格说明中，因此你可以自行核对。

按照签署解读，每日调度计划在其 startSchedule 的时钟时间重启。研究指出，OCPP 1.6 规范（在新标签页中打开）的措辞也允许另一种解读。

EVerest 通过计算已流逝的 UTC 秒数来确定每次重启，其中包含闰秒。参考模型则按签署解读所述使用时钟时间。

诊断性重跑会将较旧的锚点按此后的闰秒数向前推移。此后全部 2,000 个用例均通过。

该重跑通过修改输入来确认原因，并不修复 EVerest。

有关签署解读的更多内容，见术语表。

Lean 检查的是关于模型的数学论证，并非 C++ 实现的证明。

尚未达到：添加一个不适用的较低优先级调度计划后，限值保持不变（第四条模型规则 I4）。

证明检查会列出已完成的定理。如果其中任何定理依赖于 sorryAx（Lean 用于未完成证明的占位符）或非标准公理，检查就会失败。第四条未完成的规则不计为已证明。

EVerest 是如何测试的，结果如何？

一个驱动在每种配置 2,000 个生成用例上，将 EVerest 未经修改的调度代码与参考模型进行对比运行。

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）