Towards System-Oriented Formal Verification of Local-First Access Control. - Florian Jacob; Johanna Stuber; Hannes Hartenstein (CoRR, 2026)