Urbit has not put much effort into security, for some reason. To be fair, they don't claim their runtime is secure (yet)[1]. The process downloading and executing code from the network is not sandboxed with seccomp or anything similar, and its "jets" are unverified C libraries which any of this code is allowed to call into. They could sandbox it pretty easily (the worker process which runs third-party code only talks to a host process and not the rest of the world, so it could probably be run under seccomp, not even seccomp-bpf) which makes it all the more surprising that they haven't.

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...

Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#is-logically-verifying-co...

Let's say that Urbit claims to be formally, provably secure. But approximately nobody actually understands Urbit, which means that nobody knows whether the proof is solid. So as an outsider, I have to either take it on faith that it's secure, or I have to spend a fair amount of time immersing myself in this hard-to-learn system to see if the claimed benefits are really there.

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?

Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#is-it-actually-useful-to-...

You don't have to understand the linux kernel to buffer overlow a linux application; If they do something like "Here's the IP of a running urbit with 100BTC in it, good luck!" and it's still up in a few years, that'd be compelling.

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.