Being "formally proven" to be free of various flaws did not make seL4 immune to memory corruption flaws. Despite the formal proof, a memory corruption flaw was found a few years ago. The PRs for the commits fixing it and amending seL4's proof are public:
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
You will find a number of other memory related bugs in its issue tracker:
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
Interestingly, the PR fixing "register clobbering" in memory was not labelled bug, so it is not listed when you filter by "bug".
I used to think seL4 was immune to these issues given its proof allegedly saying it is, but upon seeing this, I have come to think that the proof is not as comprehensive as the wider community has been lead to believe. That said, seL4 is still a very impressive piece of software.
Finally, to answer your question. The specification that seL4 meets is published on github:
https://github.com/seL4/l4v
https://github.com/seL4/seL4/pull/243
https://github.com/seL4/l4v/pull/453
You will find a number of other memory related bugs in its issue tracker:
https://github.com/seL4/seL4/issues?q=is%3Aissue%20label%3Ab...
Interestingly, the PR fixing "register clobbering" in memory was not labelled bug, so it is not listed when you filter by "bug".
I used to think seL4 was immune to these issues given its proof allegedly saying it is, but upon seeing this, I have come to think that the proof is not as comprehensive as the wider community has been lead to believe. That said, seL4 is still a very impressive piece of software.
Finally, to answer your question. The specification that seL4 meets is published on github:
https://github.com/seL4/l4v