Our great sponsors

tlaplus
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.

InfluxDB
Power RealTime Data Analytics at Scale. Get realtime insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in realtime with unbounded cardinality.
Quickcheck is a Haskell testing library which allows the programmer to write propositions about how a function should behave, and the library will try to find cases which falsify the proposition.
If my understanding is correct, it can't "prove" any properties, only disprove them.
For concretely proving properties of a program, you would need something like Idris's dependent type system, where you can prove that a function always returns a sorted list, for example.