Are there any research projects trying to make "proof" programs / languages?
Dependently typed languages may fit what you're asking for. See Idris and the book Type-Driven Development with Idris for an example of encoding critical information into the type system.
Beyond that, see SPARK where you're limited to a provable subset of the Ada language (the subset has been extended with each version) so you can make assertions and it will attempt to prove (as part of compilation) that the assertions hold. As in, you could have a function that should always return a non-negative integer, but if it does something like (not fluent, so may be wrong but the principle is correct):
function Foo(A : Integer; B :integer) return Integer with
Post => Foo'Result > 0;
function Foo(A : Integer; B : Integer) return Integer is
begin
return A - B;
end Foo;