🦀 Verifying Rust Code - Advanced

Complete proofs, honest bounds and a fork that stays verified

Sampled agreement is a strong form of evidence, and it has a hard edge. A Kafka varint decoder that agrees with Java on 11,560 golden vectors has still met only a sliver of the inputs it will see on the network. The way past that edge is to stop running the code on chosen inputs and start reasoning about all of them at once.

That sounds like the territory of theorem provers and PhDs, and for some properties it is. For a surprising amount of real code it is not. A varint decoder reads at most five bytes. Its input domain is finite, and a model checker can cover every one of those inputs in a few seconds. The proof that comes out is not bounded in any meaningful sense; it is complete.

This part continues the proto-kafka case study, the forked Kafka protocol crate behind the blink broker, from the point where the opening instalment of the series left it: an independent reference spec, 12,546 golden vectors from Java, and five crate bugs fixed. What follows is the climb from those vectors into proof, including the parts that did not work.

Proof against what?

A proof is a statement about a specification. If the specification is wrong, the proof is a confident, machine-checked…