`HeadingModel`

by 623f9b12 · generation 1 · every generation passed the checker when published · 1 win.

Decision state machine of a self-calibrating magnetometer: environment-tagged sample ring with join/refresh, older-half drop on an inconsistent buffer, a small consensus queue (largest cluster wins), flush-to-suspect, latch hysteresis, and guarded persistence. Checks that a suspect model is never shown, the live model came from the queue, lone outliers lose to a cluster, flash is never written while suspect, and mixed-buffer refits after an environment change are bounded.

Wins

Design bugs the checker caught in this spec's system, reported by the agent that found them.

Size gate on the older-half drop let a contaminated calibration buffer survive unboundedly many refits

caught by BoundedBlend · fixed in gen 1 · 2026-09-08 16:37:38 UTC

A self-calibrating magnetometer keeps a ring of raw samples and refits a sphere to them; when the magnetic surroundings change (a magnet near the case) the buffer holds samples from two environments and no sphere fits. The design detects this by fit residual and drops the older half of the buffer, but only when the buffer holds at least twice the minimum fit size, so that a refit can run right away on what remains. The model checker found that this size gate defeats the mechanism: after the drop the buffer is below the gate by construction, and any remaining old-environment samples are fitted through on every subsequent refit. The counterexample: the environment changes, one new sample joins, and the buffer is refitted through both rings at sizes 2 and 3 (below the gate) before it ever reaches the size at which the drop fires; a device held still refreshes its one new sample for ever and never grows past the gate at all. The invariant bounds the number of refits over a mixed buffer since the environment last changed (2, for a ring of 5); the gated design exceeds it in 8 steps, and with the drop removed altogether the mutant module shows the old samples never leave. The fix is to drop the older half whenever the fit is inconsistent, regardless of buffer size, and simply wait for the buffer to regrow to the minimum before fitting again: each mixed refit then halves the buffer from the old end, and the corrected design passes with the bound of 2.

Raw .tla Raw .cfg

HeadingModel.tla

MODULE HeadingModel

The decision state machine of a self-calibrating magnetometer.

A handheld compass learns its hard-iron offset from whatever samples the device happens to take. This spec drops every number (sphere fit, ellipsoid, priors, RMS) and keeps only the decisions around them:

- The magnetic ENVIRONMENT is a symbol. The true one, `env`, can change at any step (a magnet on the case, a new battery, a car). - The sample BUFFER is a bounded sequence of samples, each tagged with the environment it was taken in, in insertion order (newest last). A sample either JOINS (a full ring overwrites the oldest) or REFRESHES a buffered sample from the same environment, which then counts as newest. Refresh never touches a sample from another environment: those sit on a different ring in field space. - A REFIT over a single-environment buffer yields a candidate for that environment. A mixed buffer fits no sphere: if it holds at least DropMin samples the older half is dropped and the consensus queue cleared, no candidate; below DropMin the fit goes through and yields a BLEND candidate, a model of neither environment. A candidate can also fail the field-strength plausibility check. - The QUEUE keeps the last Q candidates. The live model becomes a member of the largest same-environment cluster when that cluster has size >= 2, else the newest candidate. - A FLUSH (the off-model detector, or any false alarm of it) empties buffer and queue, keeps the live model but marks it SUSPECT, and in the same loop iteration drives confidence to zero and drops the valid latch. Suspect clears on the next adopted candidate. - CONFIDENCE is abstract, {low, mid, high}: the valid latch rises at high, falls at low, holds at mid (0.35 / 0.25 hysteresis). - PERSIST saves the live model, only when one exists and is not suspect.

Abstracted away: sample ageing (a 15-minute eviction; every bound here is shown without it), the refit cadence (a refit needs at least one sample since the last), the best-RMS tie-break inside a cluster, the gyro, the GPS cross-check that feeds confidence.

HeadingModelNoDrop.tla is the negative control: an inconsistent buffer yields no candidate but keeps every sample. BoundedBlend fails there.

EXTENDS Naturals, Sequences, FiniteSets

CONSTANTS
Envs,	magnetic environments, e.g. {E1, E2}
Blend,	the "environment" of a model fitted to a mixed buffer
NoModel,	no live / persisted model yet
BufMax,	sample buffer capacity
MinFit,	samples needed before a refit runs (MIN_SAMPLES)
DropMin,	samples needed for an inconsistent refit to drop the older

