Software validation

[DigitalDesigns]

Does D have any methods of validating code in a natural manner 
besides unit tests and contracts?

I'm specifically thinking of validating mathematical calculations 
and boolean operations that could depend on very improbable 
scenarios but are technically invalid logic.

These issues tend to creep up in calculations that involve 
floating points due to various reasons or comparisons that 
mistakenly use > for >= or vice versa.

If I have a variable such as a buffer which has a length and an 
offset in to that buffer is calculated using double precision 
then rounding errors could cause the offset to except the length 
and create an access violation.

To be able to theoretically test all the possibilities all valid 
inputs would need to be checked. One can setup unit tests to test 
these possibilities but it can be difficult to cover all cases in 
even a semi-complex program.

Just curious if something exists that allows for mathematical 
validation such code in an relatively canonical way. This isn't 
too hard for pure functions but dealing with non-pure functions 
can be a pain.