A data availability proof checked by a machine

leanDA is a post-quantum data availability sampling scheme built from Reed-Solomon codes, hash-based commitments and the LeanVM proof system. On 18 August its author, posting as b-wagn, published a machine-checked security proof of its cryptographic core, written in Lean with mathlib and the VCVio library.

Three properties are formalised and proved: completeness, position-binding, and code-binding — the last both modularly and with explicit bounds. The notions follow the Foundations of DAS paper rather than being invented for the occasion.

It covers the shortcut, not the textbook version

The part that matters is which variant was verified. leanDA does not prove exact Reed-Solomon membership inside the SNARK; it runs a cheap probabilistic membership check whose randomness comes from the commitment by Fiat-Shamir, outside the SNARK. That substitution is what makes the scheme affordable, and it is exactly the kind of optimisation where a paper proof quietly stops applying.

The difficulty the author names is the interplay of random oracles, SNARKs and rewinding. The resulting bound is explicit: an adversary making Q random oracle queries is limited by knowledge soundness error, plus position-binding error, plus a term in √(Q·δ), where δ is the code checker's soundness parameter.

The author notes AI assistance in translating to Lean. That is worth stating plainly rather than glossing: the machine checks the proof either way, which is the point of doing it in Lean at all.