Formally Verified Security for PQ-DAS / leanDA

Researchers report a machine-checked security proof in Lean (using mathlib and VCVio) for the cryptographic core of the PQ-DAS/leanDA post-quantum data availability sampling scheme, covering an optimized variant that replaces exact Reed–Solomon membership inside the SNARK with a probabilistic check whose randomness is Fiat–Shamir-derived from the commitment. The formalization proves perfect completeness, position-binding, and code-binding of the abstract erasure code commitment scheme via explicit reductions, with a final bound implying provable security governed by √(Q·δ) — e.g., a checker with δ≈2^-136 gives roughly 36 bits of code-binding security against adversaries making 2^64 random oracle queries. The result covers only the abstract scheme and its binding properties, not the compilation to full DAS, concrete checker instantiations, or production implementations, which still require separate treatment and audits.