SPARK is a formal proving system for Ada. Formal correctness is what they focus on, that Ada can safely prove mathematically how a function will behave, and how a body of functions will behave.

If you're using Ada without SPARK, it will try and enforce these same guarantees, but generally with a runtime contract system, rather than compile time.

I've always wondered this - Does the compiler actually use all that contract information, or is it just the prover?

As of Ada 2012, the redesign means that the compiler can make use of the contract information, and was one of the main reasons for a lot of the changes.

That makes sense. Otherwise why bother conflating the programing language with the verification language.

pretty nice, is the SPARK market lively ? I'd love to see how work is done there

Lively, but proprietary. A lot of SPARK stuff tends to be automotive, factory designs, fabrication and the sort of stuff where people working there are buried under dozens of NDAs preventing them from discussing their work in any way.

But projects tend to have a longer shelf-life. Contracts expected to take a decade to complete aren't unusual, and the product can be expected to be in use for twice that, or longer.