AboutA study of EVerest, open-source software for electric-vehicle chargers, and how it follows OCPP.
is open-source software that runs a charging station. The Linux Foundation Energy project maintains it.
, the Open Charge Point Protocol, is the standard a charger uses to talk to the network that manages it. In version 1.6, the network can send a charger schedules that cap how much power it gives. The charger combines those schedules into one limit for each moment. The study works from OCPP 1.6 edition 2 (opens in a new tab), sections 3.13.1 to 3.13.3, 3.13.7 and 7.8 to 7.14.
The study compared EVerest’s code for combining schedules with a . It found one difference. EVerest restarts a daily schedule one second early.
That result uses the study’s of the standard, in its smallest example. The gap grows by one second for each since the schedule first started. The study rates it low severity.
Each piece of evidence has one of five strengths: Proved, Tested, Decided by Harry, Assumed or Not yet reached. Not yet reached also covers a proof that is not finished yet. The glossary says more about EVerest and OCPP, with links to their own documentation.
The study is a worked example of the argument in Review Evidence, Not Code (opens in a new tab). Harry Nicholls (opens in a new tab) directed it and built the tool it uses.
FindingA daily schedule should restart at 11:00:00; in the study’s smallest example, EVerest restarts it at 10:59:59, a leap second early.
The schedule first started at 11:00:00 UTC on 14 September 2016. At 10:59:59 UTC on 13 August 2026 the reference model gives a limit of 6,543.6 W. EVerest has already restarted the schedule and gives 9,249.9 W.
EVerest counts elapsed UTC seconds, and those include leap seconds. The reference model restarts at the clock time, as the signed reading says.
The effect on charging is small. The difference happens the same way every time.
EVerest issue #3323 reports the finding upstream. It was filed on 2026-10-29 and is open. This website does not file or update upstream issues. View filed issue (opens in a new tab)
StudyA reference model written in Lean states the charging rules, and the study compares EVerest’s code with it.
checks proofs of three of the ’s rules. The proof of a fourth is unfinished. The proofs are about the model, not about EVerest.
A test harness runs EVerest’s scheduling code and the reference model on 2,000 generated cases per configuration. It compares their limits at each moment a schedule changes, and one second either side.
AI agents drafted the specifications, Lean code, proof attempts and test tooling. Harry approved the readings of the standard and decided which claims the evidence supports.
RepeatThe source and downloaded inputs are pinned to one study revision, 7d05c4e6.
Start from that revision, not the pull request, which may have moved on. Setup needs elan with Lean v4.28.0, Python 3, git, curl, a C++ compiler, Boost and fmt.
Your compiler, system headers and timezone database still need to match the study’s, so the environment is not fully pinned.
The run with older schedule anchors should report failures. Those failures are the finding, reproduced. They do not mean the install is broken.
Questions
Each shows a short answer and the evidence for it.
Evidence strength
- Proved
- Tested
- Decided by Harry
- Assumed
- Not yet reached
Evidence
Overview
The evidence at a glance
.
Proofs cover the reference model. The study compares production code with it on generated inputs.
| What was checked | How it was checked | Strength | Result and boundary |
|---|---|---|---|
| Three rules of the reference model | Lean checks the proofs | Proved | About the Lean model, not a proof about EVerest’s code. |
| Schedules anchored in 2017–2025 | 2,000 generated cases | Tested | All 2,000 pass. At the 57,304 moments where the model gives a limit, the two agree within tolerance. At the other 10,226 moments, neither gives a limit. |
| Schedules anchored in 2010–2016 | 2,000 generated cases | Tested | 835 pass, 92 warn and 1,073 fail, as the study reported. The report also counts 1,081 moments where only EVerest gives a limit; see the caveat on how those are classified. |
| A fourth model rule | Stated without a completed proof | Not yet reached | No proof claimed. |
Proofs cover the reference model. Tests compare EVerest with it on the inputs tried. The study reports these results; this website did not rerun them.
Finding
What went wrong?
EVerest restarts a daily schedule at 10:59:59 instead of 11:00:00. That is in the study’s smallest example, under its signed reading of the standard.
For that one second, EVerest’s limit is 9,249.9 W. The reference model’s is 6,543.6 W.
The cause is leap seconds. The gap grows by one second for each leap second since the schedule first started.
EVerest issue #3323 reports this upstream. It is open. View the issue (opens in a new tab)
Does a one-second error matter?
The study rates it low severity. For one second, EVerest’s limit is too high.
The difference is small, but it happens the same way every time.
It also grows. Restarts drift one more second for each leap second since the schedule first started.
EVerest issue #3323 reports this upstream. It is open. View the issue (opens in a new tab)
One second before 11:00
.
The study rates this low severity. Daily and weekly restarts drift by one second per since the schedule first started.
- The reference model
- 6,543.6 WThe second period still applies. Restart is at 11:00:00 UTC.
- EVerest at
dd696165 - 9,249.9 WIt has already restarted, one second early, so the limit is too high.
The input has one daily default profile, no duration, and two periods: 9,249.9 W from offset 0, then 6,543.6 W from offset 40,500 seconds. Its query window begins at 03:00:00 UTC on 13 August 2026 and lasts 24 hours.
Is this a proof that EVerest is wrong?
No. The proofs are about the reference model, not EVerest’s C++ code.
The study tested EVerest by comparing it with that program on generated inputs.
The finding also depends on how the study reads the standard. The wording allows another reading, where a daily schedule repeats every 24 hours of elapsed time. That is what EVerest does.
Why it happens
.
The finding depends on how you read the standard. The study writes its reading down in the signed spec, so you can check it.
Under the signed reading, a daily schedule restarts at the clock time in its startSchedule. The study notes that the wording of the OCPP 1.6 specification (opens in a new tab) allows another reading too.
EVerest works out each restart by counting elapsed UTC seconds, and those include leap seconds. The reference model uses clock time, as the signed reading says.
A diagnostic rerun shifts older forward by the leap seconds since then. All 2,000 cases then pass.
That rerun changes the inputs to confirm the cause. It does not fix EVerest.
Proof
What is proved
.
checks mathematical arguments about the model. This is not a proof of the C++ implementation.
- The combined limit is never above the charger-wide limit.
- It is never above the applicable transaction limit.
- While a transaction’s own schedule applies, changing default schedules does not change the limit.
Not yet reached: Adding a lower-priority schedule that does not apply leaves the limit unchanged (the fourth model rule, I4).
The proof check lists the completed theorems. It fails if any of them depends on sorryAx, the placeholder Lean uses for an unfinished proof, or on a non-standard axiom. The fourth, unfinished rule does not count as proved.
Tests
How was EVerest tested, and what came back?
A driver runs EVerest’s unmodified scheduling code against the reference model on 2,000 generated cases per configuration.
Schedules that first started in 2010–2016 give 835 passes, 92 warnings and 1,073 failures, as the study reported. Those failures are the finding.
Schedules that first started in 2017–2025 all pass.
A pass means the case met the study’s comparison rule, not that the limits agree exactly.
In 55 of those passing cases, the reference model gives no limit at any moment checked. There was nothing for EVerest to agree with, so those cases pass without testing anything.
What the tests report
.
A passing case met the study’s comparison rule. That alone does not mean the limits agree exactly. These are the study’s reported results, and this website did not rerun them.
| Configuration | Pass | Warn | Fail |
|---|---|---|---|
| Anchors 2017–2025 | 2,000 | 0 | 0 |
| Anchors 2010–2016 | 835 | 92 | 1,073 |
| Older anchors, shifted by leap seconds | 2,000 | 0 | 0 |
| Mutation self-test (seed 1) | 181 | 34 | 85 |
Seed 20261024; 2,000 cases per main configuration. The mutation self-test uses 300 cases and seed 1. Exact means within 0.05 of the profile’s unit (A or W).
The pinned report contradicts itself about extra limits, where EVerest gives a limit and the model gives none. Its updated header for the conformance rule (Q4) calls these moments warnings. An older note it kept says they were left unclassified. Its counters record 1,081 of them in the older run. The totals shown here are the report’s own published totals. A pass does not mean the limits agree exactly.
The mutation self-test changes how the code picks between stacked schedules, on purpose, to check that the harness notices. Its failures are not another defect in EVerest.
Agreement at each instant
.
The harness compares each case at the moments where schedules change, and one second either side.
| Counter | 2017–2025 anchors | 2010–2016 anchors |
|---|---|---|
| Instants compared | 67,530 | 78,263 |
| Model gives a limit | 57,304 | 66,541 |
| EVerest agrees within | 57,304 | 56,902 |
| EVerest below the model | 0 | 4,331 |
| EVerest above, or missing a required limit | 0 | 5,308 |
| EVerest gives a limit; model gives none | 0 | 1,081 |
| Neither gives a limit | 10,226 | 10,641 |
| Cases with no model limit anywhere | 55 | 64 |
In 55 recent-anchor cases, the model gives no limit at any moment checked. There is nothing for EVerest to agree with, so those cases pass without testing anything. They are . The finding does not rest on them. It comes from the older-anchor failures.
Assumptions
What does the result depend on?
It depends on Lean and its standard axioms.
The reading of OCPP 1.6 that Harry approved has to be right, and the Lean model has to match it.
The compiler, the test harness and the driver, with its installation glue and two shim headers, have to work correctly.
The timezone database has to list exactly the three leap seconds since 2010.
What the result depends on
.
The result holds only if everything in the works correctly.
- Lean v4.28.0 and its standard axioms (propext, Classical.choice and Quot.sound), for the completed proofs.
- The reading of OCPP 1.6 edition 2 that Harry approved, and the Lean model matching that reading.
- The C++ compiler, the driver with its copied installation glue and two shim headers, the Python harness, the JSON adapter and the model runner.
- The operating system’s timezone database, which the driver reads. Its leap-second table must list exactly the three leap seconds since 2010 (2012-06-30, 2015-06-30 and 2016-12-31).
The driver compiles EVerest’s scheduling code unchanged. It adds its own installation glue and two shim headers, and the comparison trusts those too.
Limits
What wasn’t checked?
The generated inputs have limits. Each case has at most 2 charger-wide, 3 default and 2 transaction profiles, with up to 4 periods each. Offsets come in 15-minute steps, windows are 24 or 48 hours in 2026, and everything is on connector 1.
No case has default profiles on connectors 0 and 1 together.
The study has not yet reached relative profiles, phases, unit conversion, the connector-0 aggregate, offline behavior, transaction IDs or OCPP 2.x.
One of the four model rules has no finished proof.
Where the result stops
.
Agreement on these inputs says nothing about the rest of OCPP. Each behavior not yet reached needs either a bigger model or a stated assumption.
Each case has at most 2 charger-wide, 3 default and 2 transaction profiles, with up to 4 periods per profile. Offsets come in 15-minute steps, and windows are 24 or 48 hours in 2026, all on connector 1. The generator makes absolute, daily and weekly schedules. Each case checks the moments where either program’s limit changes, and one second either side.
No case has default profiles on connectors 0 and 1 together, because the signed spec leaves open how they interact. The standard’s wording on repeating schedules also allows a second reading. Once a leap second falls between a schedule’s start and now, “every 24 hours, at the same time” can mean 24 hours of elapsed seconds or the same clock time. The study records this for the Open Charge Alliance (OCA) as note N4.
| Behavior | Blocking property | Open modeling question |
|---|---|---|
| Relative profiles | No transaction start time in the model | How should transaction-relative time enter the model? |
| Phases and minimum charging rate | One scalar limit and no phase count | How should phase-dependent limits be represented? |
| Conversion between amps and watts | No voltage or phase inputs | What assumptions justify conversion between units? |
| Connector-0 aggregate | No allocation state across connectors | How should the station-wide sum be constrained? |
| Offline behavior | No connectivity state | How should connectivity change profile selection? |
| Transaction ID matching | No transaction ID field or active-transaction input | How should transaction identity constrain applicability? |
| OCPP 2.x | Different profile structure and separate production code | Which rules and model changes are needed for OCPP 2.x? |
Repeat
Can I run it myself?
Yes. Check out the pinned study revision and build the driver.
Run the proof check, then run the test harness three times.
The run with older anchors should report failures. Those failures are the finding, reproduced.
Repeat the run
.
Start from the pinned study revision, not the pull request, which may have moved on. Setup downloads dependencies.
Install elan with leanprover/lean4:v4.28.0, Python 3, git and curl. The recorded driver build used:
- Apple clang 21.0.0 with C++17, on macOS arm64
- Boost 1.92.0, headers in /opt/homebrew/include
- fmt 12.2.0, header-only, in /opt/homebrew/include
See the driver prerequisites (opens in a new tab) before running.
Source and downloaded inputs are pinned. Your compiler, system headers and timezone database still need to match the study’s, so the environment is not fully pinned. The leap-second table must list the three leap seconds since 2010. The driver build checks downloaded sources against SHA-256 hashes in the pinned build script (opens in a new tab).
git clone https://github.com/nicholls-inc/crosscheck crosscheck-everest-study
cd crosscheck-everest-study
git checkout --detach 7d05c4e62284b4101e8f23722ee3b6111e5ca0e9
formal-verification/tests/ocpp16_composite/everest_driver/build.sh
formal-verification/lean/CrosscheckModel/check_ocpp16_composite.sh
python3 formal-verification/tests/ocpp16_composite/drt_harness.py --count 2000 --seed 20261024
python3 formal-verification/tests/ocpp16_composite/drt_harness.py --count 2000 --seed 20261024 --old-anchors
python3 formal-verification/tests/ocpp16_composite/drt_harness.py --count 2000 --seed 20261024 --old-anchors --leap-correct The run with older anchors should report failures. A nonzero exit there reproduces the finding; it does not mean the install failed. --leap-correct shifts the input anchors to confirm the cause, and does not fix EVerest. Each run writes drt_report_latest.md. Do not overwrite the pinned historical report.
Inspect the sources
.
Every source below names the same study revision. The live pull request (opens in a new tab) may have moved on since.
Study snapshot: 7d05c4e62284b4101e8f23722ee3b6111e5ca0e9. EVerest source: dd696165 (opens in a new tab).
- Written rules (opens in a new tab)
- Model and proofs (opens in a new tab)
- Correspondence review (opens in a new tab)
- Test report (opens in a new tab)
- Driver and shims (opens in a new tab)
- Build inputs (opens in a new tab)
- Test harness (opens in a new tab)
- Proof check (opens in a new tab)
Work in progress. These are the study’s reported results, and this website did not rerun them. Main runs dated 2026-10-24; comparison counters measured 2026-10-27.
This page summarizes evidence from the linked study. It is not an evidence-record/1 file, an automatic attestation, a new run of the experiment, or a fresh check of the proofs.
People
What did Harry decide, and what did the AI do?
Harry directed the study, approved the readings of the charging rules and decided which claims the evidence supports.
AI agents drafted the specifications, Lean code, proof attempts and test tooling.
An AI review searched for mismatches. Its verdicts do not count as evidence.
Who did what
.
AI drafted the work. Only deterministic checks and Harry’s recorded decisions count as evidence.
I built Crosscheck to make claims about AI-written code inspectable. For this study, I used its AI-assisted workflow to model OCPP 1.6 charging schedules and compare the model with EVerest’s scheduling code.
I directed the study, approved the readings of the charging rules, reviewed the correspondence findings and decided which claims the evidence supports. The signed spec and my recorded decisions show that judgment.
- AI assistance
- AI agents drafted the specifications, Lean code, proof attempts and test tooling. An AI correspondence review searched for mismatches. Harry reviewed its verdicts, and they do not count as evidence.
- What the checks establish
- Lean checks the completed proofs about the model. A test harness sends generated inputs to EVerest’s unchanged scheduling code, through a driver, and to the model, then compares their answers. The study still trusts the compiler, its reading of the standard, the driver and the harness.
- The reported result
- The study reports a low-severity drift in repeating schedules, caused by leap seconds. It shows one concrete example and diagnostic reruns. It does not show a deployed fix, full OCPP conformance or a proof about the production code.
The signed interpretation decisions (opens in a new tab) and correspondence review with Harry’s decisions (opens in a new tab) record the human judgments behind this account.
Where Harry decided
.
An AI searched for likely problems. Its verdict is not evidence. Harry’s recorded decisions are.
- Harry approved two readings of the standard. A profile applies only while its schedule covers the moment (A1). A transaction profile overrules the default profiles only while its own schedule covers the moment (A2). Harry also reclassified two findings from the AI correspondence review as abstractions rather than approximations.
- On 2026-10-27, Harry confirmed adding back a missing condition to the rule for when a schedule covers a moment (D4). The condition is s ≤ t, which says the moment t cannot come before the schedule’s start s.
- The conformance rule (Q4) says EVerest’s limit conforms if it is at or below the model’s, or if the model gives no limit. So a lower limit counts as conforming. Harry chose to have the report warn about it anyway, because a lower limit means lost charging. The report keeps the classification caveat recorded here.
Why the study is built this way
.
Each choice is listed with what it leaves unchecked.
- Separate the model from the production implementation
- A reference model in Lean lets the study state and prove rules about the model, then compare its answers with EVerest’s existing C++ code. A proof about the model does not show that the production code behaves the same way.
- Check the moments where schedules change
- The harness compares the moments where either program’s limit changes, and one second either side. That makes a one-second timing difference visible. The generator still limits profiles, periods and time windows. Agreement says nothing about other inputs.
- Record interpretation decisions before judging differences
- Harry settled the ambiguities in the signed spec, then reviewed the correspondence findings against those decisions. A difference that comes from a disputed reading of the standard has to stay separate from a real defect in the code.
- Publish the limits beside the result
- The study keeps the unfinished fourth proof, the trusted dependencies and the report’s inconsistency in plain view, with pinned inputs for replay. Shifting the inputs by the leap seconds is a diagnostic experiment. It does not fix EVerest.