I should have inferred that you were talking about Racket since some of the papers you had listed were Scheme related. Gradual Typing and similar powerful type systems are not available in the world of C/C++ where i come from (though modern C++ has a few simpler similar features). Hence my comment on that.
We already know from Curry-Howard isomorphism that "Predicates (i.e. Contracts) <-> Types". It is actually easier to first think of only predicates over the state space which can then be mapped into a type. Here you think of types as sets (as a first approximation) and predicates establishing a relation(a set of tuples) over a subset of their cartesian product. The logic is explicit with no unnecessary abstractions obscuring the concepts. This was Dijkstra's approach which is at the heart of CbC and important for us to understand.
If you straight away start with type systems with a "standard" programmer they are lost. The mistake we do is that we do not properly show the mapping of discrete mathematics onto the constructs of a programming language. With FP languages the problem is compounded since it is based on lambda calculus and so the idea of a type is even more generalized in a different dimension.
IMO, with LLMs generating gobs of code now, we need this in some form yesterday. CbC gives you one approach where the specifications are Predicates (invariants/contracts/etc.) which is successively refined to get the final program but preserving correctness at every step.
Your project sounds quite interesting; Good luck with that! You might want to write a paper/article on that for wider dissemination.