Machine-checked theorems

3,857 across 63 proof modules (~63,747 lines)

Compile-time #guard tests

2,142 (kernel-evaluated at build time)

Axioms / sorry / partial def

0 / 7 / 4

Runtime test suites

1,670 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)