Capability-safe languages in the E family, like E and Monte, have perfect isolation, or as it's known in the community, "working encapsulation." In a capability-safe system, only bugs in the implementation, such as runtime or CPU bugs, can violate isolation.
Here's an introduction to E: http://www.erights.org/talks/promises/paper/tgc05-submitted....
The Monte language's manual starts with a tutorial and an explanation of what capability-safe languages do: http://monte.readthedocs.io/