REFERENCE
RECORDEDIdeal peripheral model
CORTEX-M4 → MMIO—Reviewed model
SPI transfer
TARGET RECEIVED
—bytes
—
Loading recorded events… DOCUMENTED DEFECTS → EXECUTABLE EVIDENCE
The same firmware.
A different outcome.
The driver returns success. The simulated SPI target receives an extra byte. Turn that documented chip defect into a regression you can rerun.
Errata Replay turns vendor errata into source-grounded contracts, then compares real ARM execution across nominal, affected and workaround models.
See the first divergenceNO BOARD REQUIREDACTUAL ARM FIRMWARE IN RENODEREVIEWED, REVISION-SCOPED MODELS
01 / THE REPLAYOne requested byte.
One requested byte.
One unexpected extra.
nRF52832 · Revision 3 · Anomaly 58
Unmodified nrfx v2.11.0 · recorded integration application
Recorded Renode execution · event order, not timing
FIRMWARE IDENTITY
Checking recorded ELF hashes…—AFFECTED BEHAVIOR
RECORDEDRevision 3 · anomaly 58
CORTEX-M4 → MMIO—Erratum enabled
SPI transfer
TARGET RECEIVED
—bytes
—
Loading recorded events…Loading a sanitized real execution record. No model or emulator runs in this browser.
Read the “?” literally. The extra byte’s value is unspecified. The model counts the transfer without inventing its content.
Recorded event evidence and ELF identities
| Step | Ideal model | Affected model |
|---|
02 / ACTUAL UPSTREAM DRIVERThe driver says success.
The driver says success.
The target says two.
An unmodified Nordic nrfx driver.
A synthetic bare-metal application.
A separately observed extra transfer.
NORDIC NRFX v2.11.0 · PINNED SOURCE
A successful API call does not count the bytes on the wire.
Our small application requests one receive byte and one transmit byte through Nordic’s blocking SPIM API. The upstream driver returns NRFX_SUCCESS in both recorded models. The independent target observes one byte in the ideal model and two in the affected model.
A separately built legacy SPI application uses the documented remedy and restores the target count to one.
Inspect the exact upstream driver ↗The driver source is unmodified. Application, startup and configuration are our integration. These are Renode observations from a synthetic reproducer; physical-board and customer-firmware claims are outside this evidence.
RECORDED APPLICATION + TARGET OBSERVATIONS
| Observation | Ideal SPIM | Affected SPIM | SPI remedy |
|---|---|---|---|
| Driver return | 0x0BAD0000NRFX_SUCCESS | 0x0BAD0000NRFX_SUCCESS | 0x0BAD0000NRFX_SUCCESS |
| Target transfers | 1 | 2 | 1 |
| Trigger events | 0 | 1 | 0 |
| Unsupported accesses | 0 | 0 | 0 |
NRFX SOURCE COMMIT
Download the driver-case receipt ↓2527e3c8449cfd38aee41598e8af8492f410ed15The interactive replay above uses these same recorded nrfx case traces and ELF identities. This full receipt adds source pins, boundary controls and explicitly labeled separate diagnostic runs. The run used an existing reviewed contract and made no fresh Meta request.
03 / FROM PROSE TO PROOFThe document is the start.
The document is the start.
Execution is the check.
The model extracts a claim.
The workbench checks what follows.
01 VENDOR DOCUMENTATION SOURCE ↗
A very small condition.
A very observable consequence.
For the affected nRF52832 revision, a one-byte SPIM receive with at most one transmitted byte clocks an extra byte.
RXD.MAXCNT = 1ANDTXD.MAXCNT ≤ 1Paraphrase of anomaly 58. Scope: revision 3, builds QFAA-Gx0, QFAB-Gx0 and CIAA-Gx0. The implemented remedy selects legacy SPI.
02 META MODEL API → TYPED CONTRACT
// Readable projection of the reviewed contract
{
"device": "nRF52832",
"revision": "3",
"anomaly": 58,
"when": {
"RXD.MAXCNT": { "eq": 1 },
"TXD.MAXCNT": { "lte": 1 }
},
"effect": "one extra SPI byte",
"workaround": "legacy SPI"
}Meta extracts scope, conditions, effects, remedies and exact evidence quotations. A deterministic gate checks the result against a human-reviewed adapter before execution.
03
Run the actual ELF
Cortex-M4 instructions execute in Renode. Nominal and affected comparisons preserve the exact firmware bytes.
04
Measure outside the driver
A separate SPI target records transfers. Boundary controls test whether the documented trigger was modeled too broadly.
05
Carry the evidence
Sources, exact ELFs, observations and file hashes travel together in a reproducible regression bundle.
04 / THREE DIFFERENT FAILURE MODES
More than a one-byte trick.
Saved end-to-end runs used Meta-extracted contracts
followed by actual Renode execution.
| Reviewed revision 3 adapter | What we observe | Ideal | Affected | Workaround |
|---|---|---|---|---|
| 58 / SPIMExtra transfer ↗ | SPI target transfers bytes | 1 | 2 | 1 |
| 15 / POWERRAM status aliases ↗ | RAM power-state readback register value | 3 | 0 | 3 |
| 55 / I2SEvents after STOP ↗ | Unexpected pointer updates accepted events | 0 | 2 | 0 |
8 boundary controls passed across these three saved runs. The affected assertion deliberately fails; reproduction, workaround and controls together establish the reviewed-model result.
Inspect recorded results ↓05 / TRUST THE BOUNDARIESA model you can inspect.
A model you can inspect.
A claim you can bound.
This page replays saved execution. The executable workbench runs the compiler, emulator, contract checks and evidence export locally.
Peripheral behavior is implemented in three human-reviewed, revision-scoped adapters. This prototype models transactions, registers and events. Physical silicon parity, cycle accuracy, analog behavior and arbitrary-chip generalization are outside its evidence.
A missing trigger, unsupported access or absent workaround stays inconclusive. No model-generated peripheral or host code is executed.
06 / REPRODUCE ITBring the proof
Bring the proof
to your own machine.
Linux x86-64 · Python 3.11+ · uv
Pinned Renode and Arm GNU toolchains.
No board or GPU required.
LOCAL WORKBENCH
uv sync --frozen
uv run python tools/bootstrap_engine.py
uv run errata-replay doctor
uv run errata-replay replay --fixture nrf52832-58
uv run python tools/service.py startRun from the executable workbench source directory. Human-authored reference fixtures run without a model key. Fresh Meta extraction requires your own server-side key.
Inspect before you execute.
The browser replay is a small, sanitized public record. The workbench source contains the executable adapters, firmware, checks and evidence format.
Inspect the public GitHub source ↗Download executable source ↓Source + replay evidence ↓Download SPI execution record View content provenance
Exact source checkpoint f1028e3. Packages include the pinned vendor-source reproducer and license notices; the evidence package also contains the uploaded-ELF comparison and verification receipts.
07 / THREE-MINUTE WALKTHROUGHWatch the result.
Watch the result.
Then inspect the evidence.
Recorded demonstration · 3 minutes
English captions · silent audio
Edited actual browser captures of saved execution. The replay uses event order, not hardware timing.
Download MP4 ↓Capture and video hashes ↗