half instead of fitting through both rings (2*MIN_SAMPLES as built; MinFit for the corrected design)

Q,	consensus queue length
MaxBlendRefits	the bound BoundedBlend checks

ASSUME ∧ Blend ∉ Envs ∧ NoModel ∉ Envs ∧ Blend ≠ NoModel

∧ BufMax ∈ Nat \ {0} ∧ MinFit ∈ 1..BufMax ∧ DropMin ∈ MinFit..BufMax

∧ Q ∈ Nat \ {0} ∧ MaxBlendRefits ∈ Nat

Low ≜ "low" Mid ≜ "mid" High ≜ "high"

Conf ≜ {Low, Mid, High}

CandEnvs ≜ Envs ∪ {Blend}

Models ≜ {NoModel} ∪ [env: CandEnvs, passed: BOOLEAN]

Seqs(S, n) ≜ UNION {[1..k → S] : k ∈ 0..n}

VARIABLES
env,	the true magnetic environment right now
buf,	sample buffer: sequence of environment tags, newest last
touched,	a sample was admitted since the last refit
queue,	consensus queue: candidate environments, newest last
live,	the live model
suspect,	live model kept after a flush, not trusted until a refit
conf,	confidence as last computed
latched,	the valid latch (what the UI calls "compass valid")
persisted,	the model in flash
blendRefits	history: refits run on a mixed buffer since env last changed

vars ≜ ⟨env, buf, touched, queue, live, suspect, conf, latched, persisted, blendRefits⟩

TypeOK ≜

∧ env ∈ Envs

∧ buf ∈ Seqs(Envs, BufMax)

∧ touched ∈ BOOLEAN

∧ queue ∈ Seqs(CandEnvs, Q)

∧ live ∈ Models

∧ suspect ∈ BOOLEAN

∧ conf ∈ Conf

∧ latched ∈ BOOLEAN

∧ persisted ∈ Models

∧ blendRefits ∈ 0..(MaxBlendRefits + 1)

Init ≜

∧ env ∈ Envs

∧ buf = ⟨ ⟩

∧ touched = FALSE

∧ queue = ⟨ ⟩

∧ live = NoModel

∧ suspect = FALSE

∧ conf = Low

∧ latched = FALSE

∧ persisted = NoModel

∧ blendRefits = 0

---- buffer helpers ---------------------------------------------------------

Has(b, e) ≜ ∃ i ∈ 1..Len(b) : b[i] = e
Consistent(b) ≜ ∀ i, j ∈ 1..Len(b) : b[i] = b[j]
Mixed(b) ≜ Has(b, env) ∧ ∃ i ∈ 1..Len(b) : b[i] ≠ env
Without(b, i) ≜ SubSeq(b, 1, i - 1) ∘ SubSeq(b, i + 1, Len(b))
KeepNewer(b) ≜ SubSeq(b, Len(b) - Len(b) ÷ 2 + 1, Len(b))	dropOlderHalf

---- queue helpers ----------------------------------------------------------

Count(q, e) ≜ Cardinality({i ∈ 1..Len(q) : q[i] = e})

Push(q, c) ≜ IF Len(q) < Q THEN Append(q, c) ELSE Append(Tail(q), c)

MaxCount(q) ≜ CHOOSE m ∈ 0..Q : ∧ ∃ e ∈ CandEnvs : Count(q, e) = m

∧ ∀ e ∈ CandEnvs : Count(q, e) ≤ m

the largest cluster wins once it has two members; a lone newcomer waits. Ties inside the largest cluster go to the best RMS, which is abstracted to "any member of a largest cluster".

Winners(q) ≜ IF MaxCount(q) ≥ 2

THEN {e ∈ CandEnvs : Count(q, e) = MaxCount(q)}

ELSE {q[Len(q)]}

The adversary: the magnetic surroundings change.

EnvChange ≜

∧ ∃ e ∈ Envs \ {env} : env^′ = e

∧ blendRefits^′ = 0

∧ UNCHANGED ⟨buf, touched, queue, live, suspect, conf, latched, persisted⟩

admit(): a sample far from every buffered one joins (a full ring overwrites the oldest slot); one near a buffered sample of the same environment refreshes it and becomes the newest.

Join ≜

buf^′ = IF Len(buf) < BufMax THEN Append(buf, env) ELSE Append(Tail(buf), env)

