Examples
Counter
A program of four lines of logic, embedded here as a component with Html.map.
LeanUI counter
TodoMVC
The whole TodoMVC specification: editing, filters in the URL fragment, the list kept in localStorage as JSON. Its model logic is proved to keep the list's keys unique under every message.
todos
Roster
Can we staff this? An untrusted solver answers, and a checker proved correct in Lean decides what the app shows, down to why a day cannot be staffed. A roster comes with a proof, which an independent kernel checks again in your browser. Open the Roster demo