Linear types for large-scale systems verification

on YouTube ↗32m

" summary

Integrates linear Dafny with Dafny's SMT backend to push memory reasoning into the type system while keeping SMT for heap invariants; implements borrowing/inout updates, linear regions and ref_cell-backed heaps to hide modifies clauses. Converts a 24K-line verified storage system (very better KV) so 91% of code uses linear types and 9% uses SMT heap reasoning, cutting proof lines by 28% and total verification time by 30%.

AI-written summary · about

" chapters (8)

1. 0:00Start
2. 1:33Challenges in SMT memory reasoning with dynamic frames (Dafny)
3. 4:59Dynamic frames address potential aliasing
4. 7:07Linear Dafny
5. 7:55Variable usages
6. 13:12Non-linear data inside linear data
7. 17:56Linear data inside non-linear data
8. 18:53Formalization and soundness proof