Matter of fact, regulators for safety-critical fields are just starting to accept formal verification as evidence. CompCert is only tool I know of that's qualified to just one standard. If in those fields, using formal verification instead of whatever evaluators are used to can get something rejected. It can aid the development or be supplementary evidence at best.
Without formal verification, there's no guarantee deadlines will not be missed, hard realtime will not fail and people will not die.
Sometimes failure is cheap; Other times it is not. A lot of systems out there make outrageous claims of fitness with no formal basis.
What a sad state the industry is in.
If you improperly prioritize tasks or use semaphore locks improperly or keep interrupts disabled too long, then your application will not be real-time.
NOTE: NuttX does provide tools to measure interrupt latencies, response times, and critical section times. Those are helps in creating a real-time system.
So, it is not a meaningful to ask if the RTOS has been certified in some way to always meet deadlines. You should ask rather, does the OS provide the tools that you need and does your overall application meets its deadlines.
It is meaningful. If the system doesn't offer these guarantees, no matter how good you are and how much effort you put into what's within your scope to implement, you won't be able to offer any guarantees.
This is ok if you can afford to fail. Just don't use it e.g. where human lives would be put at risk.
Without formal proofs, no hard realtime is possible; What you've got is soft realtime instead, the relaxed version where there's no guarantees.