Hacker News Reader

Comment by lsuresh | Hacker News Reader

We've used Verus to write formally verified Kubernetes controllers.

Basically, we can prove liveness properties of the form "eventually, the controller will reconcile the cluster to the requested desired state". As you can imagine, there is a lot of subtlety and nuance to even specifying correctness here (think rapid changes to the desired state requirement, asynchrony, failures and what not).

Code: https://github.com/vmware-research/verifiable-controllers/, with a corresponding paper due to appear at OSDI 2024.

View on HN

What does it do more than unit tests?

Full-system verification is more powerful than unit tests. You can prove an implementation of a distributed system is free of entire classes of bugs, modulo your specification.

The reason is that there is simply no way to practically write tests to cover enough out of all possible executions of a distributed system. Think arbitrary interleavings of message arrivals, failures, restarts and events affecting every single entity in the distributed system.

We built a framework on top of Verus (called Anvil) that allowed us to write a top-level specifications of the form "If the ZooKeeper operator says it can reconcile a ZK cluster according to a 'spec', it will eventually bring up a ZK instance running on spec.num_replicas pods, managed by a stateful set etc.". We can then make sure the implementation of our ZK operator, repeatedly trying to executing a control loop to reconcile the current and desired states of the ZK instance it is managing, delivers on that specification. Using verification here allows us to be sure that our ZK operator is correct even in the face of failures, asynchrony, series of edits to the required desired state (think repeatedly asking the operator to switch between 3 and 10 replicas), and more. This stuff is honestly impossible to write tests for (and unsurprisingly, no open-source Kubernetes operator we've seen tests for such cases extensively).

That said, we still need to use traditional testing to be sure our assumptions about the boundary between verified and unverified code is correct (e.g., think of the Kubernetes API itself, assumptions about built-in controllers etc).

The precursor to our use of verification in this context was, in fact, a system we built to do automatic reliability testing: https://www.usenix.org/system/files/osdi22-sun.pdf -- even that work found a lot of safety and liveness bugs, but I feel it barely scratched the surface of what we could do with verification.

So while the tooling still has a long way to go, I personally hope full-system verification becomes mainstream someday.

Hmm interesting. Do you think deterministic simulation is a much more accessible approach than verification? Also curious what tooling you think is still missing/not up to par?

I assume by deterministic simulation you mean: use a harness wherein you can deterministically run specific executions of a distributed system (e.g., force specific event interleavings, failures etc?)?

If so, yes it's more accessible. The previous paper I linked (Sieve) used such a technique to reliably execute test plans so any bugs we find can be reproduced. But when it comes to correctness, I still think verification is just much more powerful.

W.r.t tooling, I think there's still quite the usability and knowledge gap to cross. The way I see it, we've had decades to figure out how to engineer complex software systems from simpler parts, with a lot written about software engineering and testing in general.

Full-system verification in contrast is still really young, and breaking up a system into an implementation, specification and proofs currently requires quite some creativity and even awareness of how the verifier works. The Anvil project I mentioned above had a team of systems, distributed computing, reliability and verification experts (including Verus authors) team up to do this.

Probably talking about something like https://antithesis.com

Reply on news.ycombinator.com