A proved TodoMVC

2026-10-23Milestone 1, done

The first milestone was TodoMVC, running natively on the Mac. TodoMVC is small, completely specified and has text input, and formal UI testing already uses it as a benchmark. It needs every layer of a UI framework and is small enough to finish.

Its state, view, layout, hit testing, focus and text editing are written in Lean. A thin Swift host passes events in and paints Lean's frames with Metal. The text fields do typing, selection, copy and paste, and input methods.

What's proved

Every action is a claim with an id, and the build won't let an id drift.
Each action does what its claim says, and the counts and filters stay right in every state.
Presence: a control is on screen exactly when its action is enabled.
Pressable: at any window size from the minimum up, a click at an enabled control's centre reaches that control, so it's visible, unclipped and on top.

Checked another way

The real app is driven through a thousand generated sequences of real pointer and key events, and must agree with the model after every step. A map of the app is generated from the claims, with the evidence behind each one, and everything the proofs trust about the host is written down in the trusted base.

Progress log

The videos and notes from this milestone as the work landed, newest first.

TodoMVC in Lean
The full TodoMVC, written in Lean and running natively on the Mac. Add, complete, double-click to edit, filter, clear completed, and toggle all. Every control is a claim (^202 to ^211). On the real app, 999 of 1,000 generated conformance sequences matched the Lean model. The one miss is a known edge case: a click that ends an edit can be dropped, as in a browser.
2026-10-23922459928s
Basics: the first Lean app
A whole app written in Lean: adding, ticking and deleting items. Lean decides the layout, focus, text editing and hit testing; Swift only draws. Every control is a claim (^101 to ^104). Lean proves that an item's Delete button exists exactly when the item does, and that the 'items left' count is right.
2026-10-23733224a17s
The host, with text
The new AppKit host painting through the Metal renderer: Core Text glyphs from an atlas, a caret, a focused field, a checkbox and a list. Typing goes through the Mac's text-input path, and every control in the accessibility tree is named by its claim id (^1 field, ^2 checkbox, ^3 Add, ^4#1 the new item). This app is the host's test fixture, with its frames built in Swift; the next video is the same host running a Lean app.
2026-10-233ff02ad18s
Boundary spike
The first thing on screen. Lean owns the state, the layout and the hit test; Swift forwards clicks and paints Lean's rectangles with Metal. The bar is the count (no text rendering yet). Reset (red) exists only while the count is above zero, which is proved in Lean, and here it's pressed through the accessibility tree.
2026-10-23a6b45bc9s

A proved TodoMVC

What's proved

Checked another way

Progress log

TodoMVC in Lean

Basics: the first Lean app

The host, with text

Boundary spike