For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_37 https://link.springer.com/chapter/10.1007/9

For the case of resource usage, you can see work like https://link.springer.com/chapter/10.1007/978-3-030-81685-8_37 https://link.springer.com/chapter/10.1007/978-3-030-81685-8_... "Synthesis with Asymptotic Resource Bounds" which implements bounded resource checking. Of course, there are programs it rejects that it can't prove, but this is the essence of type systems: if you are willing to appease the typechecker, then you can establish facts about runtime properties. For your case, there may be a simpler dependently-typed solution: in such systems, you can already say things like "given an input natural number n determined at runtime, this functions returns a vector of size n", which bounds the result vector size. One approach could be to disallow explicit memory allocation and require passing a memory allocator as a parameter along with the associated "request" number bounding how many allocations you can do, in a similar dependently-typed way.