يقترح مستخدم استخدام أحدث نموذج لغوي بميزانية ضخمة من الرموز لإنشاء نظام تشغيل كامل مفتوح المصدر يعتمد على النواة الدقيقة seL4. تتضمن الخطة تحليل شفرة مصدر seL4 وGenode وLinux لتكييف السائقين والأنظمة الفرعية لبيئة تعتمد على seL4.
- سيقوم النموذج بتحليل الشفرة من مستودعات seL4 وseL4_libs وsel4-tutorials وsel4test وGenode.
- سيقوم تدريجياً بتكييف سائقي Linux المختارين للأجهزة الشائعة وإضافة أنظمة ملفات مفيدة.
- ستكون العملية تكرارية، تتضمن مقترحات البنية، والترجمة، والاختبار، وتصحيح الأخطاء.
- سيتم إصدار النظام الناتج كمصدر مفتوح بما يتوافق مع التراخيص الحالية.
تطرح المنشور تساؤلات حول ما إذا كانت النماذج الحالية يمكنها إكمال أجزاء كبيرة من مثل هذا المشروع إذا لم تكن التكاليف مقيدة، وتحدد العقبات المحتملة مثل الحفاظ على الخطط طويلة المدى أو تصحيح الأخطاء على الأجهزة الحقيقية.