- Phase: Planning
- Language: New language
- Design: Design new domain-specific language for device driver, RTOS, and bare metal code
- Product: None
- Demo: None
- Paper: None
- Phase: Closed
- Language: C verified by VeriFast
- Design: Apply annotation to NetBSD kernel
- Product: None
- Demo: Verify sample application on ChibiOS/RT using VeriFast, Trying FreeRTOS using VeriFast
- Paper: None
- Phase: Re-training
- Language: ATS
- Design: Snatch NetBSD kernel using ATS
- Product: c2ats
- Demo: ATS programing on Arduino, ATS programing on ChibiOS/RT, ATS programing on mbed
- Paper: "ATS言語を使って不変条件をAPIに強制する", "Arduino programing of ML-style in ATS"
- Phase: Closed
- Language: Haskell (Ajhc compiler)
- Design: Snatch NetBSD kernel using Ajhc Haskell compiler
- Product: Ajhc Haskell compiler
- Demo: Application on Android NDK, Application on Cortex-M3, Application on ChibiOS/RT, NetBSD kernel driver
- Paper: "強い型によるOSの開発手法の提案", "Systems Demonstration: Writing NetBSD Sound Drivers in Haskell"