Energy · Research 004 · distributed wind
Wind power that proves its decisions. Assurance for every turbine’s supervisor.
A distributed wind system decides all day: charge, export, curtail, protect the critical load. We build the component that checks every one of those decisions against the turbine’s real limits before it is acted on, and hands back a certificate anyone can re-check.
Proof network · 149 modules · 818 checked dependencies
Agda 2.8.0 · --safe · --without-K
Target 01 · Curtailment, bounded
curtailed ≥ supply − headroom
Wind is curtailed only for a proved reason; a full battery is never counted as a sink.
Proved · for every state
21 of 48 phases closed · allocation in progress · proposed to NLR’s 2026 Competitiveness Improvement Project with Uprise Energy
What you can do here
Test a forecast
Move a wind-speed range across the turbine’s curve and watch the proved envelope beside the reading that breaks at cut-out.
in your browser · exactRead the statements
24 theorems in plain words, as mathematics, with module, line and source hash.
proved · Agda kernelWalk the system
Every module and every checked dependency, by family, and the graph to download.
proved · Agda kernelSee the grid outcomes
NLR’s EVI-DiST reproduced exactly on public feeders, beside the proved ledger.
simulated · public dataRun your turbine’s scenarios
Bring a power curve, storage and loads; we check your supervisor’s decisions against them.
partner access
01 · For turbine makers
More of your turbine’s energy, used safely, with the evidence attached.
Distributed wind is sold on reliability. Every curtailment, export and reserve decision is a place where a controller can be wrong in a way no one sees until a battery overcharges or a limit trips. The component makes each decision provably admissible and leaves an audit trail a utility, insurer or certification body can read.
A full battery is never treated as a sink
The checker refuses any dispatch that counts on storage that cannot absorb. Curtailment is bounded below by what the loads and the battery genuinely cannot take, so wind is never curtailed for an unproved reason and never sent where it cannot go.
The theorem: curtail-lower-bound ↓The power curve, read correctly across an interval
A forecast is a range of wind speeds, not a number. Reading the power curve only at the range’s two ends is wrong near cut-out: a storm interval’s lower end gives full power while its upper end gives none. The toolkit computes the true envelope, and proves it is both sound and tight.
The theorem: gen-sound ↓Absorption within the limit, from every state
Every modelled state of the wind, storage and load system is either within the absorption limit already, or one absorb step brings it there. Not on the cases we tried: for all of them.
The theorem: modelledAbsorptionWithinLimit ↓Your protection stays yours
The component is advisory and sits beside the controller, never in place of it. The OEM keeps protection, interlocks and deployment authority; the checker only decides which proposed actions are admissible, and records why.
Evidence a certification body can read
Every requirement links to a proof, test, analysis or stated limitation, with the edition of each standard recorded. A qualification roadmap maps ANSI/ACP 101-1, IEC 61400-2 and the applicable UL requirements to the future integration, so the next engineering step is clear before it is taken.
Reusable across turbines, without borrowing safety
The same typed interface serves other distributed-wind architectures, cutting duplicated schema validation, negative tests and evidence work. Each new turbine brings its own model contract and limits; nothing is transferred by assumption.
02 · The power curve, under uncertainty
Near cut-out, the obvious arithmetic is wrong.
A supervisor plans on a forecast, and a forecast is a range. Reading the curve at the range’s two ends looks reasonable and fails exactly in a storm, where one end gives full power and the other gives none. Try it: this is the toolkit’s own curve, evaluated exactly in your browser.
A forecast is a range of wind speeds. Choose one:
Generation the supervisor can count on
0 kW – 12 kW
the proved envelope: it contains every outcome, and its top is reached
Reading only the ends
12 kW – 0 kW
Wrong: it promises at least 12 kW, but a wind inside this range shuts the turbine down. A plan built on it would fall short exactly when it matters.
03 · How it works
One untrusted proposer. One independent checker.
The design separates finding a good action from deciding that it is safe. Anything may propose; only a small, proved checker admits, and every admission carries a certificate an open verifier re-checks.
01
Wind · storage · loads · EV
turbine, battery, critical loads, chargers
Chora.Wind* · GEC.Model.*
02
Typed snapshot
every reading an interval, with units, sign, time and epoch
GEC.Verify.Format · HomeFormat
03
Proposer
deterministic policy, forecast or AI model
GEC.Home.Allocate* · Fill
04
Independent checker
proved in safe Agda, extracted to native code
GEC.Verify.Proposal · Cert
05
Admitted, with a certificate
or refused, with its named reason and a safe fallback
GEC.Home.Protect* · Recover*
06
Open verifier & evidence ledger
anyone re-checks; evidence typed and invalidated on change
GEC.Verify.Evidence · Profile · Log
Demonstrator A · the 12-kW reference
A wind, storage and critical-load system anchored to Uprise Energy’s 12-kW Mobile Power Station, with high wind, a full battery and no sink among its named scenarios.
Demonstrator B · a public feeder
An EVI-DiST distribution feeder with wind, storage, EV charging and other demand, on public SMART-DS data, so anyone can reproduce it.
The neighbourhood coordinator
Above the homes, a coordinator shares a transformer between them. It is proved and checked with the rest; its engine stays with us, and its every decision is re-checkable with the open verifier.
04 · Safe AI integration
Let the AI propose. Let the mathematics decide.
Forecasting and optimisation models can find value a fixed rule leaves on the table. The architecture keeps that value and removes the risk: an AI may estimate generation and demand or propose a dispatch, but it cannot change the admissibility rules, the evidence format or the protection envelope.
In practice
- A proposal is checked against every world consistent with the measured intervals, not one guess.
- The checker is exact: no refusal on a corner case is a false alarm, and forced refusals are named.
- A universal safe fallback passes whenever any proposal could; if it fails, the system says the envelope itself must change.
- A deterministic proposer and the AI path share one interface, so their outcomes are compared on identical inputs.
05 · Cyber-resilience
Stale, replayed or forged inputs cannot buy authority.
Many attacks on control systems do not break cryptography; they replay an old message, reorder readings or exploit the gap between a command received and a command executed. The model checks these by construction.
In practice
- Messages from an obsolete configuration epoch cannot authorise a new action.
- Duplicate requests are idempotent; a reservation persists until its release event.
- An acknowledgement is not treated as execution: caps stay in flight until the shed is confirmed.
- Inconsistent units or power signs, out-of-range values and missing readings yield an explicit refusal, never a silent guess.
06 · On NLR’s EVI-DiST
We ran the laboratory’s own tool, and proved what it does.
EVI-DiST co-simulates EV charging with the distribution grid. We integrated it unmodified, reproduced its results exactly, and turned what it guarantees, and where it stops, into theorems.
| Region | EVI-DiST smart policies | Sound ledger budget |
|---|---|---|
| GSO | 54.8–54.9% | 97.4–97.5% |
| AUS | 58.4–58.5% | 97.4% |
| SFO | 50.2–51.5% | 98.4% |
Public NREL SMART-DS feeders (Greensboro, Austin, San Francisco), EVI-DiST pinned at a released revision. The ledger column is the ceiling a sound budget reaches under the same policies: the bound the controller rounds are built to approach.
Integrated, unmodified, reproduced exactly
EVI-DiST was pinned at a released revision and run as published on public NREL SMART-DS feeders. A gridless model written from its own allocation code reproduces every EV’s delivered energy to 10⁻¹¹ kWh across nine smart runs, and every transformer’s loading exactly.
The smart policies are open-loop
They subtract a fixed published base load from each transformer’s rating and receive no feedback from the grid; a closed-loop variant, a different ordering and a different floor each fail to reproduce the runs.
The obvious fix overloads; the proved one does not
Taking the measured load naively delivers all the energy but overloads 6–63 transformers, through a base-load ramp landing on an allocation made a step earlier. Under compliance latency 1–3 the proved ledger has zero model overloads, against 6–64 for the obvious rule, and the only physical residual left is line losses, at most 0.432 kVA.
A season the reference tool could not simulate
Its smart policies silently starve on any day but 1 January; season-faithful runs of six world-and-weather scenarios, from a cold snap to a heat wave, run 3.5–7.4× faster, value for value.
07 · Better science, better models
Sensor data you can trust makes predictive models you can trust.
Every reading enters as an interval with its source, time and epoch. Evidence keeps its class: a formal proof, a measurement and a third-party fact can never be promoted into one another, which is a theorem of the shipped checker. When a model weight, calibration or standard edition changes, everything that depended on it is invalidated until it is re-checked.
In practice
- Training and forecasting data carry their provenance, so a model is only as confident as its inputs allow.
- Predictive models are scored against the same certified record the controller uses.
- The same discipline underpins our verifiable sensor data research at the apiary.
08 · Interpretability by construction
Every verdict explains itself, in mathematics.
Because the system is written in a formal language, its decisions are not opaque outputs to be explained afterwards. Each admitted or refused action carries the requirement it was checked against, the assumptions it relied on and a certificate an independent verifier re-checks. The statements themselves render as mathematics a reviewer can read.
In practice
- Open verifier: anyone can re-check a decision without trusting the code that made it.
- Requirement profiles are data, checked by one generic, proved verifier.
- Semantic integration: the same formal objects connect protocols, devices and models, so meaning survives each interface.
09 · The proofs
24 statements, each for every case.
Open any one. Each is a theorem checked by the Agda proof kernel in safe mode, typeset as mathematics by our certified renderer wherever its certificate verifies, with its module, its dependencies and the hash of the source it came from.
24 published statements · 12 typeset from certificates verified for this page; the other 12 shown verbatim from source, each with the renderer’s reason
Wind & storage
The turbine’s power curve, absorption and curtailment.
01pc-boundThe modelled turbine never produces more than its rated power, at any wind speed.proved · shown verbatim
pc-bound :
(v : Nat) → WM.powerCurve v ≤ WM.pratedShown verbatim: the renderer does not yet read this module’s qualified imports (error:no_sir_line). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.ChoraBridge · line 169
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 7 modules, every one checked
- Source
- sha256 974b2a099284d02c…
- Rendering
- no certificate yet
02gen-soundFor any interval of wind speeds, the computed power bounds contain the turbine’s output at every speed in it.proved · shown verbatim
gen-sound :
(I : WS.Interval) (v : Nat) → v WS.∈ I → (genLo I ≤ WM.powerCurve v) × (WM.powerCurve v ≤ genHi I)Shown verbatim: the renderer does not yet read this module’s qualified imports (error:no_sir_line). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.ChoraBridge · line 211
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 7 modules, every one checked
- Source
- sha256 974b2a099284d02c…
- Rendering
- no certificate yet
03genHi-attainedThe upper bound is not loose: some wind speed in the interval actually produces it.proved · shown verbatim
genHi-attained :
(I : WS.Interval) → lo I ≤ hi I → Σ Nat (λ v → Within v I × (WM.powerCurve v ≡ genHi I))Shown verbatim: the renderer does not yet read this module’s qualified imports (error:no_sir_line). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.ChoraBridge · line 222
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 7 modules, every one checked
- Source
- sha256 974b2a099284d02c…
- Rendering
- no certificate yet
04naive-lo-unsoundReading the curve only at an interval’s ends is wrong near cut-out: one end gives 12 kW, the other end 0.proved · shown verbatim
naive-lo-unsound :
(WM.powerCurve (lo stormI) ≡ 12000) × (WM.powerCurve 26000 ≡ 0) × ((hi stormI <ᵇ 26000) ≡ false)Shown verbatim: the renderer does not yet read this module’s qualified imports (error:no_sir_line). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.ChoraBridge · line 342
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 7 modules, every one checked
- Source
- sha256 974b2a099284d02c…
- Rendering
- no certificate yet
05absorb-soundFrom every state, the absorb action meets the absorption contract at the generation cap.proved · shown verbatim
absorb-sound :
(s : EState) → AbsorbOK (absorbS s) (just (capS s))Shown verbatim: the renderer does not yet read this module’s qualified imports (error:no_sir_line). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.Signed · line 436
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 3 modules, every one checked
- Source
- sha256 4ee72ebeee95d006…
- Rendering
- no certificate yet
06curtail-lower-boundAny admissible absorption curtails at least the local supply that the headroom cannot take.proved · shown verbatim
curtail-lower-bound :
(t : EState) (mc : Maybe Nat) → AbsorbOK t mc → localSupply t - headroom t ≤ curtailed t mcShown verbatim: the renderer does not yet read this module’s qualified imports (error:no_sir_line). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.Signed · line 444
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 3 modules, every one checked
- Source
- sha256 4ee72ebeee95d006…
- Rendering
- no certificate yet
07modelledAbsorptionWithinLimitEvery state is within the absorption limit, or one absorb step brings it there.proved · shown verbatim
modelledAbsorptionWithinLimit :
(x : SState) → AbsOK x ⊎ Σ SState (λ y → (sstep x absorb ≡ just y) × AbsOK y)Shown verbatim: the renderer’s display probe declined this statement (refuse:probe_rejected). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.SignedHome · line 131
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 13 modules, every one checked
- Source
- sha256 1c6cfa7a284b7eac…
- Rendering
- no certificate yet
The independent checker
What any proposer, AI included, must pass.
08proposal-soundAn accepted proposal meets its guarantee in every world consistent with the measured intervals.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
proposal-sound :
(pol : Policy) (h : HomeCert) (pr : Proposal) (w : World) → InBox h pr w → Guarantee (band pol) (cap h) (E h) w (checkProposal pol h pr)- Module
- GEC.Verify.Proposal · line 440
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 1 module, every one checked
- Source
- sha256 53b2f98a4fdc3793…
- Rendering
- certificate 4e410206bb2cfe80… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Proposal.agda sha256 53b2f98a4fdc3793
09imp-boundThe checker’s worst-case grid import bounds the import of every consistent world.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
imp-bound :
(h : HomeCert) (pr : Proposal) (w : World) → InBox h pr w → impW w ≤ impWorst h pr- Module
- GEC.Verify.Proposal · line 249
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 1 module, every one checked
- Source
- sha256 53b2f98a4fdc3793…
- Rendering
- certificate 369660e617603c14… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Proposal.agda sha256 53b2f98a4fdc3793
10checkSoundAny step certificate the checker accepts describes a valid step.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
checkSound :
(c : StepCert) → check c ≡ true → ValidStep c- Module
- GEC.Verify.Cert · line 59
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 2 modules, every one checked
- Source
- sha256 154518ace2eb0c05…
- Rendering
- certificate 7295fcbf6108bc19… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Cert.agda sha256 154518ace2eb0c05
11runSafeA run of checked certificates, with a plant that follows them, keeps the budget at every step.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
runSafe :
RunSafeWith check PlantFollows- Module
- GEC.Verify.Cert · line 153
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 2 modules, every one checked
- Source
- sha256 154518ace2eb0c05…
- Rendering
- certificate b6317f764e64007e… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Cert.agda sha256 154518ace2eb0c05
12noRamp-unsafeA checker that ignores load ramps is provably not safe: the ramp clause is necessary.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
noRamp-unsafe :
¬ RunSafeWith checkNoRamp PlantFollows- Module
- GEC.Verify.Cert · line 224
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 2 modules, every one checked
- Source
- sha256 154518ace2eb0c05…
- Rendering
- certificate c95eccc08a34418e… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Cert.agda sha256 154518ace2eb0c05
Evidence & requirements
Evidence that cannot be promoted, and goes stale when it should.
13no-promotionNo rule can turn formal and physical evidence into a third-party fact: evidence classes never promote.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
no-promotion :
¬ ((reg : Registry) (now cfg : Nat) → Formal → Physical → External reg now cfg)- Module
- GEC.Verify.Evidence · line 57
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 1 module, every one checked
- Source
- sha256 58ab03e50aa4039c…
- Rendering
- certificate 9714eba04e599ae7… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Evidence.agda sha256 58ab03e50aa4039c
14invalidation-soundChanging any input invalidates every result that depends on it.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
invalidation-sound :
(g : Graph) (ch : List Nat) → Topo g → {x c : Nat} → Dep g x c → c ∈ ch → invalid g ch x ≡ true- Module
- GEC.Verify.Evidence · line 220
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 1 module, every one checked
- Source
- sha256 58ab03e50aa4039c…
- Rendering
- certificate 903e67321fec8312… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Evidence.agda sha256 58ab03e50aa4039c
15checkProfileSoundThe requirement-profile checker reports exactly each clause’s entry, and each is faithful to the stream.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
checkProfileSound :
(p : Profile) (s : Stream) (es : List Entry) → checkProfile p s ≡ reported es → (es ≡ map (entryOf s) (clauses p)) × All (Faithful s) (clauses p)- Module
- GEC.Verify.Profile · line 967
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 4 modules, every one checked
- Source
- sha256 0409565626ed0e5d…
- Rendering
- certificate bc40318529cdb310… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Verify/Profile.agda sha256 0409565626ed0e5d
The home supervisor
Import limits, reserve, recovery, and a proved design limit.
16supervisorRespectsImportLimitAn invariant holds from the start, survives every supervisor step, and keeps grid import within the cap.proved · shown verbatim
supervisorRespectsImportLimit :
Σ (FState → Bool) (λ I′ → (I′ initP ≡ true) × (((y : PEv) (x : FState) {x′ : FState} → prstep x y ≡ just x′ → Inv x → Inv x′) × (((x : FState) → ReachP x → I′ x ≡ true) × (((x : FState) → I′ x ≡ true → BudgetSettled x ≡ true → 3 - DE.exportCapOf (vw x) ≤ importCapOf (vw x) → OverCap x ≡ false) × ((x : FState) → I′ x ≡ true → BudgetPending x ≡ true → covered x ≡ true)))))Shown verbatim: declared inside an anonymous module, which the renderer does not yet display (refuse:name_in_anonymous_module). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Home.ProtectCert · line 171
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 18 modules, every one checked
- Source
- sha256 5b4faa3fa103b467…
- Rendering
- no certificate yet
17reserve-protectedWith a margin of m, the battery stays above its reserve through m stale readings.proved · shown verbatim
reserve-protected :
(b : BatterySpec) → batterySpecOf em ≡ just b → (w : List PEv) (h : FState) {h′ : FState} → ν h ≡ 0 → rLoss h w ≤ m → runP h w ≡ just h′ → isUp (grid (vw h′)) ≡ true → BatterySpec.reserve b ≤ soc (vw h′)Shown verbatim: declared inside an anonymous module, which the renderer does not yet display (refuse:name_in_anonymous_module). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Home.ProtectReserve · line 295
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 17 modules, every one checked
- Source
- sha256 1f9e58845ae0e7b1…
- Rendering
- no certificate yet
18trilemmaIf a paused EV’s demand exceeds both grid envelopes, no command can keep both: a proved design limit.proved · shown verbatim
trilemma :
(sP : EState) (ds : List Nat) (d : Nat) → sum ds ≡ sum (evDraw sP) + d → importCapOf sP + DE.exportCapOf sP < d → (b : BattFlow) (mc : Maybe Nat) → (DE.exportCapOf sP < D.exportS (cmd sP b) mc) ⊎ (importCapOf sP < U.importS (cmd (resumed sP ds) b) mc)Shown verbatim: declared inside an anonymous module, which the renderer does not yet display (refuse:name_in_anonymous_module). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Home.Trilemma · line 121
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 4 modules, every one checked
- Source
- sha256 f373fe7fa75a30ff…
- Rendering
- no certificate yet
19homeRecoveryEvery home state either recovers within 4 + n supervisor commands, or is provably stuck.proved · shown verbatim
homeRecovery :
(x : FState) → Len x → ((Recovers x × (length (recoverW x) ≤ 4 + nOf n)) × (allB isSup (recoverW x) ≡ true)) ⊎ Stuck xShown verbatim: declared inside an anonymous module, which the renderer does not yet display (refuse:name_in_anonymous_module). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Home.Recover · line 471
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 19 modules, every one checked
- Source
- sha256 51062957b8bbe00f…
- Rendering
- no certificate yet
Chargers & the feeder
OCPP charger behaviour and what we found in the reference tool.
20energy-occupiedA charger delivering energy always reports its connector as occupied.proved · shown verbatim
energy-occupied :
(t : CState) → invB t ≡ true → energy t ≡ true → connectorStatus t ≡ OccupiedShown verbatim: the renderer’s display probe declined this statement (refuse:probe_rejected). The statement is proved either way; only its typeset rendering waits.
- Module
- GEC.Model.Charger · line 1463
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 1 module, every one checked
- Source
- sha256 1c2321dcef805163…
- Rendering
- no certificate yet
21invCount-correctA closed formula counts the charger’s reachable states exactly, for every configuration.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
invCount-correct :
(cfg : TxCfg) → invCount cfg ≡ length (filter (Inv cfg) allStates)- Module
- GEC.Model.ChargerReach · line 53
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 6 modules, every one checked
- Source
- sha256 8c1e996f594f6cd6…
- Rendering
- certificate 8c791f7040d9d7bc… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Model/ChargerReach.agda sha256 8c1e996f594f6cd6
22floor-starvesA budget below the charging floor gives every EV nothing: starvation, proved for every policy.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
floor-starves :
(floor bud : Nat) (as : List Nat) → bud < floor → SemiC floor as → sum as ≤ bud → AllZero as- Module
- GEC.Model.EviBudget · line 141
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 4 modules, every one checked
- Source
- sha256 ba89306fc9384d75…
- Rendering
- certificate 04fc104760008916… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Model/EviBudget.agda sha256 ba89306fc9384d75
23shed-boundWhen EVs shed as commanded, a ledger within budget keeps the next draw within budget.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
shed-bound :
(B : Nat) (es : List EV) → All Shed es → Σledger es ≤ B → Σnext es ≤ B- Module
- GEC.Model.EviLatency · line 123
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 2 modules, every one checked
- Source
- sha256 cabe02e94152f1b8…
- Rendering
- certificate 76eb6b7cd3e88076… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Model/EviLatency.agda sha256 cabe02e94152f1b8
24link-refutes-lt1Under message latency, a concrete case where the ledger fits the budget and the next draw still overshoots.proved · certified rendering
Typeset by the renderer’s display map from the certified LaTeX; the certified Content MathML is embedded in the formula.
The Agda statement
link-refutes-lt1 :
Σ (List (EV × EVw)) (λ ps → (sum (map (λ p → cap (fst p) ⊔ₙ draw (fst p)) ps) ≤ 10) × AllW Link (map snd ps) × (map (λ p → EV.next (fst p)) ps ≡ map (λ p → EVw.next (snd p)) ps) × (10 < sum (map (λ p → EVw.next (snd p)) ps)))- Module
- GEC.Model.EviLatency · line 215
- Checked under
- Agda 2.8.0 · --safe --without-K · no postulates
- Rests on
- 2 modules, every one checked
- Source
- sha256 cabe02e94152f1b8…
- Rendering
- certificate 9f4a2961c637a104… · table tbl0-stdlib · stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core f328acc5bfe3c002; theorem source ./GEC/Model/EviLatency.agda sha256 cabe02e94152f1b8
10 · The dependency tree
Everything a result rests on, one click away.
The whole system, by family. Open a module to see what it rests on and what rests on it; every link is an import the kernel re-checks whenever the system is checked.
Wind & storage6 modules · 2,404 lines
Chora.WindForecast68 declarations · rests on 0 · used by 1Rests on the language’s built-ins only
Used byModel.ChoraBridge
Chora.WindModel35 declarations · rests on 0 · used by 1Rests on the language’s built-ins only
Used byModel.ChoraBridge
Chora.WindSense64 declarations · rests on 0 · used by 1Rests on the language’s built-ins only
Used byModel.ChoraBridge
GEC.Model.ChoraBridgepublished statements56 declarations · rests on 6 · used by 1GEC.Model.Signedpublished statements151 declarations · rests on 3 · used by 13GEC.Model.SignedHomepublished statements34 declarations · rests on 7 · used by 14Rests onCore.NetworkCore.PreludeModel.ChargerModel.EnergyModel.HomeModel.QuantaModel.Signed
Used byEverythingHome.AllocateHome.FillHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceSoundHome.RecoverProbes.ProtectQueryProbes.SignedQuery
Models18 modules · 11,395 lines
GEC.Everything0 declarations · rests on 102 · used by 0Rests onHome.AllocLineHome.AllocateHome.AllocateLinkHome.AllocatorHome.FillHome.ObserveHome.ObserveCertsHome.ObserveChargerHome.ObserveHomeHome.ObserveResidueHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceResidueHome.RaceSoundHome.RecoverHome.RecoverCertsHome.RecoverChargerHome.RecoverGracefulHome.RecoverResidueHome.TrilemmaModel.ChargerModel.ChargerPresentationModel.ChargerReachModel.ChargerReach.CompleteModel.ChargerReach.CountModel.ChargerReach.FormModel.ChargerReach.SoundModel.ChoraBridgeModel.CompleteReachModel.CompleteReachPlusModel.EnergyModel.EviBudgetModel.EviConvexModel.EviLatencyModel.EviQueueModel.HomeModel.HomeAccountingModel.HomeCorpusModel.HomePresentationModel.QuantaModel.SignedModel.SignedHomeModel.StationModel.StoryDesignNet · private coordinatorProbes.AllocQueryProbes.AllocateProbes.ChargerProbes.ChargerCodecProbes.ChargerReachCount1Probes.ChargerReachCount2Probes.ChargerReachCount3Probes.ChargerReachCount4Probes.ChargerReachQueryProbes.ContractProbes.ContractQueryProbes.CoordProbes.EviFindingsProbes.EviFindingsAUSProbes.EviFindingsSFOProbes.EviLatencyFindingsProbes.HomeProbes.HomeQueryProbes.JsProbes.JsCharPrimProbes.JsDeepProbes.JsUnconsProbes.NbhdRaceProbes.ObserveProbes.ObserveQueryProbes.PlantQueryProbes.ProfileProbes.ProtectProbes.ProtectQueryProbes.RaceProbes.RaceQueryProbes.ReachProbes.RecoverProbes.RecoverQueryProbes.SignedFindingsProbes.SignedQueryProbes.SimFindingsProbes.VerifyProbes.VerifyBridgeProbes.VerifyCorpusProbes.VerifyJsVerify.BaseVerify.CertVerify.EvidenceVerify.FormatVerify.HomeFormatVerify.LogVerify.ProfileVerify.ProfileFormatVerify.ProposalVerify.RenderViz.Text
GEC.Model.Chargerpublished statements274 declarations · rests on 1 · used by 53Rests onCore.Prelude
Used byEverythingHome.AllocateHome.FillHome.ObserveChargerHome.ObserveHomeHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceSoundHome.RecoverHome.RecoverChargerHome.RecoverGracefulModel.ChargerPresentationModel.ChargerReachModel.ChargerReach.CompleteModel.ChargerReach.CountModel.ChargerReach.FormModel.ChargerReach.SoundModel.HomeModel.HomeAccountingModel.HomeCorpusModel.HomePresentationModel.SignedHomeModel.StationProbes.AllocQueryProbes.AllocateProbes.ChargerProbes.ChargerCodecProbes.ChargerReachCount1Probes.ChargerReachCount2Probes.ChargerReachCount3Probes.ChargerReachCount4Probes.ChargerReachQueryProbes.ContractProbes.ContractQueryProbes.HomeProbes.HomeQueryProbes.ObserveProbes.ObserveQueryProbes.ProtectProbes.ProtectQueryProbes.RaceProbes.RaceQueryProbes.RecoverProbes.RecoverQueryProbes.SignedFindingsProbes.SignedQueryProbes.SimFindingsNet · private coordinator
GEC.Model.ChargerPresentation94 declarations · rests on 4 · used by 5GEC.Model.ChargerReachpublished statements11 declarations · rests on 6 · used by 2GEC.Model.ChargerReach.Complete489 declarations · rests on 4 · used by 2GEC.Model.ChargerReach.Count82 declarations · rests on 4 · used by 2GEC.Model.ChargerReach.Form26 declarations · rests on 2 · used by 9GEC.Model.ChargerReach.Sound303 declarations · rests on 3 · used by 4GEC.Model.CompleteReach80 declarations · rests on 1 · used by 3Rests onCore.Prelude
GEC.Model.CompleteReachPlus9 declarations · rests on 2 · used by 2Rests onCore.PreludeModel.CompleteReach
Used byEverythingProbes.Reach
GEC.Model.Energy66 declarations · rests on 2 · used by 31Rests onCore.PreludeModel.Quanta
Used byEverythingHome.AllocateHome.FillHome.ObserveHomeHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceSoundHome.RecoverHome.TrilemmaModel.HomeModel.HomeAccountingModel.HomeCorpusModel.HomePresentationModel.SignedModel.SignedHomeProbes.AllocQueryProbes.ContractQueryProbes.HomeProbes.HomeQueryProbes.ObserveQueryProbes.PlantQueryProbes.ProtectQueryProbes.RaceQueryProbes.RecoverQueryProbes.SignedQueryNet · private coordinator
GEC.Model.Home115 declarations · rests on 6 · used by 28Rests onCore.NetworkCore.PreludeModel.ChargerModel.EnergyModel.QuantaModel.Station
Used byEverythingHome.AllocateHome.FillHome.ObserveHomeHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceSoundHome.RecoverModel.HomeAccountingModel.HomeCorpusModel.HomePresentationModel.SignedHomeProbes.AllocQueryProbes.ContractQueryProbes.HomeProbes.HomeQueryProbes.ObserveQueryProbes.PlantQueryProbes.ProtectQueryProbes.RaceQueryProbes.RecoverQueryProbes.SignedQueryNet · private coordinator
GEC.Model.HomeAccounting7 declarations · rests on 5 · used by 1GEC.Model.HomeCorpus16 declarations · rests on 5 · used by 15Rests onCore.PreludeModel.ChargerModel.EnergyModel.HomeModel.Quanta
Used byEverythingProbes.AllocateProbes.ContractProbes.HomeProbes.HomeQueryProbes.ObserveProbes.PlantQueryProbes.ProtectProbes.ProtectQueryProbes.RaceProbes.RaceQueryProbes.RecoverProbes.SignedFindingsProbes.SignedQueryProbes.SimFindings
GEC.Model.HomePresentation82 declarations · rests on 10 · used by 1GEC.Model.Quanta60 declarations · rests on 1 · used by 49Rests onCore.Prelude
Used byEverythingHome.AllocateHome.FillHome.ObserveHomeHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceSoundHome.RecoverHome.TrilemmaModel.ChoraBridgeModel.EnergyModel.EviBudgetModel.EviConvexModel.EviLatencyModel.EviQueueModel.HomeModel.HomeAccountingModel.HomeCorpusModel.HomePresentationModel.SignedModel.SignedHomeModel.StoryDesignProbes.AllocQueryProbes.AllocateProbes.ContractProbes.ContractQueryProbes.HomeProbes.HomeQueryProbes.JsProbes.ObserveProbes.ObserveQueryProbes.PlantQueryProbes.ProtectProbes.ProtectQueryProbes.RaceProbes.RaceQueryProbes.RecoverProbes.RecoverQueryProbes.SignedFindingsProbes.SignedQueryProbes.SimFindingsProbes.VerifyBridgeViz.TextNet · private coordinator
GEC.Model.Station121 declarations · rests on 2 · used by 4GEC.Model.StoryDesign55 declarations · rests on 2 · used by 1Rests onCore.PreludeModel.Quanta
Used byEverything
Home supervisor25 modules · 9,452 lines
GEC.Home.Allocate67 declarations · rests on 16 · used by 2GEC.Home.AllocateLink23 declarations · rests on 4 · used by 1GEC.Home.Allocator128 declarations · rests on 5 · used by 5GEC.Home.AllocLine20 declarations · rests on 6 · used by 1GEC.Home.Fill197 declarations · rests on 7 · used by 19Rests onCore.PreludeModel.ChargerModel.EnergyModel.HomeModel.QuantaModel.SignedModel.SignedHome
Used byEverythingHome.AllocateHome.ObserveHomeHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceSoundHome.RecoverProbes.AllocQueryProbes.ContractQueryProbes.ObserveQueryProbes.ProtectQueryProbes.RaceQueryProbes.RecoverQueryNet · private coordinator
GEC.Home.Observe44 declarations · rests on 2 · used by 2Rests onCore.ControlCore.Prelude
GEC.Home.ObserveCerts6 declarations · rests on 2 · used by 2Rests onCore.CertSrsCore.CertSyntax
GEC.Home.ObserveCharger89 declarations · rests on 4 · used by 1GEC.Home.ObserveHome7 declarations · rests on 9 · used by 2GEC.Home.ObserveResidue44 declarations · rests on 6 · used by 1GEC.Home.Protect77 declarations · rests on 7 · used by 15Rests onCore.PreludeHome.FillModel.ChargerModel.EnergyModel.HomeModel.QuantaModel.SignedHome
Used byEverythingHome.AllocateHome.ObserveHomeHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RecoverProbes.AllocQueryProbes.ContractQueryProbes.ObserveQueryProbes.ProtectQueryProbes.RecoverQueryNet · private coordinator
GEC.Home.ProtectBound21 declarations · rests on 10 · used by 4GEC.Home.ProtectCertpublished statements53 declarations · rests on 11 · used by 6GEC.Home.ProtectReservepublished statements49 declarations · rests on 10 · used by 2GEC.Home.ProtectResidue38 declarations · rests on 12 · used by 5GEC.Home.ProtectSafety93 declarations · rests on 9 · used by 10GEC.Home.Race68 declarations · rests on 7 · used by 2GEC.Home.RaceResidue24 declarations · rests on 6 · used by 2GEC.Home.RaceSound34 declarations · rests on 11 · used by 1GEC.Home.Recoverpublished statements127 declarations · rests on 12 · used by 2GEC.Home.RecoverCerts5 declarations · rests on 2 · used by 2Rests onCore.CertAutCore.CertSyntax
GEC.Home.RecoverCharger28 declarations · rests on 3 · used by 2GEC.Home.RecoverGraceful96 declarations · rests on 2 · used by 3GEC.Home.RecoverResidue63 declarations · rests on 4 · used by 1GEC.Home.Trilemmapublished statements17 declarations · rests on 4 · used by 1Rests onCore.PreludeModel.EnergyModel.QuantaModel.Signed
Used byEverything
Open verifier10 modules · 4,354 lines
GEC.Verify.Base87 declarations · rests on 0 · used by 19Rests on the language’s built-ins only
Used byEverythingHome.AllocLineHome.AllocateHome.AllocatorProbes.AllocateProbes.CoordProbes.ProfileProbes.VerifyProbes.VerifyBridgeVerify.CertVerify.EvidenceVerify.FormatVerify.HomeFormatVerify.LogVerify.ProfileVerify.ProfileFormatVerify.ProposalVerify.RenderNet · private coordinator
GEC.Verify.Certpublished statements75 declarations · rests on 2 · used by 10GEC.Verify.Evidencepublished statements54 declarations · rests on 1 · used by 4GEC.Verify.Format35 declarations · rests on 1 · used by 17GEC.Verify.HomeFormat31 declarations · rests on 3 · used by 2GEC.Verify.Log28 declarations · rests on 3 · used by 4GEC.Verify.Profilepublished statements259 declarations · rests on 4 · used by 6GEC.Verify.ProfileFormat114 declarations · rests on 4 · used by 3GEC.Verify.Proposalpublished statements153 declarations · rests on 1 · used by 3Rests onVerify.Base
GEC.Verify.Render5 declarations · rests on 2 · used by 4
EVI-DiST analysis4 modules · 723 lines
GEC.Model.EviBudgetpublished statements39 declarations · rests on 3 · used by 6GEC.Model.EviConvex45 declarations · rests on 4 · used by 3GEC.Model.EviLatencypublished statements40 declarations · rests on 2 · used by 5GEC.Model.EviQueue5 declarations · rests on 3 · used by 1Rests onCore.PreludeModel.EviBudgetModel.Quanta
Used byEverything
Neighbourhood coordinator7 modules · 2,290 lines
GEC.Net · private coordinator7 modules · checked, unpublished · rests on 15 · used by 11Rests onCore.NetworkCore.PlanLB11Core.PreludeHome.FillHome.ProtectModel.ChargerModel.EnergyModel.EviLatencyModel.HomeModel.QuantaVerify.BaseVerify.CertVerify.FormatVerify.LogVerify.Render
Used byEverythingHome.AllocLineHome.AllocateHome.AllocateLinkHome.AllocatorProbes.AllocQueryProbes.AllocateProbes.ContractProbes.ContractQueryProbes.CoordProbes.NbhdRace
Visual emitters1 module · 252 lines
GEC.Viz.Text31 declarations · rests on 2 · used by 3Rests onCore.PreludeModel.Quanta
Gluing Engine core37 modules · 21,254 lines
GE.Core.CertAut126 declarations · rests on 5 · used by 2GE.Core.CertConn41 declarations · rests on 7 · used by 2GE.Core.CertGauge67 declarations · rests on 6 · used by 3GE.Core.CertKit25 declarations · rests on 3 · used by 6GE.Core.CertOpen61 declarations · rests on 11 · used by 1GE.Core.CertPoly110 declarations · rests on 5 · used by 1GE.Core.CertSrs279 declarations · rests on 18 · used by 2GE.Core.CertSyntax105 declarations · rests on 1 · used by 8GE.Core.Complex179 declarations · rests on 3 · used by 13GE.Core.Control76 declarations · rests on 1 · used by 2Rests onCore.Prelude
GE.Core.Cover215 declarations · rests on 4 · used by 4GE.Core.DivModN8 declarations · rests on 1 · used by 1Rests onCore.Prelude
Used byCore.PolyZ
GE.Core.Gauge148 declarations · rests on 4 · used by 4GE.Core.IntOrder52 declarations · rests on 3 · used by 3GE.Core.Kronecker86 declarations · rests on 5 · used by 1GE.Core.Network102 declarations · rests on 5 · used by 8GE.Core.Newman87 declarations · rests on 6 · used by 4GE.Core.NormalForm142 declarations · rests on 3 · used by 8GE.Core.OpenComplex58 declarations · rests on 6 · used by 1GE.Core.Peaks137 declarations · rests on 4 · used by 5GE.Core.PlanLB11182 declarations · rests on 2 · used by 1Rests onCore.NetworkCore.Prelude
Used byNet · private coordinator
GE.Core.PolyZ102 declarations · rests on 6 · used by 3GE.Core.Prelude81 declarations · rests on 0 · used by 115Rests on the language’s built-ins only
Used byCore.CertConnCore.CertGaugeCore.CertKitCore.CertOpenCore.CertPolyCore.CertSrsCore.CertSyntaxCore.ComplexCore.ControlCore.CoverCore.DivModNCore.GaugeCore.IntOrderCore.KroneckerCore.NetworkCore.NewmanCore.NormalFormCore.OpenComplexCore.PeaksCore.PlanLB11Core.PolyZCore.PresentationCore.RaceCore.RankCore.RealCellsCore.RelaxCore.RingSolveCore.SquierCore.SquierCtxCore.TaskCore.WordCore.ZFastCore.ZZHome.AllocateHome.AllocateLinkHome.FillHome.ObserveHome.ObserveChargerHome.ObserveHomeHome.ObserveResidueHome.ProtectHome.ProtectBoundHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyHome.RaceHome.RaceResidueHome.RaceSoundHome.RecoverHome.RecoverChargerHome.RecoverGracefulHome.TrilemmaModel.ChargerModel.ChargerPresentationModel.ChargerReachModel.ChargerReach.CompleteModel.ChargerReach.CountModel.ChargerReach.FormModel.ChargerReach.SoundModel.ChoraBridgeModel.CompleteReachModel.CompleteReachPlusModel.EnergyModel.EviBudgetModel.EviConvexModel.EviLatencyModel.EviQueueModel.HomeModel.HomeAccountingModel.HomeCorpusModel.HomePresentationModel.QuantaModel.SignedModel.SignedHomeModel.StationModel.StoryDesignProbes.AllocQueryProbes.AllocateProbes.ChargerProbes.ChargerCodecProbes.ChargerReachCount1Probes.ChargerReachCount2Probes.ChargerReachCount3Probes.ChargerReachCount4Probes.ChargerReachQueryProbes.ContractProbes.ContractQueryProbes.EviFindingsProbes.EviFindingsAUSProbes.EviFindingsSFOProbes.EviLatencyFindingsProbes.HomeProbes.HomeQueryProbes.JsProbes.JsCharPrimProbes.JsDeepProbes.JsUnconsProbes.NbhdRaceProbes.ObserveProbes.ObserveQueryProbes.PlantQueryProbes.ProtectProbes.ProtectQueryProbes.RaceProbes.RaceQueryProbes.ReachProbes.RecoverProbes.RecoverQueryProbes.SignedFindingsProbes.SignedQueryProbes.SimFindingsProbes.VerifyBridgeViz.TextNet · private coordinator
GE.Core.Presentation130 declarations · rests on 3 · used by 19Rests onCore.PreludeCore.RelaxCore.Word
Used byCore.CertOpenCore.CertSrsCore.ComplexCore.CoverCore.NetworkCore.NewmanCore.NormalFormCore.OpenComplexCore.PeaksCore.RaceCore.SquierCore.SquierCtxCore.TaskHome.ProtectResidueHome.RaceResidueHome.RaceSoundModel.ChargerPresentationModel.HomePresentationProbes.Charger
GE.Core.Race103 declarations · rests on 7 · used by 1GE.Core.Rank408 declarations · rests on 2 · used by 4GE.Core.RealCells173 declarations · rests on 6 · used by 1GE.Core.Relax34 declarations · rests on 1 · used by 3Rests onCore.Prelude
GE.Core.Reset66 declarations · rests on 1 · used by 2Rests onGolden.Hub.Sync.PairBarrier
GE.Core.RingSolve83 declarations · rests on 2 · used by 3Rests onCore.PreludeCore.ZFast
GE.Core.Squier145 declarations · rests on 7 · used by 1GE.Core.SquierCtx69 declarations · rests on 8 · used by 1GE.Core.Task115 declarations · rests on 3 · used by 3GE.Core.Word42 declarations · rests on 1 · used by 27Rests onCore.Prelude
Used byCore.CertConnCore.CertGaugeCore.CertOpenCore.CertSrsCore.ComplexCore.CoverCore.GaugeCore.NetworkCore.NewmanCore.NormalFormCore.OpenComplexCore.PeaksCore.PresentationCore.RaceCore.SquierCore.SquierCtxCore.TaskHome.ObserveHomeHome.ProtectResidueHome.RaceResidueHome.RaceSoundModel.ChargerPresentationModel.HomePresentationProbes.ChargerProbes.ObserveProbes.ObserveQueryProbes.ProtectQuery
GE.Core.ZFast29 declarations · rests on 2 · used by 5GE.Core.ZZ75 declarations · rests on 1 · used by 4Rests onCore.Prelude
Golden.Hub.Sync.PairBarrier207 declarations · rests on 0 · used by 1Rests on the language’s built-ins only
Used byCore.Reset
Kernel probes41 modules · 12,666 lines
GEC.Probes.Allocate82 declarations · rests on 12 · used by 1GEC.Probes.AllocQuery8 declarations · rests on 16 · used by 2GEC.Probes.Charger29 declarations · rests on 6 · used by 1GEC.Probes.ChargerCodec46 declarations · rests on 2 · used by 8GEC.Probes.ChargerReachCount117 declarations · rests on 4 · used by 1GEC.Probes.ChargerReachCount217 declarations · rests on 4 · used by 1GEC.Probes.ChargerReachCount317 declarations · rests on 4 · used by 1GEC.Probes.ChargerReachCount417 declarations · rests on 4 · used by 1GEC.Probes.ChargerReachQuery8 declarations · rests on 4 · used by 1GEC.Probes.Contract102 declarations · rests on 6 · used by 1GEC.Probes.ContractQuery7 declarations · rests on 10 · used by 2GEC.Probes.Coord283 declarations · rests on 6 · used by 1GEC.Probes.EviFindings6 declarations · rests on 2 · used by 1Rests onCore.PreludeModel.EviBudget
Used byEverything
GEC.Probes.EviFindingsAUS9 declarations · rests on 3 · used by 1Rests onCore.PreludeModel.EviBudgetModel.EviConvex
Used byEverything
GEC.Probes.EviFindingsSFO9 declarations · rests on 3 · used by 1Rests onCore.PreludeModel.EviBudgetModel.EviConvex
Used byEverything
GEC.Probes.EviLatencyFindings18 declarations · rests on 2 · used by 2Rests onCore.PreludeModel.EviLatency
Used byEverythingProbes.NbhdRace
GEC.Probes.Home122 declarations · rests on 7 · used by 1GEC.Probes.HomeQuery45 declarations · rests on 8 · used by 11Rests onCore.PreludeModel.ChargerModel.EnergyModel.HomeModel.HomeCorpusModel.QuantaModel.StationProbes.ChargerCodec
Used byEverythingProbes.AllocQueryProbes.ContractQueryProbes.HomeProbes.ObserveQueryProbes.PlantQueryProbes.ProtectQueryProbes.RaceQueryProbes.RecoverQueryProbes.SignedQueryProbes.SimFindings
GEC.Probes.Js42 declarations · rests on 3 · used by 1Rests onCore.PreludeModel.QuantaViz.Text
Used byEverything
GEC.Probes.JsCharPrim2 declarations · rests on 1 · used by 1Rests onCore.Prelude
Used byEverything
GEC.Probes.JsDeep3 declarations · rests on 1 · used by 1Rests onCore.Prelude
Used byEverything
GEC.Probes.JsUncons3 declarations · rests on 2 · used by 1Rests onCore.PreludeViz.Text
Used byEverything
GEC.Probes.NbhdRace83 declarations · rests on 5 · used by 1GEC.Probes.Observe144 declarations · rests on 7 · used by 1GEC.Probes.ObserveQuery3 declarations · rests on 12 · used by 2GEC.Probes.PlantQuery25 declarations · rests on 6 · used by 2GEC.Probes.Profile25 declarations · rests on 5 · used by 2GEC.Probes.Protect181 declarations · rests on 5 · used by 1GEC.Probes.ProtectQuery45 declarations · rests on 16 · used by 6Rests onCore.PreludeCore.WordHome.FillHome.ProtectHome.ProtectCertHome.ProtectReserveHome.ProtectResidueHome.ProtectSafetyModel.ChargerModel.EnergyModel.HomeModel.HomeCorpusModel.QuantaModel.SignedHomeProbes.HomeQueryProbes.RaceQuery
Used byEverythingProbes.AllocQueryProbes.ContractQueryProbes.ObserveQueryProbes.ProtectProbes.RecoverQuery
GEC.Probes.Race248 declarations · rests on 5 · used by 1GEC.Probes.RaceQuery28 declarations · rests on 9 · used by 3GEC.Probes.Reach20 declarations · rests on 3 · used by 1GEC.Probes.Recover153 declarations · rests on 5 · used by 1GEC.Probes.RecoverQuery13 declarations · rests on 13 · used by 2GEC.Probes.SignedFindings164 declarations · rests on 5 · used by 1GEC.Probes.SignedQuery19 declarations · rests on 10 · used by 2GEC.Probes.SimFindings16 declarations · rests on 5 · used by 1GEC.Probes.Verify161 declarations · rests on 7 · used by 1GEC.Probes.VerifyBridge6 declarations · rests on 4 · used by 1Rests onCore.PreludeModel.QuantaVerify.BaseVerify.Format
Used byEverything
GEC.Probes.VerifyCorpus2 declarations · rests on 0 · used by 3Rests on the language’s built-ins only
GEC.Probes.VerifyJs1 declarations · rests on 2 · used by 1Rests onProbes.VerifyCorpusVerify.Log
Used byEverything
The module graph as JSON · drawn from a frozen snapshot of the toolkit; the private coordinator appears as one node.
11 · The development record
21 of 48 phases closed, each with its gate.
A phase closes only when its gate passes: proofs checked, seeded mistakes caught, results reproduced. This record grows here as each one lands.
Foundations
- P0aOCPP 2.0.1 / 2.1 witnessed
- P0bFrozen contract corpus
- V0Visuals emitted by Agda
Charger
- H1OCPP charger model
- H1bEvery reachable state, counted
Home, wind & storage
- H2Home supervisor
- S1Independent simulator
- SASigned flows · wind absorption
- H3Certified decision order
- H4PROTECT supervisor
- H5aVerifier bound, measured
- H5Recovery
- H6Minimal telemetry
- H7Allocation
- H8Device monitors
NLR EVI-DiST
- E1Public scenario replicated
- E1bThree regions
- E4EV plant with latency
- ST1The night everyone plugged in
- E2Its policies certified
- E3HELICS adapter
- E5Upstream package
Neighbourhood
- N1Coordinator ledger
- N2Proved street rule
- N3
- N4
- N5
Verifier & profiles
- VF1Open verifier · checkProposal
- PR1Requirement profiles
- PR2Reporting exports
Simulation, devices & close-out
- S2–S4Campaigns
- D1–D4Device builds
- T1–T2Tooling
- C1–C3Close-out & landing
closed · brass: in progress · dashed: planned
12 · The CIP proposal
Auditable Supervisory Assurance for Distributed Wind.
Our proposal to NLR’s 2026 Competitiveness Improvement Project turns this toolkit into a component a U.S. turbine maker can integrate: advisory in Phase 1, beside the existing protections, with public artifacts at the end of one bounded phase.
| Topic | 4 · Component Innovation · six months · Phase 1 |
|---|---|
| Manufacturer | Uprise Energy, 12-kW Mobile Power Station (signed participation letter) |
| Demonstrator A | Public/synthetic wind–storage–critical-load system anchored to the 12-kW reference |
| Demonstrator B | A public EVI-DiST feeder with wind, storage, EV charging and other demand |
| Acceptance | Core proofs check in the pinned environment; ≥ 100 named scenarios; ≥ 10 safeguard mutations; zero unexplained checker/reference differences; clean-room reproduction |
| Public release | Agda specifications, generated checker, EVI-DiST adapter, scenarios, replay tools, SBOM, under BSD-3-Clause |
Standards it is built against
- NIST SSDF 1.1 for secure software development
- NIST SP 800-82r3 for operational-technology threat boundaries
- NIST AI RMF 1.0 for documenting AI risk
- Selected NASA-STD-7009B practices for modelling credibility
- A qualification map to ANSI/ACP 101-1-2021, IEC 61400-2 and applicable UL requirements
These guide development and evaluation. Product certification is a later, separate step, and the plan names its route rather than assuming it.
13 · Read further
The mathematics underneath.
The toolkit runs on our Gluing Engine, which turns the local rules of a system into machine-checked answers about the whole. Two recent papers set out the method; the full library tells the whole story, from the kernel up.
Where the Parts Make a Whole
A certified instrument for collective sense-makingThe engine underneath: give it the local rules a system follows, and it returns machine-checked answers on which states are the same, whether order matters, what survives failure and whether every local view can agree. Section 3 works the EV charger in a home with solar, wind and a battery end to end.Read the paper (PDF) →3 November 2026 · preprint
What Meaning Can Copy
Machine-checked copy laws, braiding limits and exact acceptance for compositional modelsThe semantic side: exactly what copying permits in compositional models of meaning, from shared weights in learned models to quantum readings, with laws checked by machine and an experiment registered before it was run.Read the paper (PDF) →
Who it is built with
A real turbine. A public tool. An open result.
The work is anchored to hardware a U.S. manufacturer ships and to data anyone can download, so every result can be checked by someone other than us.
Manufacturer partner
Uprise Energy
Maker of the 12-kW Mobile Power Station, the reference system for Demonstrator A, with a signed participation letter for the proposed Phase 1.
Public tool
NLR’s EVI-DiST
Used as published, on public data, for Demonstrator B and the results above. About EVI-DiST →