Area is the mainline OSTD executable-LoC budget per module; modules outside the verification plan count as unplanned. Hover or focus a module for its exact counts.
Functions with a verified body, linked to their Verusdoc documentation and grouped by module.