Urbit has also had (and almost certainly still has) bugs where jets give different results than the code they're supposed to accelerate (a "jet mismatch") [2]. I agree that its "axiomatic" bytecode would lend itself well to verification theoretically, but Urbit as she is spoke is not anywhere close. They also at least historically seemed somewhat hostile towards academic CS research (including formal methods) probably for weird Moldbug reasons.
[1]: https://urbit.org/faq#:~:text=The%20security%20of%20the%20ru....
[2]: https://urbit.org/blog/common-objections-to-urbit#:~:text=Ye...
But it's not just Urbit. Rust has essentially the same problem.
In fact, perhaps all of formal verification has this kind of problem. How do you prove the benefits to someone who doesn't know the tools?
But more generally, if it's true that the only way to make a provably secure app is to design the OS and language around that purpose, then the problem you describe is general too - it will always be a challenge to find auditors.