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:

1. The Lion library: a pipelined RISC-V core.
2. lion-formal: formally verify the core using riscv-formal.
3. lion-soc: a System-on-Chip demonstrating usage of the Lion core on the VELDT.
4. 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.