If there is a validation report about FreeRtos ?

FreeRTOS as delivered is tested dynamically using very strict code coverage criteria (which is why you see the 'mtCOVERAGETESTMARKER()' macros, which when defined allow us to determine which decision/condition points in the code have been executed for both true and false inputs), but this is informal. In addition a couple of universities have provided formal proofs (mathematical proofs) that were published at various academic conferences, albeit on older versions. In addition WITTENSTEIN high integrity systems have their SafeRTOS derivative which has been been certified to various industrial and medical software standards.