Project Flawless

What if we could prove that a piece of software is free from vulnerabilities and bugs?

Goal

The goal of this project is to create a minimal assembler toolchain and a prover that are themselves proven to be free from vulnerabilities and bugs.

The assembler must be capable of assembling itself and the prover.

Definitions

Flawless

A piece of software proven to be free from vulnerabilities and bugs, will from now on be called 'flawless'

Software

Software is a parent term that refers to either a source or an output, depending on the context in which it is used. It is used whenever the distinction between a source and an output is not relevant.

Source

The source of a software is the complete human-readable specification. It contains all information required by an assembler to produce the corresponding output.

Output

An output is the machine-readable representation produced by an assembler from a source. It is the artifact whose behavior is intended to correspond exactly to the specification given by the source.

Assembler

An assembler is a toolchain that transforms a source into its corresponding output.

Assumptions

1. Flawless Assembler

A flawless assembler transforms a flawless source into a flawless output.

2. Flawless Composition

A flawless composition of multiple pieces of software produces a flawless software.