The FM-1 is a pocket keyboard with a 240-pixel screen, seven knobs and a speaker. This firmware gives it four lanes. Each divides the clock into a rhythm (Euclidean patterns, cellular automata, ratchets) and picks notes from a scale (random walks, Markov chains, grammars, Tonnetz chord walks). The voices are all 48 Braids shapes, a four-operator FM voice and an 808, each through a filter, with a reverb and a ping-pong delay on sends. 142 patches to start from, 17 of them demo songs. Alfred bows at boot and stands in the corner when you stop the clock.
The lanes, the voices' arithmetic, the effects, the mix and the patch format are Lean 4, compiled to C and then to the chip. 315 theorems about that code go through Lean's kernel on every build. What is trusted (the screen, the drivers, the loops that call the Lean, Braids' tables, Lean's C backend, JieLi's clang and the runtime) is listed in the README.
Try it in the browser Install on an FM-1
The simulator is the same firmware compiled to WebAssembly. Chrome or Edge for MIDI in.
78 seconds: one song from four patches, played by four runs of the firmware.
Each link opens the simulator on a demo song; press Power on.
Rhythm
A lane's bar is Euclidean by default: 1 to 32 steps, hits spread as evenly as possible, at any of eight
clock divisions. Or a rotated bar with accents, a cellular automaton, ratchets. A lane's position in its
bar depends only on the tick count, so four lanes at four speeds stay in phase
(run_clock_never_drifts), and at play chance 100 a bar plays exactly the hits you set
(run_bar_plays_every_hit); below 100 it never plays a rest (lane_note_only_on_hit).
Notes
Eleven note sources, among them a random draw, walks, a mutating loop, a Turing register, a Markov chain
that learns from the keys, and a grammar. Chord progressions are written as degrees; a lane can follow the
chord, its
seventh, or the notes outside the key. The last three progressions walk the Tonnetz by P, L and R. The note
that comes out is always in the scale (lane_note_in_scale).
Sound
255 sounds: Braids' analog, digital, physical, percussion, vowel, wavetable and noise engines, eight FM shapes, ten 808 drums, each with an envelope and a filter. Every lane has an LFO. The keys have an arpeggiator, a scale or chord quantizer, and a page of punch-in effects. The reverb and the delay are sends.
Each group button opens its pages; the same button again moves to the next page. The four knobs set the four values on screen.
| Group | Pages |
|---|---|
| HOME | the four lanes: hits, steps, speed, chance; Alfred when stopped |
| SEQ | RHYTHM, FEEL, NOTES, RANGE |
| EDIT | SOUND, FILTER, ENVELOPE, MIX, PAN |
| FX | REVERB (send, decay, bright, return), DELAY (time, feedback, tone, return) |
| LFO | target, rate, depth, for the chosen lane |
| ARP | mode, rate, octaves, gate; ARP again latches; then QUANT |
| REC | PUNCH: the keys as momentary effects on the mix |
| GLO | HARMONY, SYSTEM, MIDI, BANKS |
| SELECT | the lane; in a browser, the group |
| PRESETS | the sound or patch browser |
| ALGORITHM | tempo |
| PLAY · SEL · SAVE | start or stop; mute the lane; save the patch |
315 theorems on the three standard axioms, checked by Lean's kernel and by
lake comparator, and each run on concrete inputs too.
| Area | Theorems | What is promised |
|---|---|---|
| The sequencer | 106 | The four lanes. No note is left sounding when you stop, the lanes stay in phase, at play chance 100 a bar plays exactly the hits set and never a rest below it, and every note is in the scale and the range. |
| The voices | 133 | Braids' engines in Lean, the FM voice, the 808 and the filter. Table reads stay inside their tables, the shipped tables meet what the proofs assume, and a sample is the arithmetic clipped, not wrapped, except where Braids itself overflows (docs/LEAN-ENGINES.md). |
| Setting a voice up | 42 | Per-note and per-block setup: parameters land in range, smoothing does not overshoot, table reads are in bounds. |
| The mix and the effects | 28 | The mix does not wrap, the reverb and delay stay inside their lines, their gains are below one so tails die away, and their filters do not overshoot. |
| Patches | 6 | A saved patch loads back as saved, anything else in a slot is rejected, and every factory patch is in range. |
Every theorem is in docs/PROOFS.md with its statement, why it matters and the definitions it depends on. The README lists what is trusted: the screen, the drivers, the accessors that read Braids' tables, and the C loops that call the Lean. The proofs are about the Lean the chip's code is compiled from (Lean's C backend and JieLi's clang are trusted); the engine arithmetic is also checked sample for sample against the original Braids.