3.4. Heartbeats🔗

Lean heartbeats count work mainly through small allocations on the current execution thread, with extra weight for selected allocation-avoiding paths. They are useful beside elapsed time when managed Lean work stays similar but wall-clock noise moves.

Heartbeats are not instructions, cycles, bytes, or device work. A foreign call can take a long time while adding few Lean heartbeats. Each Lean thread has its own counter.