Software bez chýb existuje, ale je ho veľmi málo, pretože jeho vývoj je šialene drahý. Napr. existuje soft s TCSEC A1 alebo EAL7 assurance level. To už vyžaduje formálnu verifikáciu. Formálna verifikácia ešte nemusí síce nutne znamenať, že SW je bez chýb, ale že vyhodnocované kritériá sú formálne dokázané (čo už má k bezchybnosti dosť blízko, závisí na kritériách).
Teoreticky by sa za SW bez chýb dal považovať kernel MINIXu 3, ale ten je navrhnutý ako minimalistický mikrokernel (kód má niečo cez 8500 riadkov). "Teoreticky" preto, že asi nikto formálne nedokazoval jeho správnosť, takže je možné, že nejaká chybička by sa tam našla.

