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.

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.

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.

Example from the Versus tutorial with verification:

    fn octuple(x1: i8) -> (x8: i8)
        requires
            -16 <= x1,
            x1 < 16,
        ensures
            x8 == 8 * x1,
    {
        let x2 = x1 + x1;
        let x4 = x2 + x2;
        x4 + x4
    }

    fn octuple(x1: i8) -> i8 {
        debug_assert(-16 <= x1);
        debug_assert(x1 < 16);
        let x2 = x1 + x1;
        let x4 = x2 + x2;
        let x8 = x4 + x4;
        debug_assert(x8 == 8 * x1);
        x8
    }

or, use prusti, that has contracts with a similar syntax checked at compile time as well

> verifying the correctness of code

What is the difference between "verifying" the correctness of code, as they say here, vs "proving" the correctness of code, as I sometimes see said elsewhere?

Also, is there a good learning resource on "proving" things about code for working programmers without a strong CS / math background?

Edit: I'm also very curious why "zero knowledge" proofs are so significant, and why this is so relevant. Eg I heard people talking about this and don't really understand why it's so cool: x.com/ZorpZK

One note though: Verus and the tool Software Foundations works with (Coq) take different approaches to proving things.

Verus attempts to prove properties automatically using something called an SMT solver, which is an automated system for solving constraints. Coq on the other hand, requires you to manually prove much more, offering a more limited set of automations for proving things.

Both have their advantages and disadvantages, namely that automation is great when it works and annoying when it doesn't.

