A sequencer that plays by itself, with proofs.

Four lanes of Euclidean rhythm, each choosing its own notes, every one of the 48 Braids shapes, chord progressions, and a butler who bows. The sequencer and the voices are written in Lean 4, and what they promise is proved there.

Install the latest release · Try it in your browser · Source and proofs

• Four lanes

  Each one divides the clock into a Euclidean rhythm and then picks its notes by one of eleven algorithms, anything from a random draw to a Turing machine or a small grammar, inside a range and a scale you set.

• Every Braids shape

  The 48 oscillator shapes of Mutable Instruments' Braids are all here, arranged into 199 sounds and 128 patches that a browser sorts by engine or by what kind of sound they are.

• Theorems about the music

  That every note lands in its scale, that a bar has exactly the hits you asked for, that stopping the clock leaves nothing sounding: Lean's kernel checks these against the firmware's own code, not a model of it.