Hello,
I’m having a hard time finding the answer to my question.
In a real life & commercial system that needs to be accredited, how can the seL4 proofs by used by the accreditors? I have problems understanding what’s the output generated from those proofs and how the accreditors can trust that output?
Thanks for your help 