A research RISC-V OS written in ATS ((http://www.ats-lang.org/). The goal is to explore concepts used in ATS to make an OS that can be formally verified at compile time. A-OS do not have the goal to be a complete OS. It aimns at making Idris2 a better system language and thus concepts explored are expected to be rejected or to be eventually included in Idris2. The medium to explore those concepts in Idris2 is Pi-OS.
Please be patient. This is just the beginnings of the journey.