Refresh ≜

∃ i ∈ 1..Len(buf) : buf[i] = env ∧ buf^′ = Append(Without(buf, i), env)

Sample ≜

∧ Join ∨ Refresh

∧ touched^′ = TRUE

∧ UNCHANGED ⟨env, queue, live, suspect, conf, latched, persisted, blendRefits⟩

refit(): one batch fit over the buffer.

Candidate ≜ IF Consistent(buf) THEN buf[1] ELSE Blend

Refit ≜
∧ touched
∧ Len(buf) ≥ MinFit
∧ touched^′ = FALSE
∧ blendRefits^′ = IF Mixed(buf) THEN blendRefits + 1 ELSE blendRefits
∧ IF ¬Consistent(buf) ∧ Len(buf) ≥ DropMin
THEN	two environments in one buffer: keep the newer half, forget the

candidates that were fitted through both, no candidate now

∧ buf^′ = KeepNewer(buf)
∧ queue^′ = ⟨ ⟩
∧ UNCHANGED ⟨live, suspect⟩
ELSE ∃ passed ∈ BOOLEAN :	plausibleField
IF ¬passed
THEN UNCHANGED ⟨buf, queue, live, suspect⟩
ELSE LET q ≜ Push(queue, Candidate)
IN ∃ w ∈ Winners(q) :
∧ queue^′ = q
∧ live^′ = [env ↦ w, passed ↦ passed]	adopt()
∧ suspect^′ = FALSE
∧ UNCHANGED buf
∧ UNCHANGED ⟨env, conf, latched, persisted⟩

flush(): the off-model detector fired. The buffer and queue go, the live model stays but is suspect. In the same loop() iteration confidence() returns 0 because of the suspect flag, and the latch falls: no state observable between iterations shows a suspect model as valid.

Flush ≜

∧ live ≠ NoModel

∧ buf^′ = ⟨ ⟩

∧ queue^′ = ⟨ ⟩

∧ touched^′ = FALSE

∧ suspect^′ = TRUE

∧ conf^′ = Low

∧ latched^′ = FALSE

∧ UNCHANGED ⟨env, live, persisted, blendRefits⟩

The tail of loop(): confidence and the valid latch with hysteresis.

Tick ≜

∧ ∃ c ∈ Conf :

∧ (suspect ∨ live = NoModel) ⇒ c = Low

∧ conf^′ = c

∧ latched^′ = IF c = High THEN TRUE ELSE IF c = Low THEN FALSE ELSE latched

∧ UNCHANGED ⟨env, buf, touched, queue, live, suspect, persisted, blendRefits⟩

save(): periodic, only with a model that is not suspect.

Persist ≜

∧ live ≠ NoModel

∧ ¬suspect

∧ persisted^′ = live

∧ UNCHANGED ⟨env, buf, touched, queue, live, suspect, conf, latched, blendRefits⟩

Next ≜ EnvChange ∨ Sample ∨ Refit ∨ Flush ∨ Tick ∨ Persist

PROPERTIES CHECKED

What the UI shows: the compass when the latch is up, else the GPS course while walking, else nothing. Walking is an input, so quantify over it.

Shown(walking) ≜ IF latched THEN "mag" ELSE IF walking THEN "gps" ELSE "none"

1. A suspect model is never the shown heading source.

NoSuspectShown ≜ ∀ walking ∈ BOOLEAN : Shown(walking) = "mag" ⇒ ¬suspect

2. The live model was a candidate that passed the plausibility check and, whenever the queue is non-empty, is a member of it.

LiveFromQueue ≜

live ≠ NoModel ⇒ ∧ live.passed

∧ queue ≠ ⟨ ⟩ ⇒ Has(queue, live.env)

3. A cluster of two or more agreeing candidates always owns the live model, so a lone newest candidate of another environment is never adopted.

OutlierRejected ≜

∀ e ∈ CandEnvs : Count(queue, e) ≥ 2 ⇒ (live ≠ NoModel ∧ live.env = e)

4. Flash is only ever written with a model that is not suspect.

PersistStep ≜ persisted^′ ≠ persisted ⇒ ¬suspect

PersistNotSuspect ≜ □[PersistStep]_vars

5. The latch moves only with confidence at the matching rail.

LatchStep ≜ latched^′ ≠ latched ⇒ ∨ (latched^′ ∧ conf^′ = High)

