Automated public certification of specifications and software

A system for public verification of software, the system comprising:

• at least one computing device comprising a processor, the processor configured to:
• generate a formal specification from an original pre-technical specification of a software project;
• generate algorithmic code, based on the formal specification, via a proof management computer system implementing mathematical proof-checking that fulfils the formal specification, wherein the formal specification comprises a mathematical description and a theorem;
• extract, from the algorithmic code, formally verified code in an executable language;
• generate, from at least one of the algorithmic code, the formal specification, or the formally verified code, a technical specification, wherein the technical specification comprises an interpretation of the formal specification written in a language for accessible for human comprehension;
• compile at least one of the formally verified code, a revised formally verified code, or an updated formally verified code into an executable program;
• and
• execute the executable program.

A non-transitory computer readable medium having embodied thereon a program, the program being executable by a processor to perform a method for public verification of software, comprising:

• automatically generating algorithmic code, based on a formal specification, via a proof management computer system implementing mathematical proof-checking that fulfils the formal specification;
• automatically extracting, from the algorithmic code, formally verified code in an executable language;
• automatically generating, from at least one of the algorithmic code, the formal specification, or the formally verified code, a technical specification, wherein the updated technical specification comprises an interpretation of the formal specification written in a language for accessible for human comprehension;
• compiling at least one of the formally verified code, a revised formally verified code, or an updated formally verified code into an executable program;
• and
• automatically executing the executable program.