Open source verification in an anonymous volunteer network

•Categorical formalisation of an ‘open’ certification process not based on any central agency.•Trace semantics and soundness proof for the NRBG program logic.•Report on ‘volunteer cloud’ experiment performing a semantic audit of the Linux kernel source using a lightweight formal method.

An ‘open’ certification process is characterised here that is not based on any central agency, but rather on the option for any party to confirm any part of the certification process at will. The model for this paradigm has been a distributed, piece-wise, semantic audit carried out on the Linux kernel source code using a lightweight formal method.Our goal is a technology that allows open source developers to receive formally backed certifications for their project, in quid pro quo exchanges of resources and expertise with other developers within an amorphous and anonymous cloud of volunteers. To help ensure the integrity of the results, identifying details such as subroutine and variable names are not included in the data sent for analysis, each part of the computation is repeated many times at different sites, and checkpoint information is generated that enables independent checks to be carried out without starting from scratch each time.