Currently, Ada. It's a fair tradeoff between formal verifiability and time/space control. You have to do a lot more extra work to meet these three requirements.
In the future, as we figure out how to make things like Haskell or an ML meet all three requirements, we'll move away from the labour intensive languages.
In fact, if strict real-time requirements aren't necessary Haskell is already useful. It's being used in the UK's national air traffic system.
Use Haskell+Agda to generate a subset of C. You also don't seem to understand what formal verification means. It's a verification of correctness, not resources.
In Real-time systems the two are synonymous. If you run-out of memory or fail to finish a vital calculation in a prescribed amount of time, your program is not correct. See Rate Monotonic Analysis for an example of verification (used in both formal and semi-formal situations) of time.
Where did you get this definition? Formal verification is named as such because it uses "formal methods" (mathematical proofs) to verify the behavior of the program. Your definition isn't formal verification, it's just... verification. You can't formally verify performance any more than you can formally verify physics.
All formal verification requires some assumptions. For example, you might assume that a cosmic ray isn't going to alter a bit in your instructions stream (or you might be developing for outer space and you assume that no more than X bits will be flipped in a given amount of time).
Certain assumptions can make it trivial to verify the performance of code (e.g. assume all memory accesses miss cache and happen right at the beginning of a DRAM refresh for the address you are accessing).
That usually ends up too crappy, so you bound the worst case a bit more by using the cache-replacement model of the CPU you are using. Writeback cache make this analysis quite difficult which is one of many reasons for the existance of writethrough cache. In any event, given a certain execution model, it is tractable to bound the worst-case performance of a system formally.
In the future, as we figure out how to make things like Haskell or an ML meet all three requirements, we'll move away from the labour intensive languages.
In fact, if strict real-time requirements aren't necessary Haskell is already useful. It's being used in the UK's national air traffic system.