Energy & infrastructure · Research 001 · with Morningstar
Let the sun set the pace. Let proof hold the line.
A solar controller knows the power available. A verified supervisor asks the next question: which work can we admit, while preserving the reserve? This page is the open record of that research, from the first proof to the first real instrument, and it grows as each round of work produces evidence.
Round 1 of 6 complete · software research done · bench commissioning next
01 · The solar observatory
Every decision has a consequence. Inspect it.
Follow a synthetic day, from harvest to essential service and flexible work. Both policies face exactly the same weather; every verdict shown was produced by the native core and recorded.
Loading recorded evidence…
02 · The mathematics
The mathematics is part of the machine.
Tests examine examples. A proof establishes a stated property for every input satisfying its assumptions. Here the decision procedure and its witnesses live in the same safe Agda core, compiled to the native executable.
I · A current budget that composes
Reserve before you send.
Iessential + Σ Ireserved + Inew ≤ Ilimit
An accepted reservation preserves the ledger’s current bound. Pending and uncertain commands retain their allocation; an acknowledgment does not count as a physical observation.
II · A conservative energy invariant
Keep the reserve in view.
E + Glower − Dessential− Dflexible ≥ R
Admitted work preserves the modeled reserve floor when actual generation and demand respect the declared bounds. A forecast cannot quietly become guaranteed energy. If essential demand alone is infeasible, the result stays visible.
III · Evidence with an expiry
Recheck at the boundary.
0 ≤ now − tsample ≤ agemaxΔtsamples ≤ skewmax
Admission also binds measurement quality, source, configuration and epoch. Queued work is authorized again against the current ledger immediately before sending, so stale approval cannot grant fresh authority.
The exact scope matters: these are software properties under explicit model and input assumptions. They do not prove controller firmware, physical wiring, battery state of charge, or electrical fail-off. Essential-channel separation is structural; hardware validation is a separate research step.
03 · Open the whole record
Show the limits, alongside the results.
No hand-picked victory lap. All twelve scenarios and all three weather seeds stay in the comparison, including the low-energy failures and the missing measurements.
| Scenario | Supervisor | Baseline | Reserve breaches · sup. / base |
|---|---|---|---|
| C01 · Steady supply | 9 / 9 | 9 / 9 | 0 / 0 |
| C02 · Cloud budget | 6 / 9 | 6 / 9 | 0 / 0 |
| C03 · Extended low generation | 6 / 9 | 6 / 9 | 54 / 54 |
| C04 · Overoptimistic forecast | 9 / 9 | 9 / 9 | 0 / 0 |
| C05 · Invalid modeled SOC | 0 / 9 | 0 / 9 | 0 / 0 |
| C06 · Stale measurement | 0 / 9 | 0 / 9 | 0 / 0 |
| C07 · Delayed command | 0 / 9 | 0 / 9 | 0 / 0 |
| C08 · Lost acknowledgment | 3 / 9 | 3 / 9 | 51 / 51 |
| C09 · Restart while on | 6 / 9 | 6 / 9 | 67 / 67 |
| C10 · Native schedule conflict | 6 / 9 | 6 / 9 | 0 / 0 |
| C11 · Configuration mismatch | 6 / 9 | 6 / 9 | 0 / 0 |
| C12 · Insufficient resolution | 9 / 9 | 9 / 9 | 0 / 0 |
04 · The development record
Built in the open, one round at a time.
Each round has a gate: what must be true, on real evidence, before it is called complete. When a round passes, its evidence is published here and the page gains what the round brings. Until then it says plainly what is still to come.
- 01
Phases A–Bcomplete · 2026-11-05
From construction to execution.
A safe Agda core states the supervisor’s rules and proves them; the same core is extracted to a native executable that runs the simulator, the paired policy comparisons, exact replay and the dashboard. Thirty-six of the plan’s forty-four sprints.
Its gate
Every core property proved in safe Agda; every reference run reproduced from source; discrimination controls that must catch planted faults, caught.
On this page
- The solar observatory over all 72 recorded runs
- The three theorems with their exact proof sources
- The complete comparison table, failures included
Explore the observatory Proof sources (19 modules) All 72 reference runs
- 02
Native consolein development
Our console, speaking the controller’s own language.
The supervisor learns the GenStar’s native vocabulary: identity, modes, telemetry, history and settings, each read through a contract the proved core can check. The configuration a relay channel would receive is constructed and witnessed by the core itself, not by a script beside it.
To be complete
Every native read and setting the demonstration relies on has a checked meaning, units and legal range on the exact controller profile; the request path schedules within the device’s real capacity without relaxing freshness.
Adds to this page
- Run a fresh policy pair in the browser, through the native core
- Exact replay of any recorded run, call by call
- The native settings explorer: what each value means and which values the core admits
- 03
Phase Cnext on the bench
Meet the actual instrument.
A qualified operator commissions the bench: inventory, source, protection, earthing, firmware and the reference meter, all recorded. Then the supervisor watches, and only watches, a real GenStar for at least ten minutes, with its readings compared against an independent meter at the beginning, middle and end.
To be complete
At least 600 seconds of valid read-only telemetry from the real controller, every gap retained, native and meter readings in agreement, and the operator’s attestation. No writes.
Adds to this page
- A live telemetry strip: the GenStar feed beside the reference meter
- The commissioning record and the full capture, gaps included, for download
- The hardware-seconds figure above, counting up from zero
- 04
Phase Dplanned
Advise in the shadow, beside the native controller.
The supervisor runs beside Morningstar’s own relay schedule and says what it would admit and what it would refuse, while the native controller stays in charge. A deliberate network interruption tests that it recovers without inventing authority.
To be complete
At least two observed on/off cycles, at least two accepted and two rejected recommendations with their reasons, and one attended interruption with clean reconciliation.
Adds to this page
- The shadow log: each recommendation, the core’s verdict, and what the controller actually did
- The recovery trace from the attended interruption
- 05
Phase Econditional
Attended control of a single channel.
Only if a documented, supported command interface exists for an individual relay channel. The first command is a harmless off; every command is followed by a separate readback; restart and a lost acknowledgment are exercised while attended. Without that interface, this round stays open and says so.
To be complete
A supported channel mapping confirmed from qualified evidence, then an attended actuation receipt: exact channel, readback, native schedule intact, no effect on any other channel.
Adds to this page
- The first proof-gated command to real hardware, with its readback
- The interface dossier: what is supported, and what remains unanswered
- 06
Phase Fplanned
Hand it to someone who did not build it.
A reproducible review package (technical report, two-page findings, operator runbook, application note, five-minute walkthrough) and an independent reviewer who reproduces a fresh scenario end to end and tries to catch planted faults.
To be complete
A non-author reads the proofs, catches the planted faults and reproduces the pipeline with matching hashes; hardware review recorded separately.
Adds to this page
- The technical report and findings
- The independent reviewer’s receipt
- The five-minute walkthrough
05 · Questions & sources
What this establishes.
What does the comparison actually establish?
Both policies pass through the same verified admission core, under the same documented weather and loads, so any difference is the policy itself. The baseline is a documented threshold and schedule policy. Priority order changes the sequence of proposals, and where the curves overlap, that is the result.
What is modeled, and what is measured?
Storage and power flows are modelled today; measurement on a real controller is the next round. C12 deliberately includes 24 current-measurement gaps, and modelled energy is labelled as such. Every reserve failure in the zero-generation case is shown, essential-only infeasibility included.
Does this page send commands to a controller?
No. Everything here is recorded simulation evidence. Installed firmware and device capabilities are established during commissioning, and no command reaches hardware before the attended-actuation round, if that round becomes possible at all.
Inspect the native build and evidence provenance
Provenance manifest · Viewer data · Full runs, event chains, inputs and formal sources
Every run is hash-chained, and a download provides the exact native inputs and outputs for independent replay.
Morningstar technical references
The research references GenStar MPPT, GenStar Modbus specification and LiveView. Installed firmware and device capabilities are established during commissioning.
Research & equipment partner
Better questions. Re-checkable answers.
Morningstar’s equipment support makes this line of research possible. IAOM contributes constructive mathematics, executable proofs, and a record anyone can inspect as the work progresses.