Lion is a formally verified, 5-stage pipeline RISC-V core. Lion targets the VELDT FPGA development board and is written in Haskell using Clash.
This repository contains four parts:
- The Lion library: a pipelined RISC-V core.
- lion-formal: formally verify the core using riscv-formal.
- lion-soc: a System-on-Chip demonstrating usage of the Lion core on the VELDT.
- lion-metric: Observe Yosys synthesis metrics on the Lion Core.
In my view, with RISC-V, it is finally within the realm of possibility for every single layer of a machine’s architecture to be open source and formally verified. The development on this seems to have gone mostly dormant (and many of the toughest parts of the process remain).
I am posting this here because this sounds like a great foundation for a cypherpunk machine. My vision is for an end-to-end formally verified machine and OS. 99.9999999999% free of back doors, exploits. That’s sort of impossible but this machine might have less of them. It would obviously require extreme hardening in comparison to a typical Linux machine.
This might be the foundation for something like “trusted hardware”.
applications for such a machine:
- Lemmy/ActivityPub instance (this one would be the perfect candidate)
- secure communications
- pen testing
- voting machines
- stake pool/node/mining
- lite node for real-time on-site transaction verification
I don’t nearly have the skills to approach this. But what I do have is time.