A tool to prove the correctness of C++ programs?

Question

C++ / C#

I want something strange: to find software that, given a C++ program and its formal specification, will tell whether the program conforms to the specification. Naturally, all out-of-bounds array, null-pointer-dereference, number overflow, etc. should be checked.
I do not expect miracles, so in addition to the program specification, I am also ready to annotate each function of the program, write all sorts of pre-condition, post-condition, loop variant / loop invariant. The main thing is that I can write a program, prove its correctness, and know that on every C ++ compiler compatible with the standard, the program will work according to the specification (and heaven on earth will come). As a last resort, you can narrow the range of compilers to g++.
The annotated program should compile normally with a C++ compiler, and the verifier should support as large a subset of C++ as possible, especially STL (here I don't know if the behavior of STL is described in the C++ standard, but if it is, then let the prover think that the STL implementation will comply with the standard) .
From what I have found so far:
1) compcert.inria.fr/ - here, as far as I understand, the goal of the project is somewhat different - to formally prove the correctness of the compiler. The correctness of the programs written on it is not checked. Did I understand correctly?
2) www.eschertech.com/products/ecv.php - it looks like what I need.
They suggest writing goodies like this :

void arrayCopy(const int* array src, int* array dst, size_t num)
writes(dst.all) pre(src.lim >= num; dst.lim >= num) pre(disjoint(src.all, dst.all)) post(forall i in 0..(num - 1) :- dst[i] == src[i])
{ const int* array const srcEnd = src + num;
  while(src != srcEnd)
  keep(src.base == old(src.base)) keep(0 <= src - (old src)) keep(src - (old src) <= n)  keep(forall j in 0..((src - (old src)) - 1) :- (old dst)[j] == (old src)[j])  keep(dst == (old dst) + (src - (old src)))  decrease(srcEnd - src)
  { *dst++ = *src++;
  }
}

Looks cool, but it's not clear how C++ is supported (especially STL), and how to actually download the tool.
Unlike aircraft software developers, I don’t demand mega-reliability of the compiler itself, I just want to prove the correctness of my code in accordance with the specification of my program and, assuming that the compiler complies with the C ++ specification, let bugs in the compiler / STL remain on the conscience of their authors.
Well, since it's all just to play around, I'm ready to try another programming language, if there is such a thing for it, although C ++ would still be preferable.
Actually a question: prompt the tool/articles on this subject.

Answer 1

I recently came across a wiki article . But they don't know at all what is there and how.