Tools

Profiling

LeanProfiler

LeanProfiler records nested IO spans, structured runtime metadata, Lean heartbeats, and process resource counters. It writes a Trace Event file for Perfetto and a JSON summary that can be compared with an earlier run.

The TorchLean example wraps an existing model runner. Device completion hooks can include synchronized work in a span, and the report labels that measurement as completion latency rather than device-kernel time.

Checked case studies

TorchLean Verified Examples

The current examples cover batch-invariant inference and a verifiable transformer checkpoint. Each README says what Lean checks and what still depends on Python, CUDA, solver output, or hardware.