[libre-riscv-dev] formal proof NLnet proposal in
Luke Kenneth Casson Leighton
lkcl at lkcl.net
Mon Sep 23 03:58:54 BST 2019
submitted. this is a proposal that we adopt formal mathematical
proofs as the "default" unit test, exactly as samuel falvo did. does.
and receive funds for doing so.
what that gives us is a greatly-simplified testing regime (as outlined
and explained by sam). it also ensures that there's no 3rd party that
needs to be approached in an independent audit of the code.
More information about the libre-riscv-dev