Post #1027736

Many misguided (intentionally or otherwise) things have been said about the discovery of kernel bugs in Rocq using a LLM. For instance, some people have mentioned CompCert and use for Airbus. Well, I don't think these kernel bugs have any relevance for this.