AWS 用 Lean 4 数学证明 Aurora Grover 数据修复协议的鲁棒性

Much of our digital data — our family photos, novel drafts, medical histories — exists as electrical patterns in metal boxes subject to grid outages and disasters natural and artificial. Any given box has an intolerably high chance of failure, so we copy our data into several metal boxes in different geographical regions. Redundancy protects data. But what if we want to change our data — to edit that novel or add a new blood test to that medical record? We send our desired edits to all the boxes, but we can’t assume reliable communication: some box’s received edits may have gaps; some boxes might miss out on other boxes’ updates; and different boxes may hear about an edit at different times. Keeping redundant data synchronized and up to date requires a delicate dance of distributed updates. AWS Aurora’s distributed protocol Grover choreographs that dance for database storage. For example, Grover’s default setting has sixfold redundancy and promises to be robust to simultaneous failure of any two out of six boxes. In Amazon’s Automated Reasoning group, we have mathematically proven that Grover’s core data-repair-and-migration protocol keeps that promise. The proof, like a Sudoku solution, can be checked without trusting the process that found it (in our case, generation by large language models). To enable automatic proof checking, we express our claims and their proofs in Lean 4, a language and toolkit for expressing and proving claims with mathematical rigor. Step 1: Initial specification of the Grover protocol in Lean 4 Our first challenge was to precisely define the Grover protocol in Lean 4. We wrote a Lean 4 template by hand, a template general enough for any distributed protocol, then had LLMs fill it in for Grover from the existing natural-language documentation. During this process, we found many ambiguities and typos in the Grover documentation that, if taken literally, would describe a protocol that can lose data. One example is a hidden assumption whose violation would sometimes cause data loss when Grover scaled to higher-than-default redundancies. The documentation authors were aware that Grover makes that assumption but forgot to record it. Our work surfaced such safety requirements and recorded them for those who will maintain and modify Grover. Formalization has therefore not only produced a verified reference algorithm on which to base future implementations but has also helped improve existing documentation. Step 2: Coevolving the proof and the specification Using the Lean 4 version of the Grover protocol, we proved that once a piece of data is safely stored, it stays safely stored through every later round of repair and reshuffling. The proof doesn't assume a particular number of boxes, so it covers whatever redundancy setting Grover runs with, not just the default six. We used an LLM to iteratively propose the Lean 4 specification of the protocol and the same LLM to attempt a proof or a counterexample for each proposal. The search usually produced a counterexample, in which case we made a minimal, most-faithful-to-documentation change to the specification to rule it out, then repeated the process. We converged to a formal protocol plus correctness proof, both in Lean 4. To check that every deviation from the documentation was indeed necessary, we automatically constructed counterexamples showing that leaving any single change out would break the associated theorems. Finally, we simplified the formal protocol from an explicit style — the style that automatic reasoning works with most easily, which spells out every transition in full — into a human-readable style, a compact notation we designed for distributed protocols, in which the whole protocol fits in one file an expert can read. We formally proved the two versions equivalent. This allows human experts on the Grover team, as ongoing work, to check that the proven protocol is indeed the intended protocol. Our proof of concept illustrates a new working method that may accelerate Amazon’s broader work on distributed protocols and strengthen the end results. Armed with automatic correctness checkers, developers can optimize aggressively and tailor to complicated customer uses, without fear that new complexity invites bugs. If we succeed in applying our automated-reasoning methods to general protocols, then developers can enhance distributed protocols at a rate that scales with their appetite for enhancement, not their appetite for risk. Acknowledgements: Alexey Gotsman, Mark Tuttle