Prokázat neexistenci vady není možné. Nenechte se zmást pojmem "existence bezpečnosti", protože ve skutečnosti se ověřuje, že tam není žádná chyba ani vada.
Vaše věta "pro sérii exaktně definovaných příkazů jde určit exaktní výsledek série" pak zřejmě předpokládá systém, který nemá žádné vstupní parametry. Tedy třebas konstanta. Jakmile jsou nějaké vstupní parametry, tak už je potřeba zkoumat, jak na tyto parametry systém reaguje. Třebas generátor konstanty PI, kde jako parametr je požadovaný počet desetinných míst. A rázem musíte zkoumat, jak to reaguje na malá čísla, jak na velká, jak na záporná, jak na desetinná a jak na hodně velká (nedojde tomu pamět? Nepřeteče tam nějaká proměnná?) Navíc jako auditor hledáte právě takové kombinace vstupních hodnot, kdy se to začne chovat chybně. A ta nemožnost to "absolutně ověřit" plyne z toho, že nemůžete zkusit všechny kombinace vstupů, ale jen nějakou množinu. Že pro ni to funguje ještě neznamená, že neexistuje jiná, pro kterou začne "chodit pěšinkama".
A ještě jedna věc, k té vaší "zaručeně a definitivně". Zkuste tohle v několika programovacích jazycích, ve skriptech, zkuste to jako float i jako double:
a = 2000000
b = 0.000002
c = a + b
echo a
echo b
echo c
Co může být jednoduššího, než sečíst dvě čísla? Přesto většinu lidí překvapí, co se při použití 32bitového floatu uloží do c. A otázka pak je, zda by to nešlo nějak zneužít. Přidejte fakt, že řada lidí používá desetinná čísla a operátor porovnání na přesnou shodu a máte dost možná útočný vektor.