-
An Agent at the Watchmaker’s Bench
Two ETA PDFs, a CAD folder and one sentence. An hour and a quarter later, a Swiss pocket-watch movement could be assembled screw by screw in a browser and set ticking.
-
seL4, Meet Lean
Can the mountain of human-checked proof behind the world's most verified kernel bootstrap a version in Lean? 27 hours with Claude Opus 5.5: what worked, what checking against l4v's own Isabelle caught, and what finishing would cost.