FM-1 simulator the real firmware
Off. Power on to boot the firmware (browser audio needs a click).
Off
The proofs, watched the theorems' statements, checked on the running machine
The theorems are about the Lean. The C that calls it and the compiler are trusted; here twelve of the statements are also asserted at the point the C uses the Lean's answer. A failure could only come from those trusted parts.
| theorem | checks | state |
|---|---|---|
| power on first | ||
Keys: computer rows Z–/ play from C4 and Q–T from C5, or click the keys.
- and = are OCT- and OCT+. Space is PLAY, Esc is HOME, [ and ] turn Select,
PageUp and PageDown step through the patches. Knobs: scroll wheel, drag up or down, click the left or right half,
or arrow keys when focused. Hover a button for what it does. A link with ?patch=N loads that patch at power on.