Team Eiffel

"A Direct Path to Dependable Software" is the title of a recent article in the CACM. It piques the interest, but otherwise has few details on how the approach would work. But an interesting quote:

As the required level of confidence rises, though, testing soon becomes prohibitively expensive, and the use of more sophisticated methods is likely to be more economical. Invariants may be harder to write than test cases, but a single invariant defines an infinite number of test cases, so a decision to write one (and use a tool that checks all the cases it defines) will pay off very soon.