(Another side note: Zero Knowledge Proofs (ZKPs) are kind of something different. A great many people who work in formal verification/proof don't touch ZKPs at all (ex: me). They are better thought about as a cryptography primitive)

As for zero knowledge proofs, there is little practical use, significance, or relevance to them due to the overhead involved and the lack of a "killer app", so to speak. But they're conceptually interesting.

> I have never done anything 'useful.' No discovery of mine has made, or is likely to make, directly or indirectly, for good or ill, the least difference to the amenity of the world.

Despite his self-proclaimed focus on pure mathematics, Hardy's work, particularly in number theory, has had profound applications in cryptography and other fields.

I agree about the overhead. The costs have come down significantly already but they still remain a few orders of magnitude too large. That being said, it’s killer app is cloud compute. Right now the only way to amortize the cost of HW is to run it on someone else’s computer, which brings along with it all sorts of security and privacy risks. Well-performing ZK proofs (which we don’t know if it exists / it may be a long time before we figure out how to do it) would let you do cloud computing securely without worrying about vulnerabilities in your cloud provider’s network. Like all cryptography, it’s a double-edged sword because the same techniques would let websites deliver code for your machine to execute that you have no knowledge of what it’s doing.

Cloud compute might be a good use case. But the overhead would have to come down dramatically for it to ever beat simply doing the compute in-house and incurring the overhead of managing a physical rack. Which is (and always has been, and likely always will be) an extremely viable option for anyone who is seriously interested in data access control.

A physical rack needs several physical people to look after it. Imagine it going down in the middle of the night while your sysadmin is on a vacation on Hawaii.

And cloud computing is also not expensive. If you don't have a large load, a t4g.micro instance on AWS costs 0.5 cents per hour ($1.2 per day, $438 per year). It will run most small workloads just fine, and you can easily scale it up with a couple of clicks.

Even when considering network bandwidth (where hyperscalers are famously expensive, and orders of magnitude above wholesale pricing), hyperscalers still be might be the cheaper option for larger public companies because of the structural issues they face internally (e.g., the inability to make it official that they are already running an ISP anyway, and start buying much cheaper carrier services from other ISPs).

As compared to what? Hypothetical IT departments staffed by the best engineers in the world?

> If we take what off-brand cloud providers charge (who compete mostly on price) and compare that to the EC2 pricing, AWS must have some tremendous inefficiencies if they only have 30% margins.

You're committing the cardinal sin of comparing list price. B2B sales heavily discounts the list price so you don't actually know what large companies are paying for vs what the discount providers would charge. I promise you the discrepancy isn't that wide.

Off-brand providers are usually much closer between list price & B2B pricing because their product offerings are so narrow that they can't offset losses in one with gains in another.

You also have to remember that hyperscalars need to charge a profit to reinvest those profits back into R&D. Corporate IT departments don't do that because it's a cost center. So even if you hired a super duper amazing team and built something that meets the needs today, over time the bean counters at your company cause you to underinvest what you actually needed (or you make a strategic mistake) and now you're having to spend significant resources to make up that shortage. Public cloud scaling is a way to mitigate that cost.

There's also the knock on effect of employee salaries - public cloud means more available (i.e. cheaper) expertise. A privately managed cloud means you have higher salaries if you're competing competently.

I've talked to people who run and run on private clouds (e.g. banks who are regulatory banned from it) and while it's impressive they really struggle to keep up with business needs in ways that you don't with public cloud. Yes, it's cheaper in some aspects & more customizable, but scaling limits have to be actively negotiated constantly - businesses gladly pay extra to not have to have that kind of internal negotiation.

Out of sheer curiosity, by which metric deploying the pre-packaged code (which takes seconds) into the cloud incurs a higher overhead compared to maintaining an in-house physical rack?

So the question is, does this hypothetical entity with very precious data incur the extra orders of magnitude of compute time in oder to not maintain a rack in house, or do they just... maintain a rack. Keeping in mind, of course, that they already must maintain a rack in order for ZKP's to make any sense at all. So... do they add a server to their existing rack to handle the workload, or refactor their entire computation to use ZKP's, and incur several extra orders of magnitude of compute time, and outsource the work to a cloud service?

An obvious use case for ZKP’s, which is under active research, is allowing medical data from institutions like the NHS to be processed by research organisations and pharmaceutical companies. Allowing pharmaceutical and research organisations to extract useful medical data from large populations, without requiring the handover of personal medical data.

In that situation the owner of the data has a clear incentive to use ZKP’s (they’re required to protect medical data), and so does the data processor (they can extract new inferences from previously inaccessible, but extremely large, datasets). There’s obviously a clear profit motive as well, and given the cost of medical research, the use ZKP’s doesn’t seem unreasonable.

The self-managed rack:

  1. Has to exist somewhere.
  2. Therefore it required the initial capital investment at some point, which is a mid five figure amount or more.
  3. Scales by its weight, height, depth and hardware specifications.
  4. Does not scale beyond (3) – hardware constraints of blades deployed in the rack are very rigid.
  5. Has to have available processing capacity to support the new workload.
  6. Has a habit of running of capacity at the most inconvenient moment requiring, well, a new rack.

  1. Has to be paid for from a budget. The budget may or may not exist when the new rack is required, therefore potentially incurring further, potentially lengthy, delays (i.e. «no money in the budget until the next financial year». Boom.).
  2. Has to be taken through the procurement. Depending on the organisation and its size, procurement can take anywhere in between 3 and 12 months.
  3. Has to be in stock.
  4. Has to be installed, deployed and configured.
  5. Requires technicians and engineers to be available within a designated time slot to complete (4). The technicians and the engineers (all of them or a single/few) may be unavailable due to X, Y or Z.

  1. The DC may not have enough room / power / cooling / etc. You and your rack are now stuck for an non-deterministic amount time.

  2. Adding a new rack to your rack HA setup requires a new network interconnect due to the network capacity reaching a saturation point. It is called «an expensive network switch». Add further delays, repeat all steps required to procure a new rack, add new/unforeseen delays.

Obviously you haven’t seen my org’s cdk repos

If "the cloud" was so simple, there wouldn't be 6-7 figure job positions dedicated to just setting up and managing their complexity and they definitely wouldn't come with certification requirements. Somehow the requirement of having a small team of employees "who can manage our own infra" is a deal-breaker but having a team of AWS Solution Architects is not.

In terms of time? Probably not much. In terms of cost, we’ll it’s about scale.

I worked on a project for a big financial firm about 8 years ago, to implement a burst-capacity overflow to cloud strategy for their compute needs. About one week a month or even one week a quarter, they would need a few tens of thousands of extra cores.

At this scale the cloud providers were not really able to react or provision fast enough, and required us to reserve the capacity full time. In the end the costs for “buy and manage more racks” internally worked out cheaper.

8 years ago the cloud did not effectively exist yet. Today the available capacity surpasses the needs of the prevailing majority of cloud customers, with a caveat – see below.

> At this scale the cloud providers were not really able to react or provision fast enough, and required us to reserve the capacity full time.

A few things have happened since then:

  1. Hardware capacity has been ramped up at a very large scale.
  2. Most importantly, advances in the workload distribution and optimisation: the cloud control plane distributes workloads to the available capacity across cloud data centres.

For most demanding customers, cloud providers have a solution called «the cloud appliance». A truck rolls in with the hardware that gets deployed as an extension of your own private cloud within a few days. Deployed software does not notice a difference and gets automatically distributed to the new processing capacity. If that is not enough, another truck rolls in with another «cloud appliance». It is presumed that if one operates at such a scale, they also have the money to pay for it.

Yeah it really did. I’ve been around a while. “Cloud” was becoming a buzzword around the tech industry 16 years ago. 8 years ago we had AWS, IBM, and Microsoft all vying for our business on this project.

> For most demanding customers, cloud providers have a solution called «the cloud appliance». A truck rolls in with the hardware that gets deployed as an extension of your own private cloud within a few days

None of which was as cost effective as adding more capacity to your own data centres, if you’re already running them at scale, because fundamentally someone is profiting from renting out those cloud appliances. If you have the in-house capabilities already, you can cut out the middlemen.

And the best way to verify a compiled binary is correctly compiled is to do the compilation. That's a trivial amount of work. Constructing a ZKP of the same is certainly more cost intensive.

But for the verifier, that isn't so obviously true: - Firstly, the verifier might not even have access to the formal proof that the program meets the memory correctness guarantees. It might have access to a binary code, plus a proof that the binary code compiled from a completely memory safe language. The verifier would need zero knowledge of the code (which might be proprietary). - Secondly, proofs aren't necessarily that big (especially for Groth16 circuits), and can be applied recursively (you prove that you had a proof that something was true), and aren't that expensive to verify. If verifying a program once when you download it means it can be flagged as being safe to run without expensive bounds and MMU checks, it could open up new types of more performant CPUs, and potentially save far more than it costs to verify.

This makes the assumption that you both have the source code and that the compiler is deterministic. With the latter one being not the case for (most?) modern compilers.

I'd argue that this is antinomic. Proving things about code isn't something working programmers do yet. I'd say that Hoare logic is a good starting point as it is sometimes taught in introductory CS classes.

Coq has a steep learning curve, especially if you're not familiar with OCaml or similar languages. Maybe Why3 is more beginner friendly https://www.why3.org

Proving vs verifying: could mean the same thing. Proving seems to me as something more interactive in nature, while verifying could be automatized (model checking, SMT-solving of annotated programs).

There's nothing trivial about "const a: int = foo();" though. Compilers disprove the claim by contradiction all the time.

It also might provide better options for identity verification, i.e. proving you have a certain government-issued ID but without actually leaking the document to the server (for it to be stored "for a maximum of 2 years / 3 years / 6 months / etc." but then leaked in a data breach anyway).

In this context it is the same.

> Also, is there a good learning resource on "proving" things about code for working programmers without a strong CS / math background?

I wish. The Dafny docs are pretty good but IMO formal software verification is not really at the point where it is usable for normal programmers like us who don't have a PhD in CS / maths. The examples make it look relatively easy, but you will quickly run into "nope, couldn't prove it" and the answer as to why is some hardcore implementation detail that only the authors would know.

I know. Four decades ago I headed a project to build a system amazingly similar to this one, intended for real-time automobile engine control code.[1][2] This new system for Rust looks practical. It seems to be intended for people who need bug-free code. Most verification systems come from people in love with formalism. Those involve too much human labor.

Hints:

- The assertions and invariants need to be part of the language. Not something in comments, and not different syntax. They should be syntax and type checked during compiles, even if the compiler doesn't do much with them.

- It's useful to work off the compiler's intermediate representation rather than the raw source code. Then you're sure the compiler and verifier interpret the syntax the same way.

- SAT solvers aren't powerful enough to do the whole job, and systems like Coq are too manual. You need two provers. A SAT solver is enough to knock off 90% of the proofs automatically. Then, the programmer focuses the problem by adding assertions, until you get the point where you have

    assert(a);
    assert(b);
 

I notice that the examples for this verified Rust system don't seem to include a termination check for loops. You prove that loops terminate by demonstrating that some nonnegative integer expression decreases on each iteration and never goes negative. If you can't prove that easily, the code has no place in mission-critical code.

Microsoft's F* is probably the biggest success in this area.[3]

[1] https://archive.org/details/manualzilla-id-5928072/page/n3/m...

[2] https://github.com/John-Nagle/pasv

[3] https://www.microsoft.com/en-us/research/video/programming-w...

I think that the explanation for such different levels of success is that economic incentives are different. The cost of a hardware bug is much much higher than the cost of the average software bug; this means that hardware companies are willing to spend a lot of money in getting designs right the first time, versus software companies that know they can always make bug fixes in new versions of their products. Additionally, hardware companies are used to paying millions of dollars in software licenses, which is not common in the software world.

My guess is it's because the problem is so much simpler. No variables, no loops, no recursion, etc.

As soon as you introduce any kind of feedback in your RTL design it's possible to do any kind of computation that SW can do and therefore proving correctness is difficult.

My guess: it's because people actually care about correctness for hardware. It's really expensive to throw out all those fab runs when you notice you messed up...

I don't think it's the mathematics, it's the tools. If the proof is separate and needs to be kept aligned with the specification and implementation manually, that's not really useful except for niche applications. Integrated approaches (like Verus here, or SPARK in the Ada context) should solve the implementation/proof gap, but such tools are not widely available for languages people actually use.

Software Foundations is great: https://softwarefoundations.cis.upenn.edu

If you stick with it long enough, you'll even build up to Hoare logic which is the underpinning the tools like dafny use to generate the equations they throw to the solver.

You don't need a particularly strong formal background in CS or maths to verify code, but it's a challenging task never the less.

1. The first challenge where people often give up is that you will often need to reason about your code in a different language than the code itself (not necessarily true for Verus that's being discussed here). In that sense it helps a lot if you already know multiple programming languages, ideally using different paradigms. 2. The second challenge is that you will need to be actually precise in describing what your want your program to. This is a lot harder than it sounds; there's no hand-waving, no "works in practice", but even beyond that, it's actually really difficult to express what you want from the program succinctly, and often not even possible or feasible. On the other hand, this is possibly the most practical skill you will currently be able to take away from the verification tools; it absolutely can change the way how you work, how you collect requirements, and how you go about writing code. 3. The third challenge is then actually performing the verification/proofs. This is currently painfully hard; most literature I've seen comes up with a ration between 5-20x between the amount of code you're verifying (in terms of lines of code, say) and the number of "proof lines" you need to write in some form. This may make sense for extremely critical code where a bug can cost tons of money; e.g., aerospace, or huge companies with tons of users - AWS is doing proofs at a fairly large scale, Apple is now doing the same at a smaller scale too. I would generally recommend NOT writing proofs if you can, but using tools that can do some kind of limited or heuristic verification. Which tools exactly I would recommend for a "working programmer" depend on what you're trying to do. For example, if you are writing concurrent or distributed code, I would recommend using something like TLA and the associated TLC tool. For lower-level Rust code (data structures and similar), I'd recommend the Kani verifier over something like Verus. For many other languages, the choices are limited or non-existent.

Zero-knowledge proofs roughly allow you to convince someone that something is true, without leaving them any wiser WHY it's true. Generally this is not what's interesting for software verification, but it's nevertheless extremely cool (because it's super counterintuitive). Most of the excitement indeed comes from blockchains, where these things are used, but it's debatable whether they're really practical. You can use them to transfer crypto around already today, without revealing the identities of the sender or recipient for example. However they are still computationally quite expensive and only work because there's currently not so much volume in crypto.

There is not much difference, except that verification usually includes identifying a formal logical proposition about the behaviour of the code.

In other words, formally verified code is code that has been proven to meet at least one formal proposition about its behaviour - for example, a proposition about a function f might be: if variable x is greater than 0, then `f(x) = 1`.

There is no such thing as proving something 'correct', you need someone to define what exactly correct means, and then someone proves it meets that definition. So the proving is only a subset of the overall formal verification task.

> Also, is there a good learning resource on "proving" things about code for working > programmers without a strong CS / math background?

Most will be specific to a particular technology and type of verification. There are some courses online that provide a high level overview, e.g. https://anton-trunov.github.io/csclub-coq-course-spring-2021....

If you want to get into specifics, you might need to pick an approach. You could learn a dependently typed language, for example there are some good resources out there on proving things in Agda or Idris. Or perhaps play around with one of the formal verification systems that can be bolted on to C or Rust.

> Edit: I'm also very curious why "zero knowledge" proofs are so significant, and why this > is so relevant. Eg I heard people talking about this and don't really understand why it's > so cool: x.com/ZorpZK

ZK is an exciting area of cryptology because breakthroughs in that area power new applications that people wouldn't have thought possible before. Applications to cryptocurrencies in particular can solve some of their scaling and privacy problems.

For example, one of the biggest problems with cryptocurrencies is that every single transaction ever needs to be recorded in a ledger that is distributed to every node participating in the network. That simply won't scale to microtransactions. Let's say that 1000 people each start with 1 coin, and do 100,000 small transactions averaging 0.001 coins amongst themselves (maybe they bought a coffee, or paid for information on a per-view basis, or whatever). Storing those 100,000 transactions forever will have an ongoing cost for every one of thousands of nodes on the network long after the transaction has happened.

Now that could be solved with centralisation - the parties send their transactions to a trusted company, who maintains balances for each of them without sending transactions to the network, but lets them withdraw their balance to the network if they ever want to. But centralisation is a risk - what if the company betrays their trust?

Zero-knowledge cryptography allows for the parties to roll up the signed transactions into a cryptographic proof saying, given these were the balances at the start of the 100,000 transactions, the person creating the roll-up has access to the signed transactions proving that the balances of each of the 1,000 parties at the end are this. Notably, the proof can be much smaller than the size of the 100,000 transactions. So that enables applications where people work off in 'side chains', and but can merge the side chain back into the main chain by submitting proof about the effects (but not all the detail of) the side chain into the main chain.

Automatic (SMT-based) verifiers like Verus, Dafny, F* (and my VCC :) require you to annotate most every function and loop but give you broad guarantees about the correctness of the program.

Tools based on interactive provers (like Coq or Lean) typically require more guidance from the user but can guarantee even more complex properties.

I understand Verus is an SMT based verification tool, and Lean is both an interactive prover and SMT based tool.

But my understanding in the area of formal verification is limited, and it would be good to get an opinion from someone well versed in formal methods for software.

- state and prove things about (e.g.) C code, like the "Software Foundations" book does for Coq. However, nobody seems to be doing this with Lean and the tools are missing.

- write programs in Lean4 and prove things about them. Some people are doing this a tiny little bit.

- formalize pure math and publish papers about that. This is what Lean4 (and Coq) is mostly used for.

The kinds of things Lean/Coq are able to practically state and prove are more general. Maybe you don't need that generality for real-world programs though.

Creusot does it in a different way using attributes, which IMO is a better approach because it means normal tooling works, though it does have much worse syntax.

So maybe an example could be a bare-bones gui app with a single textbox, that does an http request to some resource (having data that is unknown at compile-time and potentially untrusted is a very common thing) and fetches an array, which is bubble-sorted and displayed in the box. The bubble sort has some intentional bug (maybe due to some off by one error, the last element remains untouched). There are unit-tests that somehow don't trigger the bug (worrying that your tests are incomplete would be a primary motivator to go for proofs). It could then show how to replace the unit tests with a proof, in the process discovering the bug and fixing it.

The example wouldn't need to go into huge detail about the proof code itself as it is potentially advanced, instead it would focus on the nitty-gritty details of adding the proof, like how the interface between proved mathematical code and non-proved io code works, what command line to run to prove&build, and finally a zip archive with all of that, that you can play around with.

Edit: Actually just reading from stdin and writing to stdout is probably good enough.

1. Cases where specification is much less complex than implementation, like proving a sorting algorithm - the spec is very simple, forall integer i,j : i result[i]<=result[j] plus the requirement that elements may not be removed or added

2. Ability to eliminate checks for improved performance (not sure if this applies to Rust yet, but it works great with Frama-C).

3. "Unit tests" for entire classes of behavior, not just specific inputs. Even if you cannot write a formal specification for a huge complex protocol, you can incrementally add asserts which cover much more area than simple unit tests.

There's a place for formal verification, usually in places where a bug causes death or significant financial loss.

If I wrote a simple BFS or DFS and enumerated the search space how far would I get.. Is that not what TLA+ does in principle.

I am surprised people prefer having a dependency of something like Z3 at compiler level.

This is an extension of the CDCL (conflict driven clause learning) approach to SAT solving, which is a heuristic approach that uses information discovered about the structure of the problem to reduce the search space as it progresses. At a high level:

  1. assign true or false to a random value
  2. propagate all implications
  3. if a conflict is discovered (i.e. a variable is implied to be both true and false):
    1. analyze the implication graph and find the assignments that implied the conflict
    2. Add a new constraint with the negation of the assignment that caused the conflict
    3. backtrack until before the first assignment involved in the conflict was made

While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done.

[1]: https://apalache.informal.systems

It looks like there are some TLA+ implementations that do use SMT solvers under the hood.

It looks like the TLA+ Proof System does the same thing, but I believe you can also use TLA+ in "brute force all the states" mode. I haven't actually used it.