FORMALFRED

a sequencer for the M-VAVE FM-1 · written in Lean · 315 theorems about it

The FM-1's RHYTHM page: a bar of sixteen steps drawn as a circle, its seven hits joined

The FM-1

M-VAVE · $60 · JieLi AC7911B · 213 firmwares listed on 1 November

The M-VAVE FM-1: a black pocket keyboard with 27 keys, seven knobs and a small square screen

The FM-1 running Doom, a pen beside it for scale

photos: M-VAVE; Nick Indge, Ars Technica

Fart Machine One · "eleven artisanal farts on the keys, a reverb, a delay, and a 16-step sequencer"

"We're not even through October, and there are already more community firmware projects available to install on the FM-1 than I could ever hope to cover. And just in case you were wondering: yes, it plays Doom."

Ars Technica, 26 October 2026

the chip they all run on

JieLi AC7911B: integer core, no floating point, 1 MiB of flash run in place.
No debug header, no recovery button.

The others were written in weeks, in C, with an AI, for a chip with no debugger. So was this one, in Lean. 315 theorems about that Lean go through the kernel on every build.

The instrument

a generative sequencer, and why prove one

A generative sequencer with a modular synth's oscillator in a $60 keyboard, with 315 theorems about the promises it makes.

A Eurorack modular synthesizer; in its middle row a Mutable Instruments Braids with CSAW on its display

a Eurorack case; middle row, a Mutable Instruments Braids reading CSAW, the oscillator this firmware compiles from source. Photo Paul Anthony, CC BY-SA 4.0

what it is

Four lanes, each a rhythm (Euclidean by default) choosing its own notes.
Nothing written down: the rules are the song.
Braids (Mutable Instruments), an FM voice and an 808 kit, in Lean.
All integers: the chip has no floating point.

why prove any of this

Promises you can hear: in key, on the beat, nothing stuck.
A test plays some settings; a theorem holds at all of them.
Fixed-point bugs are silent until they are noise or a crash.
No debugger on the chip: prove it before flashing.
The rhythm is a Christoffel word; the chord walks are a group.

What it does

four lanes · Braids, FM, an 808 kit, a filter · two sends · the PUNCH page · seven looks

SEQ > NOTES: the Turing note source, its length, flip chance and range

the sequencer

Four lanes: hits, steps, speed, chance; the bar drawn as a circle.
FEEL: Euclid, rotated with accents, a cellular automaton, ratchets.
NOTES: random, walk, up, down, bounce, loop, Turing, step, Markov, grammar, chord.
HARMONY: key, scale lock, progressions as degrees, Tonnetz walks. Swing, MIDI in and out, external clock, arpeggiator, quantized keys.

EDIT > FILTER: cutoff, resonance, envelope amount and type of the chosen lane's sound

the engines

Braids, all 48 shapes: analog, filter, voice, FM, physical, percussion, wavetable, noise.
Four-operator FM voice in Lean: piano, bell, bass, brass, glass, mallet, organ, clang.
808 kit in Lean: kick, snare, clap, hats, toms, cowbell, cymbal.
Per-voice filter (low, band or high), opened by the envelope; in Lean, states proved in range.
Browser by engine or by type; per lane an envelope, an LFO, pan and level.

FX > REVERB: send, decay, bright and return

the effects

Clouds' reverb on a send: decay, brightness, return. Its tail is proved to die away.
Ping-pong delay on the same send: a note value at the song's tempo, feedback, tone.
Each lane sets its own send: one lane dry, another wet.

REC > PUNCH: the keys as effects, CRUSH, STUTTER and WASH lit

punch-in effects

REC makes the keys momentary effects on the whole mix, like the OP-XY's punch-in FX.
HALF and DOUBLE time, STUTTER, ROLL, octaves, SHIFT, GATE, CRUSH, WASH, THROW, BREAK, four mutes, four rolls.
Let go and it is gone: with no key held every effect is the identity, a theorem; the gate fades out in 1.5 ms.

Lean on the chip

Firmware/ → C → the FM-1 and the browser; Proofs/ about the Firmware

Check	What it establishes
Proved	315 theorems about the Lean the chip runs: sequencer, FM voice, 808, range and no-wrap facts about every Braids engine, reverb, delay, mix, patch format. Three standard axioms, nothing else.
The compiler, tested	354 exported functions compiled to C and run on random inputs; the kernel checks each value against the definition. 2124 values a run.
The proofs, watched	Twelve theorem statements asserted on the running firmware where the C takes the Lean's answer. Tens of millions of checks over the test run; the count and the failures (zero) are printed by `make test`.

trusted, listed in the README

What is left of Braids' C++, the per-block setup; the sample arithmetic is Lean, checked sample for sample against the original.
The C loops that call the Lean; the screen, the drivers, Dinghy's update path.
Lean's C backend, JieLi's clang, the 14 KB of C runtime, and the 39 accessors that read Braids' tables.

What is proved

315 theorems, in five kinds

Kind	Theorems	For example	What it is good for
The music it plays	84	`run_every_note_on_has_a_note_off` `run_clock_never_drifts` `run_bar_plays_every_hit`	Every note the lanes and the arpeggiator start gets its note-off, over a whole performance. A lane's step is a function of the tick count: notes cannot make lanes drift apart. At chance 100 a bar plays exactly the hits on the screen; never a rest. With QUANT on, the keyboard cannot leave the scale or the chord.
Music theory	22	`euclid_is_christoffel` `tonnetz_group_is_dihedral` `harmony_hexachord_theorem`	The rhythm is a Christoffel word: maximally even. The chord walks are the PLR group of order 24: they come home. A six-note set and its complement share their intervals (Babbitt): why BLACK KEYS sounds as it does.
Sound, in fixed point	175	`fm_sine_bounded` `drum_output_never_wraps` `filter_states_stay_bounded`	A proved sample is clipped, not wrapped (four places where Braids itself overflows are matched, not proved: LEAN-ENGINES.md). No oscillator runs past Nyquist. Every table index the Lean computes stays inside its table (two of Braids' own overruns are kept and listed). With no floating point, these bugs are noise or a crash screen.
The mix and the effects	28	`mix_bus_never_wraps` `reverb_tail_dies_away` `delay_echoes_die_away`	Six voices and two sends fit the mix without wrapping. With nothing fed in, reverb tail and echo die away at every knob setting: no howl.
Patches	6	`patch_decode_encode_round_trip` `patch_decode_only_fits` `presets_all_fit`	A saved patch loads back as saved. A foreign or corrupt flash slot is rejected whole, never read as settings. Every factory patch is in range of the tables it indexes.

The song

four presets playing at once, 78 seconds (P) · mpancia.github.io/fmfm · make install && make run

the film

formalfred.webm

P plays · R from the start