Following #640, we should also run that proofs in CI following the approach that mlkem-native is taking: https://github.com/pq-code-package/mlkem-native/blob/main/.github/workflows/hol_light.yml