Man-Made Minions is a privately-owned and funded UK-based commercial venture. The goal of the SMVS Project at MMM is to achieve a state of affairs whereby every line of operational program source code in the world has been formally verified as correct and therefore contains zero bugs.

Those of you with a solid background in theoretical Computer Science are probably thinking that the immense desirability of such a goal is matched only by the immense difficulty of achieving it! (Nothing worthwhile is easy!)

If you fall instead somewhere between being a practical professional programmer and a complete non-techie (at least in this field) then you're probably wondering what the hell we're talking about! What is "formal program verification", what's so great about it, and why should you care?

Basically, software bugs consume tons of money. Worldwide expenditure on software development is $1.5 trillion per year, including $500 million spent every day identifying and fixing bugs. Widely-practicable debugging methods find some bugs but not all bugs, leading to lots of bugs being missed and ending up in operational code, leading to software failures costing a further $500 million per day. That's $1 billion wasted every day!

In a nutshell, formal program verification has the potential to catch EVERY bug, but is currently too impractical for most software developers to use. The SMVS Project aims to eliminate these impracticalities so that formal verification may be universally applied. This is the Holy Grail of Computing!