I discovered seL4 at a conference I’m currently attending and it looks really interesting. Seems it would play nicely with usecases proposed around SBOMs (software bill of materials) at https://www.ntia.gov/sbom. Any possibility a cycloneDX (or SWID or SPDX) SBOM has been created for any version of seL4, or better yet that it is built into the build process? If so, I’d like to include in the corpus being built up by that group. If not, would anyone consider add SBOM as a feature?