Comment by Ericson2314
2 days ago
The author should try some more modern formal methods.
Tools like Lean and Rocq can do arbitrary math — the limit is your time and budget, not the tool.
These performance questions can be mathematically defined, so it is possible.
Indeed.
And the SeL4 kernel has latency guarantees based on similar proofs (at considerable cost)