Ça pourrait être intéressant si le code source de la vérification était disponible... ce qui n'est pas le cas.
Oh c'est même pire que ça: seL4 est propriétaire donc le code de seL4 n'est pas disponible non plus..
Ceci dit, vu le manque d'intérêt des libristes (mis à part les chercheurs) pour les preuves de programmes, l'équivalent libre n'est pas prêt d'arriver..
[^] # Re: Avis de Linus Torvalds sur les micro-noyaux
Posté par reno . En réponse à la dépêche Entretien avec Andrew Tanenbaum à propos de MINIX. Évalué à 5.
Oh c'est même pire que ça: seL4 est propriétaire donc le code de seL4 n'est pas disponible non plus..
Ceci dit, vu le manque d'intérêt des libristes (mis à part les chercheurs) pour les preuves de programmes, l'équivalent libre n'est pas prêt d'arriver..