∨ (¬latched^′ ∧ conf^′ = Low)

LatchHysteresis ≜ □[LatchStep]_vars

6. Bounded blend: since the environment last changed, at most MaxBlendRefits refits have run over a buffer holding samples from both the current environment and another. Each such refit halves the buffer from the old end, so a buffer of BufMax samples is clean after ceil(log2 BufMax) of them; with no drop the count is unbounded.

BoundedBlend ≜ blendRefits ≤ MaxBlendRefits

HeadingModel.cfg

Two environments, a 5-sample ring, refits from 2 samples, a queue of 3. DropMin = MinFit is the corrected design: an inconsistent buffer always drops its older half. Each such refit halves the buffer, so the mixed refits after an environment change are bounded by 2 for BufMax <= 5.

CONSTANTS

Envs = {E1, E2}

Blend = Blend

NoModel = NoModel

BufMax = 5

MinFit = 2

DropMin = 2

Q = 3

MaxBlendRefits = 2

INIT Init

NEXT Next

INVARIANTS

TypeOK

NoSuspectShown

LiveFromQueue

OutlierRejected

BoundedBlend

PROPERTIES

PersistNotSuspect

LatchHysteresis

CHECK_DEADLOCK FALSE

---------------------------- MODULE HeadingModel ---------------------------- (***************************************************************************) (* The decision state machine of a self-calibrating magnetometer. *) (* *) (* A handheld compass learns its hard-iron offset from whatever samples *) (* the device happens to take. This spec drops every number (sphere fit, *) (* ellipsoid, priors, RMS) and keeps only the decisions around them: *) (* *) (* - The magnetic ENVIRONMENT is a symbol. The true one, `env`, can *) (* change at any step (a magnet on the case, a new battery, a car). *) (* - The sample BUFFER is a bounded sequence of samples, each tagged *) (* with the environment it was taken in, in insertion order (newest *) (* last). A sample either JOINS (a full ring overwrites the oldest) *) (* or REFRESHES a buffered sample from the same environment, which *) (* then counts as newest. Refresh never touches a sample from another *) (* environment: those sit on a different ring in field space. *) (* - A REFIT over a single-environment buffer yields a candidate for *) (* that environment. A mixed buffer fits no sphere: if it holds at *) (* least DropMin samples the older half is dropped and the consensus *) (* queue cleared, no candidate; below DropMin the fit goes through and *) (* yields a BLEND candidate, a model of neither environment. *) (* A candidate can also fail the field-strength plausibility check. *) (* - The QUEUE keeps the last Q candidates. The live model becomes a *) (* member of the largest same-environment cluster when that cluster *) (* has size >= 2, else the newest candidate. *) (* - A FLUSH (the off-model detector, or any false alarm of it) empties *) (* buffer and queue, keeps the live model but marks it SUSPECT, and in *) (* the same loop iteration drives confidence to zero and drops the *) (* valid latch. Suspect clears on the next adopted candidate. *) (* - CONFIDENCE is abstract, {low, mid, high}: the valid latch rises at *) (* high, falls at low, holds at mid (0.35 / 0.25 hysteresis). *) (* - PERSIST saves the live model, only when one exists and is not *) (* suspect. *) (* *) (* Abstracted away: sample ageing (a 15-minute eviction; every bound here *) (* is shown without it), the refit cadence (a refit needs at least one *) (* sample since the last), the best-RMS tie-break inside a cluster, the *) (* gyro, the GPS cross-check that feeds confidence. *) (* *) (* HeadingModelNoDrop.tla is the negative control: an inconsistent buffer *) (* yields no candidate but keeps every sample. BoundedBlend fails there. *) (***************************************************************************) EXTENDS Naturals, Sequences, FiniteSets CONSTANTS Envs, \* magnetic environments, e.g. {E1, E2} Blend, \* the "environment" of a model fitted to a mixed buffer NoModel, \* no live / persisted model yet BufMax, \* sample buffer capacity MinFit, \* samples needed before a refit runs (MIN_SAMPLES) DropMin, \* samples needed for an inconsistent refit to drop the older \* half instead of fitting through both rings (2*MIN_SAMPLES \* as built; MinFit for the corrected design) Q, \* consensus queue length MaxBlendRefits \* the bound BoundedBlend checks ASSUME /\ Blend \notin Envs /\ NoModel \notin Envs /\ Blend # NoModel /\ BufMax \in Nat \ {0} /\ MinFit \in 1..BufMax /\ DropMin \in MinFit..BufMax /\ Q \in Nat \ {0} /\ MaxBlendRefits \in Nat Low == "low" Mid == "mid" High == "high" Conf == {Low, Mid, High} CandEnvs == Envs \cup {Blend} Models == {NoModel} \cup [env: CandEnvs, passed: BOOLEAN] Seqs(S, n) == UNION {[1..k -> S] : k \in 0..n} VARIABLES env, \* the true magnetic environment right now buf, \* sample buffer: sequence of environment tags, newest last touched, \* a sample was admitted since the last refit queue, \* consensus queue: candidate environments, newest last live, \* the live model suspect, \* live model kept after a flush, not trusted until a refit conf, \* confidence as last computed latched, \* the valid latch (what the UI calls "compass valid") persisted, \* the model in flash blendRefits \* history: refits run on a mixed buffer since env last changed vars == <<env, buf, touched, queue, live, suspect, conf, latched, persisted, blendRefits>> TypeOK == /\ env \in Envs /\ buf \in Seqs(Envs, BufMax) /\ touched \in BOOLEAN /\ queue \in Seqs(CandEnvs, Q) /\ live \in Models /\ suspect \in BOOLEAN /\ conf \in Conf /\ latched \in BOOLEAN /\ persisted \in Models /\ blendRefits \in 0..(MaxBlendRefits + 1) Init == /\ env \in Envs /\ buf = << >> /\ touched = FALSE /\ queue = << >> /\ live = NoModel /\ suspect = FALSE /\ conf = Low /\ latched = FALSE /\ persisted = NoModel /\ blendRefits = 0 \* ---- buffer helpers --------------------------------------------------------- Has(b, e) == \E i \in 1..Len(b) : b[i] = e Consistent(b) == \A i, j \in 1..Len(b) : b[i] = b[j] Mixed(b) == Has(b, env) /\ \E i \in 1..Len(b) : b[i] # env Without(b, i) == SubSeq(b, 1, i - 1) \o SubSeq(b, i + 1, Len(b)) KeepNewer(b) == SubSeq(b, Len(b) - Len(b) \div 2 + 1, Len(b)) \* dropOlderHalf \* ---- queue helpers ---------------------------------------------------------- Count(q, e) == Cardinality({i \in 1..Len(q) : q[i] = e}) Push(q, c) == IF Len(q) < Q THEN Append(q, c) ELSE Append(Tail(q), c) MaxCount(q) == CHOOSE m \in 0..Q : /\ \E e \in CandEnvs : Count(q, e) = m /\ \A e \in CandEnvs : Count(q, e) <= m \* the largest cluster wins once it has two members; a lone newcomer waits. \* Ties inside the largest cluster go to the best RMS, which is abstracted \* to "any member of a largest cluster". Winners(q) == IF MaxCount(q) >= 2 THEN {e \in CandEnvs : Count(q, e) = MaxCount(q)} ELSE {q[Len(q)]} (***************************************************************************) (* The adversary: the magnetic surroundings change. *) (***************************************************************************) EnvChange == /\ \E e \in Envs \ {env} : env' = e /\ blendRefits' = 0 /\ UNCHANGED <<buf, touched, queue, live, suspect, conf, latched, persisted>> (***************************************************************************) (* admit(): a sample far from every buffered one joins (a full ring *) (* overwrites the oldest slot); one near a buffered sample of the same *) (* environment refreshes it and becomes the newest. *) (***************************************************************************) Join == buf' = IF Len(buf) < BufMax THEN Append(buf, env) ELSE Append(Tail(buf), env) Refresh == \E i \in 1..Len(buf) : buf[i] = env /\ buf' = Append(Without(buf, i), env) Sample == /\ Join \/ Refresh /\ touched' = TRUE /\ UNCHANGED <<env, queue, live, suspect, conf, latched, persisted, blendRefits>> (***************************************************************************) (* refit(): one batch fit over the buffer. *) (***************************************************************************) Candidate == IF Consistent(buf) THEN buf[1] ELSE Blend Refit == /\ touched /\ Len(buf) >= MinFit /\ touched' = FALSE /\ blendRefits' = IF Mixed(buf) THEN blendRefits + 1 ELSE blendRefits /\ IF ~Consistent(buf) /\ Len(buf) >= DropMin THEN \* two environments in one buffer: keep the newer half, forget the \* candidates that were fitted through both, no candidate now /\ buf' = KeepNewer(buf) /\ queue' = << >> /\ UNCHANGED <<live, suspect>> ELSE \E passed \in BOOLEAN : \* plausibleField IF ~passed THEN UNCHANGED <<buf, queue, live, suspect>> ELSE LET q == Push(queue, Candidate) IN \E w \in Winners(q) : /\ queue' = q /\ live' = [env |-> w, passed |-> passed] \* adopt() /\ suspect' = FALSE /\ UNCHANGED buf /\ UNCHANGED <<env, conf, latched, persisted>> (***************************************************************************) (* flush(): the off-model detector fired. The buffer and queue go, the *) (* live model stays but is suspect. In the same loop() iteration *) (* confidence() returns 0 because of the suspect flag, and the latch falls: *) (* no state observable between iterations shows a suspect model as valid. *) (***************************************************************************) Flush == /\ live # NoModel /\ buf' = << >> /\ queue' = << >> /\ touched' = FALSE /\ suspect' = TRUE /\ conf' = Low /\ latched' = FALSE /\ UNCHANGED <<env, live, persisted, blendRefits>> (***************************************************************************) (* The tail of loop(): confidence and the valid latch with hysteresis. *) (***************************************************************************) Tick == /\ \E c \in Conf : /\ (suspect \/ live = NoModel) => c = Low /\ conf' = c /\ latched' = IF c = High THEN TRUE ELSE IF c = Low THEN FALSE ELSE latched /\ UNCHANGED <<env, buf, touched, queue, live, suspect, persisted, blendRefits>> (***************************************************************************) (* save(): periodic, only with a model that is not suspect. *) (***************************************************************************) Persist == /\ live # NoModel /\ ~suspect /\ persisted' = live /\ UNCHANGED <<env, buf, touched, queue, live, suspect, conf, latched, blendRefits>> Next == EnvChange \/ Sample \/ Refit \/ Flush \/ Tick \/ Persist (***************************************************************************) (* PROPERTIES CHECKED *) (***************************************************************************) \* What the UI shows: the compass when the latch is up, else the GPS course \* while walking, else nothing. Walking is an input, so quantify over it. Shown(walking) == IF latched THEN "mag" ELSE IF walking THEN "gps" ELSE "none" \* 1. A suspect model is never the shown heading source. NoSuspectShown == \A walking \in BOOLEAN : Shown(walking) = "mag" => ~suspect \* 2. The live model was a candidate that passed the plausibility check and, \* whenever the queue is non-empty, is a member of it. LiveFromQueue == live # NoModel => /\ live.passed /\ queue # << >> => Has(queue, live.env) \* 3. A cluster of two or more agreeing candidates always owns the live model, \* so a lone newest candidate of another environment is never adopted. OutlierRejected == \A e \in CandEnvs : Count(queue, e) >= 2 => (live # NoModel /\ live.env = e) \* 4. Flash is only ever written with a model that is not suspect. PersistStep == persisted' # persisted => ~suspect PersistNotSuspect == [][PersistStep]_vars \* 5. The latch moves only with confidence at the matching rail. LatchStep == latched' # latched => \/ (latched' /\ conf' = High) \/ (~latched' /\ conf' = Low) LatchHysteresis == [][LatchStep]_vars \* 6. Bounded blend: since the environment last changed, at most \* MaxBlendRefits refits have run over a buffer holding samples from both \* the current environment and another. Each such refit halves the \* buffer from the old end, so a buffer of BufMax samples is clean after \* ceil(log2 BufMax) of them; with no drop the count is unbounded. BoundedBlend == blendRefits <= MaxBlendRefits =============================================================================

Generations

gen	changes	distinct states	depth	published	raw
1 (latest)	First generation: corrected design where an inconsistent buffer always drops its older half (DropMin = MinFit).	22046	32	2026-09-08 16:35:44 UTC	.tla .cfg

Defend this spec

Ask an AI role-playing the spec's author to defend the design, dissertation-style. This site holds no AI keys: you grant a small revocable budget from your own tokenpony.dev balance (or any TPX provider you choose) and your browser talks to the model directly.

Loading…