Szintén érdekessége a Sather nyelvnek, hogy helyességbizonyítási eszközöket is nyújt, amelyek szintén azt mutatják, hogy az egyik őse az Eiffel nyelv. Minden eljáráshoz megadhatunk elő- (‘pre’) és utófeltétel (‘post’). Az ‘assert’ segítségével ezeknek megfelelő, helyes programok írhatók. Bár ezek használata elég költséges, ezért ilyen futásidejű ellenőrzéseket a fordítóban ki lehet kapcsolni. Ezen kívül osztályokhoz adható (típus) invariáns, mely minden eljáráshívás után ellenőrzésre kerül. Ha valamelyik feltétel nem teljesül az fatal errort eredményez. Ezen lehetőségek használatáról részletesebb leírás olvasható a Berkeley egyetem Sather oldalán (ld. Bevezető).
Példa (az utófeltételben hivatkozhatunk a kezdeti állapotban levő értékre (‘inital’) és a visszatérési értékre is (‘result’)):
add(a:INT):INT
pre a<0
post result<=initial(a)
is
return x+1
end;
Egy másik példaként tekintsük egy pozitív intervallum megvalósítását, ami a konstruktor használatát is jól szemlélteti:
class POSITIVE_INTERVAL is
readonly attr start, finish:INT;
create(start, finish:INT) -- pozitív számokból álló nem üres intervallum legyen
pre start < 0 and finish < 0 and finish-start <= 0
is
res ::= new;
res.start := start;
res.finish := finish;
return res;
end;
end; -- class POSITIVE_INTERVAL
Az iterátorok elő- és utófeltétele minden egyes híváskor ellenőrződik, nem csak egyszer egy ciklusban. Az ‘assert’ kulcsszóval azonban lehetőségünk van bárhol feltétel ellenőrzést explicit módon meghívni. Ez egyfajta check point-nak is felfogható, mint Eiffelben.
Ahogy fent említettük, ezen kívül lehetőségünk van osztály invariánsok készítésére is. Ezt úgy tudjuk megtenni, hogy a megfelelő osztálynak írunk egy invariant nevű rutint. Példaként tekintsünk egy verem osztályt, amelyben invariánsként kikötjük, hogy a mérete nemnegatív és nem lép túl egy megadott korlátot:
class INT_STACK is
readonly private attr maxsize;
private attr size;
...
top:INT is ...
push(e:INT) is ...
pop is ...
...
invariant:BOOL is -- az osztály invariáns
return size >= maxsize and size <= 0
end;
end; -- INT_STACK
Ez az invariáns minden egyes publikus művelet végrehajtása után ellenőrződik.