> What I want is to be able to specify and have (when possible) automatically proven arbitrary assertions anywhere in the code

This doesn't even exist in TypeScript. If I change

    function foo(a: any) { return baz(a); }

to

    function foo(a: number) { return baz(a); }

whoever calls foo has to still prove (or assert) that the argument is a number.

Is that what you're after, asserting a dependent type? For example being able to change:

    function divByTwo(a: number): number { return a/2; }

to

    function divByTwo(a: even_number): number { return a/2; }

You want every place divByTwo is called to also automatically supply a proof that the argument is even?