SoundfishSoundfish writes each promise about its behavior as one sentence and keeps the promises in one list. On 2026-09-24 the list held 72 promises, and all 72 were open. Two pieces of work are further along: proofs about how a loop is written to bytes, and models of how the synthesizer starts and stops sound.
Status: Beta.
Bugs that depend on order
Picture a bug of the kind these checks target. You press Stop, close the project, and a moment later a note you did not play rings out. Part of the audio engine was waiting on an answer, got it late, and acted on it. Nothing crashed. The bug appears only when a slow sound bank, a closed tab and a quick restart happen in one order out of thousands.
Much new software is written fast, more and more of it by models, and it looks finished on the first run. It breaks on the second use: the reload, the second tab, the file shared with a friend. Many apps rest on code nobody checked, and the failures that matter sit in orderings nobody tried.
"Verified" rarely tells a reader much. It usually means one checker passed on one piece of a product, and the reader cannot tell which piece or what was assumed. A written list of promises answers both questions. Next to each promise it names the kind of evidence it needs and what that evidence leaves out. When a promise is closed properly, a whole class of failure is ruled out within the stated assumptions, including the cases nobody remembered to test. An open promise is visible as open.
Seventy-two promises, none closed
Soundfish's verification overview opens with the count and the scope:
"The registry contains 72 open application claims: 59 original obligations, nine v2 workstation obligations and four evolution obligations. Its source and gate inventory is checked; the claims are not yet proved. The registered Lean modules cover legacy loop canonical text, document encoding, bounded decoding, byte budgets and identity definitions; six TLA+ models cover synthesizer lifecycle obligations."
On 2026-09-24 every one of the 72 entries was marked open. The project's tooling checks that each promise points at real code, real assumptions and a planned kind of evidence; it does not mark any promise as kept.
Proofs about the loop format
A Soundfish loop can travel as a link, so its bytes have to decode back to the same music every time. The proofs are written in Lean, a language where a theorem passes only if the proof checker accepts every step. On 2026-09-24 the project's list of formal checks registered 14 theorem modules and two small executable reference programs.
The central law is a round trip. Written for this article and simplified, it reads:
-- For every document that passes validation,
-- decoding its encoding gives back its normal form.
-- (Real name: Soundfish.CborBudget.canonical_document_roundtrip.)
theorem roundtrip (doc : Document) (valid : Valid doc) :
decode (encode doc) = some (normalize doc)
The real statement also proves the other direction: any byte string the decoder accepts re-encodes to the same bytes, so each loop has one spelling. Other theorems pin the limits that decide whether a loop fits in a link. A document may use up to 24,493 bytes. With the reviewed 110-character envelope around it, the proofs show that this comes to 32,768 characters of link fragment, and one more byte comes to 32,769.
A theorem is only about the definitions it states. The Lean definitions model the TypeScript code; they do not run it. A separate comparison feeds fixed cases to both: 126 cases against the proof's reference decoder, 203 against the shipped encoding code, 118 links between the two, and 29 cases of malformed framing. The overview labels this comparison as sampled evidence.
Models of starting and stopping sound
The synthesizer, described in Playing MIDI in the browser without a plugin, fails through the order of events. A sound bank loads while the listener leaves; one of two users cancels a shared loader; an acknowledgement arrives after the engine was torn down. For these, Soundfish writes models in TLA+ and runs TLC, a model checker that walks every reachable state of a small version of the system.
The six synthesizer models cover:
- sending commands to the audio engine one at a time, and cleaning up when the engine is destroyed mid-command;
- sharing a loader between two listeners, so one cancelling cannot stop the other;
- posting sound banks to the decoder in one fixed order snapshot, with a failed read blocking later dispatch;
- handing decoded samples to the audio thread at most once, and treating a load as done only after the audio thread acknowledges it or there were no samples;
- matching each completion message to the request that caused it;
- switching sound banks on only after the engine confirms they loaded.
An invariant is a sentence that must hold in every state the checker reaches. The command model's first safety invariant, quoted as written, says the engine never has two unanswered native commands at once:
AtMostOneOutstandingNative == Cardinality(dispatched \ settled) <= 1
"Every state" means every state of a finite instance. The command model runs with four commands and then five; the others have their own small sizes. Progress properties, such as "after destroy, the engine eventually closes", also assume that pending native events are eventually delivered, and the model guide lists each of those assumptions by the event it depends on. Recorded model runs are replayed against the real renderer code through controlled stand-ins for the browser.
A seventh model, a counter that wraps around, exists only to test the model-checking tooling.
Checks built to fail
A proof or model that checks nothing still passes. Soundfish guards against that in two ways.
First, each model carries deliberately false statements that name a state the model must be able to reach. The tooling model is small enough to show whole:
Next == x' = IF x = Max THEN 0 ELSE x + 1
NeverMax == x # Max \* must be violated
The checker is required to break NeverMax with a step-by-step trace. If someone later removes the step that reaches Max, the model has no failures, and the run fails because the expected trace is missing.
Second, planted bugs. Each synthesizer model has a switch that plants one known mistake, such as releasing an engine slot early or publishing sound banks before they are confirmed. Seven such planted bugs must each break their named property. The codec comparison has six planted production bugs and three planted proof bugs that must be caught at the intended check. A crash, a timeout or an unrelated failure does not count as catching one.
Limits
On 2026-09-24 the plan of record listed the loop-format proofs and the synthesizer models as pilots in progress, and proofs for the workstation had not started. The proofs cover the older loop format, not the workstation's project format. The models say nothing about real browser thread scheduling, audio worklet timing or what comes out of a speaker. The checks trust the pinned toolchain, Bun, the operating system and SHA-256.