Agriculture & pollinators · Research 003 · at Brumble Bee Farms
What makes a sensor reading worth keeping? Verifiable sensor data, at the hive.
A reading can outlive the reasons for trusting it. At our research apiary we are building readings that carry their own argument: which instrument, placed where, calibrated how, interpreted by which model, and fit for which question. Proved where proof applies, measured where the world decides.
Measurement core in development · report published · instrument characterization next
- 01 · Weather & flight[⅘, 6⁄5] Ka change in temperature: the same answer in Celsius and in kelvin⊢ windowDifferenceSound
- 02 · Hive weightm ∈ [c − r, c + r]nectar flow and stores, calibrated with honest error bars⊢ massEnclosureSound
- 03 · Fit for the question4 of 4a study decides whether the evidence fits its purpose, and says why
- 04 · Identity5 layersequipment, asset, installation, channel and configuration travel with every reading⊢ chainSound
- 05 · Brood-nest heatSₖ₊₁ = a·Sₖ + (1 − a)·Tₖ + eₖa thermal response you can inspect, enclosed step by step⊢ thermalStepSound
- 06 · ForagingΣ wᵢlᵢ ⁄ Wwindow averages that keep missing and refused slots visible⊢ weightedMeanSound
01 · A question at the hive
A hive cools overnight. Why?
A beekeeper may need to decide whether to open the hive; a scientist may want to compare it with other colonies and seasons. Both need to know how the recorded trace relates to what they care about. A number such as 18.5 °C, on its own, cannot say.
- The colonyis producing less heat
- The airoutside has cooled
- The windhas raised heat loss
- The probeis still catching up with a change that happened earlier
Each explanation leads to a different action, and the trace alone cannot choose between them. The reading has to carry more than its number.
02 · The reading and the room
A probe is not the air around it.
Every probe lags. Model the lag, and a reading becomes a precise statement about the world: not one temperature, but the exact range of environments that could have produced it. Change the probe’s speed and watch the honest answer change.
How quickly does the probe respond?
a is how much of the previous reading survives each step: near 0 the probe tracks the air at once, near 1 it barely moves.
The probe now reads 18.3–18.7 °C, after reading 14 °C. The air must be:
26.47 – 28.53 °C
exactly [1853/70, 1997/70] · width 2.06 °C
A reading of about 18.5 °C can mean a much warmer room when the probe is still warming. Treat it as the air temperature and the explanation is lost; the slower the probe, the wider the honest answer.
03 · What a reading carries
More than a number, and more than a device name.
Swap the calibration files of two identical probes and every spreadsheet column still looks right. Bind each reading to who measured it, where and how, and the swap is caught before a plausible wrong answer becomes a research input.
Its identity, layer by layer
- Equipment classwhat kind of instrument
- Assetwhich individual instrument
- Installationwhere and how it is placed
- Channelwhich signal it reports
- Configurationthe interpretation in force for this record
Its journey, step by step
- Physical quantity
- Instrument response
- Raw record
- Calibration enclosure
- Model transformation
- Aggregate
- Study decision
Software checks every computational step and keeps it bound to its inputs. At the two ends, where the physical world and a human question meet, empirical evidence stays indispensable.
04 · Five contracts
Proved in safe Agda, run as native code.
Each contract is a theorem with a precise scope: if the evidence holds, the result follows, for every input. Exact rational arithmetic removes rounding from these calculations; it never pretends to remove physical uncertainty.
thermalStepSoundA thermal response you can inspect
Sₖ₊₁ = a·Sₖ + (1 − a)·Tₖ + eₖ, 0 ≤ a ≤ 1
If the sensor state, the environment and the residual each lie in their intervals, the next state lies in the computed enclosure, step after step.
massEnclosureSoundCalibration with honest error bars
m ∈ [c − r, c + r], c = (n·g + b)/d, r = (n·δg + δb + δs)/d
Every realization of an affine calibration with bounded gain, offset and residual errors lies inside the interval, and its extremes reach the endpoints.
chainSoundThe result belongs to this record
inputs · digests · calibration · model · provenance ⇒ result
A result is indexed by the exact inputs and stages its theorem applies to. A correct answer for some other record is not accepted.
weightedMeanSoundAverages that keep their contributors
[ Σ wᵢlᵢ / W , Σ wᵢuᵢ / W ], W = Σ wᵢ > 0
A weighted mean over a time window, with missing and refused slots kept visible rather than silently dropped.
windowDifferenceSoundChanges with their units intact
A − B ∈ [ aₗ − bᵤ , aᵤ − bₗ ]
The difference between two windows, as a temperature difference: the Celsius-to-kelvin offset correctly never enters it.
Agda 2.8.0 with --safe and --without-K, standard library 2.3, compiled through MAlonzo and GHC 9.12.2.
05 · Tested against substitutions
The right answer, for the right record, for the right reason.
A typechecker can accept a weak or irrelevant statement. So the audit also asks whether each result still says what the science needs, and whether it belongs to the record it claims.
The same question, three ways
| Reference case | Difference | Decision |
|---|---|---|
| Leaf, in Celsius4 of 4 slots | [4/5, 6/5] K difference | Fits the study profile |
| Root, in kelvin4 of 4 slots | [4/5, 6/5] K difference | Fits the study profile |
| Leaf, expired calibration and a gap1 of 4 slots | unavailable | Insufficient evidence |
Celsius and kelvin agree exactly, and missing evidence stays visible instead of becoming a favorable answer. Reference vectors that make the meaning executable, not a measured change in a hive.
The audit
| Challenge | Outcome |
|---|---|
| A fresh mass-calibration casetests the numbers on a new input | exact expected endpoints |
| A raw count changed without re-bindingtests that evidence belongs to its record | rejected |
| The installation changedtests identity consistency | rejected |
| A vacuous stand-in for the thermal modeltests that the proof still says what science needs | compiles, then the detector rejects it |
| Fifteen policy checks and a promotion mutanttests that scope cannot be inflated | checks pass, mutant exposed |
06 · Beyond the hive
Toward verifiable sensor data for science and AI.
The hive is where the contracts were first built. Our research report carries the same discipline to 3D capture, and to the point where scientific and AI systems take data in.
the case study
A beautiful model, a hidden error
A six-position room capture produced convincing panoramas and point clouds, yet a soft reconstruction. The cause: an assumed camera-rig model disagreed with the images themselves by about 116 degrees. The picture looked right; the evidence said otherwise.
the ingestion boundary
Accept, refuse, or unverified
Each claim travels with its observation identity, measurement meaning, transformation, evidence and execution context. It is accepted only within its declared scope; otherwise it is refused or kept unverified, never silently promoted.
four propositions
The contracts, made precise
Conditional composition; calibrated range enclosures; geometric error propagation, ‖p − p̂‖ ≤ εt + εr + r̂εu + r̂εR; and when another sensor actually adds information, ker C = ker A ∩ ker B.
07 · Who it serves
Every field that runs on readings.
The installation and physics change from hive to greenhouse to factory; the evidence contract carries over. Here is what it gives each community today, and what the next rounds add.
Pollinator & agricultural science
Compare hives, seasons and farms with readings whose meaning survives the trip.
- Today
- Readings carry their equipment, installation, calibration and model, and a study decides fitness with reasons.
- Next
- A characterized field protocol and a hive–weather pilot tested on held-out periods.
Climate & nature data (dMRV)
Environmental measurements that markets, policy and science can trust without re-collecting them.
- Today
- Every computed result is bound to its record and refuses to be promoted past its evidence.
- Next
- Exports alongside PROV and RO-Crate, with round-trip checks for anything lost in packaging.
AI data & governance
Know which observations entered a training set, which were excluded, and under which calibration.
- Today
- Admission, exclusion and calibration revision are explicit, inspectable decisions per record.
- Next
- Data-selection policies with their exclusion reasons and missingness carried into the dataset.
Instrument makers
Show what a sensor’s readings can and cannot support, in a form customers can check.
- Today
- Calibration and response are modeled contracts with enclosures that reach their worst cases.
- Next
- Controlled characterization against reference instruments, published with its residuals.
Metrology & demanding environments
Measurement chains that stay traceable as they cross equipment and organizations.
- Today
- Identity, numerical meaning and physical evidence are kept as separate, inspectable layers.
- Next
- A bounded pilot in environmental monitoring, test instrumentation or platform maintenance.
Formal methods & applied category theory
A real measurement problem where composition must preserve meaning, not just types.
- Today
- Concrete stage contracts and composition proofs in safe Agda, extracted to native code.
- Next
- Shared-uncertainty composition and a categorical interface whose laws are actually proved.
08 · The development record
From reference vectors to the field.
The next decisive experiment closes one loop: a physical response model, a real observation, an inferred constraint on the hive, and a prediction tested on data the model never saw.
- 01
Apiary measurement corein development
Readings that carry their argument.
An exact-rational Agda core with five measurement contracts, record-bound processing chains, aggregates and purpose-relative decisions, compiled through MAlonzo, with an offline dashboard and a local adversarial audit. Local validation is complete for its scope; authoritative acceptance stopped at 23 of 66 checks and is being completed.
To be complete
The full candidate accepted by the authoritative checker, with every contract, chain and audit result reproduced.
Adds to this page
- The five contracts
- The reference outcomes and the substitution audit
- 02
Verifiable Sensor Data reportcomplete · 2026-11-02
From a camera’s mistake to a framework.
A 3D-reconstruction case study (a 116-degree disagreement between an assumed camera-rig model and the images themselves), a proposed ingestion boundary that accepts, refuses or leaves a claim unverified, and four propositions that make the contracts precise.
Its gate
Published as a research technical report with every result’s status and scope stated.
On this page
- The camera case and the ingestion record
- The report, to read
- 03
Instrument characterizationnext on the bench
Meet the actual probe.
A controlled thermal experiment: a specified probe and placement compared with a reference instrument, its response coefficient and residuals fitted on some trajectories and tested on others.
To be complete
A residual bound that holds on held-out trajectories, or an investigation of the assumption that failed.
Adds to this page
- The probe’s measured response, beside the model
- Held-out residuals, failures included
- 04
Inference in Agdaplanned
From the reading back to the world, proved.
The inverse enclosure, from a probe’s readings to the environments that could have produced them, formalized with the strict condition a < 1 and an honest unresolved state at a = 1.
To be complete
A checked inverse theorem that preserves feasibility status, registered before it is described as implemented.
Adds to this page
- The checked inverse, replacing the illustration above
- 05
Hive–weather pilotplanned
The hive and the sky, in one model.
Couple a bounded hive heat model to weather inputs through an explicit shared interface, and compare direct use of readings with the characterized observation model on held-out periods.
To be complete
Predeclared coverage, width and failure-detection criteria met on held-out data, with weather-data dependencies preserved.
Adds to this page
- The pilot’s held-out comparison
- 06
Independent reuseplanned
Handed to another research group.
An independent group reconstructs the argument from the raw observations and supplied models: what was measured, an enclosure reproduced, a substituted installation detected.
To be complete
A reuse study by researchers outside the project, with the questions they could and could not resolve.
Adds to this page
- The independent reuse report
An Institute project
Brumble Bee Farmsresearch apiary · live camerasHelp a hive become a reference for science.
The next steps are concrete: a reference instrument for a characterization run, hive scales and probes placed by protocol, field compute and storage for the record, and partners in metrology, agriscience and formal methods. Every contribution becomes a named capability, and every result is published with its evidence.