The suite

The chain of trust

What each level proves, what it still takes on trust, and how the two levels on either side of each step are checked against each other. A step is only as strong as the weakest link below it, so the trusted links are the suite's to-do list.

From the source to the board

Each box is something you could hold: a source file, a compiled program, a specification, a circuit. Each line is a check between two of them. Teal is checked by a tool, every time; amber is trusted, a step taken on faith for now.

Teal: checked by a tool on every build. Amber, dashed: trusted. The two checks against isa.sysr are what join software and hardware: the code and the core are each shown to mean what the same specification says.

Level by level

Level	Proves or checks	Trusts	Read more
sysp	every function: bounds, overflow, contracts, linear ownership, for every input, with z3; a function that cannot be proven is rejected	z3; the checker itself (its soundness log lists what was found and fixed); every `extern`'s contract	sysp's reference
sysi	every lowering is well formed (`sysi check`); the linked RV64 executable means what its sysi says, block by block, each instruction as `isa.sysr` defines it (`sysi validate`), so the assembler and linker are checked too	the lowering from sysp to sysi (next: checked against sysp's proofs); the calling convention's alignment; sysp's proofs that every access is in bounds	sysi's docs
sysr	the core's execute stage, ALUs, multiplier, load/store unit and PMP equal to the ISA and the privileged spec, by k-induction; the PLIC's claim; the core compared cycle for cycle with an independent ISS	`isa.sysr` as a transcription of the RISC-V manual; Yosys and nextpnr; the FPGA	sysr's docs
sysk	proof obligations across the kernel and the default system's user code; deadlock freedom by its model; the platform's devices against sysr's contract	lines of assembly and extern contracts; the model's assumptions; QEMU and clang where they are still borrowed	sysk's trusted base
sysh	proven as user code; holds only the capabilities its manifest gives; every job it starts is judged by the kernel before it runs	what sysk trusts	The shell

sysk's numbers here are read from its own generated files when sysk sits beside sysx; a question mark means it is not there. The other parts' facts live in their repositories until they have sites of their own.

What would close each amber link

The lowering from sysp to sysi: a check that each lowered function keeps the contracts sysp proved of it. sysi's next step; after it, the C compiler leaves sysk's trusted base.
isa.sysr against the manual: it stays a transcription, but one that two independent tools (the core's proofs and sysi's validation) read the same way, and that the ISS cross-checks.
Synthesis and the board: borrowed, as z3 is, for the foreseeable future; the core's behaviour is cross-checked in simulation of the generated Verilog.
sysk's assembly and externs: a budget with a test, never above its limit, each extern listed with what it assumes; sysr's platform contract already discharges the interrupt controller's and the UART's.