μSkia: Formal Skia semantics in Lean powers a verified optimizer, 18.7% faster rendering

Researchers have built μSkia, a formal semantics for the Skia 2D graphics library, and mechanized it in the Lean proof assistant. Their motivation is a persistent gap in graphics performance: libraries like Skia, CoreGraphics, and Direct2D are heavily optimized internally, but the applications calling them routinely issue wasteful sequences of drawing operations. Even Chrome, developed alongside Skia, emits inefficient instruction streams across the 100 most-visited websites — a symptom of Skia’s intricate semantics and its opaque execution model, which make it hard for developers to reason about what the library actually does.

μSkia models the pieces that matter for correctness — canvas state, the layer stack, blending, and color filters — and splits the semantics into three strata to keep concerns separate and the model extensible. Using this foundation, the authors catalog four recurring patterns of suboptimal Skia code that Chrome produces, write replacement sequences for each, and prove the rewrites correct in Lean, surfacing several subtle side conditions along the way. Those verified patterns feed a high-performance optimizer that rewrites Skia command streams on the fly.

Across 99 programs captured from the top websites, the optimizer delivered an 18.7% speedup over Skia’s most modern GPU backend while adding at most 32 microseconds of overhead, with gains holding across different sites, backends, and GPUs. To close the loop, the optimizer’s traces are replayed through the μSkia semantics and translation-validated in Lean, giving end-to-end assurance that the faster output stays faithful to the original. It’s a clean demonstration of compiler-style optimization backed by machine-checked proofs applied to a real, widely deployed graphics stack.