Not too much of what I said changes, but let me restate some things.
[I said] >> The entire discussion is very general in details. It is nothing remotely like a proof. It does not at all address the issue of imperfections in implementation or make any claims in this respect.
The discussion is about models mostly and is very high level. However, by being within a manual for a product, unless they clarify elsewhere (see last paragraph of this comment), it can be argued they are representing the product at least at some level.
The page says, "SELinux uses the Bell-La Padula BLP model...."
[I said] >> To conclude, I think you are overestimating the claims that Red Hat is presumably making. It's clear from the type of discussion that they are not offering any claims for an actual product. What they offer is a high level description of the model upon which their product is based. They offer the source code so the customer and the world has an opportunity to separate hype from reality. They possibly offer a certification. It's notable to mention that few vendors offer the entire buildable source code so that others can check up on the glossy hype. Unfortunately, I wish the open source community was advanced enough to be offering the source code to hardware.
Well, they are making claims about a product indirectly, but I think context should show that it is about the general behavior of the product and not a statement that it has been proven that the product behaves as the model described in all circumstances without any exceptions.
I think engineers would read such a high level documentation and recognize that the documentation is the intended behavior and not a promise that the software will abide to the models described therein to perfection.
Red Hat likely disclaims many things in the actual contracts they sign with their customers and customers. I am not familiar with the contracts vendors put forward to be able to compare and contrast them.