The Dexcom G7 is the small white disc that sits on the back of the arm, reads blood sugar every five minutes, and alerts a phone when something is wrong. A pile of software already surrounds it: DexVal, GluCoPilot, a macOS menu bar icon that shows the current number. None of it writes down what the device is supposed to do. This TLA+ spec does.
It is one of three TLA+ specs, alongside the walk-in oven and laptop models. The interactive microwave spec is a friendlier on-ramp for a reader who has never used TLA+.
The G7 is a sensor plus a transmitter that lives on the arm for ten days. There is a 30-minute warmup after insertion, then it samples glucose every five minutes, transmits over BLE to a receiver (usually a phone), and the receiver decides whether to fire a high or low alert. After 10 days the sensor enters a 12-hour grace period and then expires.
g7.tla models all of that as a state machine. The state variables look like this:
VARIABLES
now, \* elapsed minutes since sensor insertion
sensorState, \* "NotInserted" | "Warmup" | "Active" | "Expired"
lastSample, \* most recent sample produced by the sensor
receiverStore, \* sequence of samples stored on the receiver
connected, \* BLE connection status
alerts \* { high: BOOL, low: BOOL }
The actions are the things the device can do: InsertSensor, FinishWarmup, ProduceSample, ConnectOrDisconnect, TransmitSample, UpdateAlerts, ClearAlerts, ExpireSensor, and a Tick that advances now by one minute. Transmission is nondeterministic, since packets can be delivered or dropped: in practice the phone is often in another room and the BLE link is unreliable.
There are two config files. g7.debug.cfg shrinks everything (lifetime 10 minutes, glucose values 80 to 82) so TLC can finish in a second. g7.realistic.cfg uses real numbers: 30-minute warmup, 10-day lifetime, 12-hour grace, glucose range 40 to 400. The realistic one explodes the state space.
The safety property that matters most is NoReadingsAfterExpiry:
NoReadingsAfterExpiry ==
\A i \in 1..Len(receiverStore) :
receiverStore[i].time <= LIFETIME_MINS + GRACE_MINS
In English: nothing should ever land in the receiver's store with a timestamp past the sensor's expiration. A stale or post-expiration reading is worse than useless. If the CGM reports 110 when the real value is 50, the wearer eats nothing, and a 50 with no alert is how diabetics end up in the ER. False-negative readings are the failure mode to design out, not the false positives.
Running TLC against the debug config catches this. The model surfaces a state where lastSample gets produced and stored after the sensor should have moved to Expired, because ExpireSensor and ProduceSample race on the same tick. That is the point of writing the spec: the invariant is not satisfied by the current model, and the trace says where to tighten it.
A lot. The spec does not model calibration (the G7 mostly does not need it, but the API surface still exists). It does not model the signal loss state when the transmitter and receiver are out of range for too long. It does not model the difference between the sensor producing a sample and the transmitter packaging it for BLE. Alerts are a single high/low flag instead of the hysteresis the device actually uses: Dexcom will not refire the low alert if the wearer is already in low territory and has not climbed back out. There is no model of the predictive "you'll be low in 20 minutes" alerts.