sysx
A computer you can read all the way down. A language whose every function is proven; the machine code it becomes, checked against the instruction set; a processor core and its devices, proven against that same instruction set; and a kernel and a shell written in the language, running on that core. Each part lives in a repository of its own; sysx is what they share.
The parts, and how they fit
On the left, how a program is built: written in sysp, proven, lowered to sysi, and turned into RV64 machine code that is checked against the instruction set. On the right, what it runs on, from the board up to you. The two meet twice: the kernel is such a program, and the instruction set the code is checked against is the one the core is proven against.
isa.sysr, on both sides.Each part
A part has a name when it has an interface of its own that other code is written against (Names). Each keeps its docs in its own repository; until it has a site, its README is the place to start.
Why one suite
Each part stands on its own: sysp is a language you could use for anything, sysr a hardware language with its own benchmark, sysi an IR with its own checks. Together they make it possible to own every layer of a computer, and so to try what a borrowed layer would not allow: isolation by a proven language rather than by virtual memory, messages that are copied rather than shared, capabilities rather than a superuser. The layers that are still borrowed (QEMU, clang, the C backend) are being replaced from below, one that runs at a time: sysi already builds sysk without a C compiler, and sysr's core boots it unchanged. What each level proves, and what it still trusts, is the chain of trust.