Machine-checked theorems

6,615 across 131 proof modules (~151,897 lines)

Compile-time #guard tests

3,411 (kernel-evaluated at build time)

Axioms / sorry / partial def

0 / 0 / 8

Runtime test suites

1,810 tests across 15 suites

Spec examples passing

132/132 (100%)

yaml-test-suite IDs

358/358 YAML 1.2.2-applicable (100%)

yaml-test-suite total

358/406 (88%; 48 skipped are YAML 1.1/1.3)