It is not possible, normal types can only prove so-called trivial properties (from Rice’s theorem). Every non-trivial property is unprovable in the general case.

Dependent-type systems can express more things (e.g. they can represent a concat function that takes two lists of n and m length, and return a list of length n+m), but proving those properties are hard and may not scale well. There are trade offs, like one might not have to actually prove the properties, just having them as facts may also be good enough.

I doubt it. The ultimate consequence of this endeavour is that a program that takes an int as input and produces an int as output would then have the type a:A->B(a). For example, a program P that for a given n produces the n-th prime number would express this in its type signature. Another program using that as a sub-function and doing p=P(n) could never reach the state where p is not the n-th prime number, the type system would be able to express that, and the type checker would need to be able to validate it. Etc. etc.

A type checker would amount to an automatic correctness proof, which in its full generality is impossible (by halting problem), but for the practically interesting classes could be done using a theorem prover / proof assistant and the occasional hint from the programmer. That would be great to have, but none of the examples you mention is anywhere close.