pith. sign in

arxiv: 2604.23560 · v1 · submitted 2026-04-26 · 💻 cs.DC · cs.CR

Towards System-Oriented Formal Verification of Local-First Access Control

Florian Jacob , Johanna Stuber , Hannes Hartenstein This is my paper

Pith reviewed 2026-05-08 05:25 UTC · model grok-4.3

classification 💻 cs.DC cs.CR
keywords CRDTlocal-firstaccess controlByzantine fault toleranceformal verificationcapabilitieshash chroniclesVerus
0
0 comments X p. Extension

The pith

A replicated data type for simplified collaboration groups can be given precise semantics and invariants that hold under Byzantine faults.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper takes a bottom-up step toward formally verified authorization for local-first systems that must work without mutual trust among participants. It defines semantics and invariants for a replicated data type that manages simplified collaboration groups by combining capability-based access control with hash chronicles that record replication history. The model is expressed and proved inside the Rust language using the Verus verifier, so the artifact serves as both machine-checked specification and executable reference implementation at zero runtime cost. The authors report preliminary results on the simplified case and identify the increase in access-control expressiveness needed for full-scale systems such as Matrix or Keyhive.

Core claim

We contribute semantics and invariants of a replicated data type for managing simplified collaboration groups, based on capabilities for access control and hash chronicles for replication. The verification is performed in Rust using the Verus framework and the Z3 theorem prover, incurring zero runtime cost, with the goal of making the approach accessible to system engineers.

What carries the argument

The capability-based replicated data type for simplified collaboration groups, whose semantics and invariants ensure access rights are respected under replication and Byzantine faults.

If this is right

  • Access decisions can be made locally without requiring participants to trust one another.
  • Hash chronicles allow every replica to detect and reject inconsistent history without a central authority.
  • The same Rust code serves as both the formal specification and the reference implementation.
  • Extensions that add more expressive permissions can reuse the verified core while preserving the invariants.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the simplified model generalizes, the verified component could be reused as a building block in other local-first applications that face similar trust problems.
  • The same verification style could be applied directly to the replication layers of existing projects to reduce dependence on informal specifications.
  • A concrete next step would be to encode a fragment of Matrix or Keyhive permission rules inside the same framework and re-establish the invariants.

Load-bearing premise

The simplified model of collaboration groups is representative enough that its verified properties will continue to hold when the model is extended to real-world access control policies.

What would settle it

An execution trace of the data type in which a Byzantine participant grants access to an unauthorized user despite the claimed invariants.

Figures

Figures reproduced from arXiv: 2604.23560 by Florian Jacob, Hannes Hartenstein, Johanna Stuber.

Figure 1
Figure 1. Figure 1: A chat group consisting of entities𝐴, 𝐵,𝐶. (i) Entity 𝐴 adds a new message to its local chat history first, then broadcasts to 𝐵 and 𝐶. (ii) Entity 𝐶 adds a message while concurrently, 𝐵 revokes the authorization that 𝐶 utilized. Causal and Concurrent Authorisation C ?!* new events Hi! ... stored events C ?!* Hi! ... authorized events ⟶ local-first authorization? Johanna Stuber – Verification of an Authori… view at source ↗
Figure 2
Figure 2. Figure 2: Given new events and stored events only, spec￾ifications for local-first authorization define how entities independently decide authorization of each event. on delegation, revocation, and compensating actions consec￾utive to access control concurrency conflicts [26, 27]. Other work on local-first authorization usually has different as￾sumptions on Byzantine faults [26, 35], while formal work on CRDTs [1] u… view at source ↗
Figure 4
Figure 4. Figure 4: Authorization rules formalized with Verus – a function contract for the executable function log ensures that only authorized events are applied to the system state, as defined by the specification function authorizes. Pure functions deterministically derive the same out￾put given the same input, and are free of side effects. We verify strong convergence of query results by proving that all queries are tota… view at source ↗
read the original abstract

Conflict-free replicated data types (CRDTs) and the local-first concept are increasingly employed not only in small-scale collaboration systems among few users who trust each other, but also in large-scale systems, like Matrix for instant messaging and Keyhive for collaborative documents. Since mutual trust is no longer warranted, these systems require Byzantine fault tolerance and fine-grained access control. As of today, Matrix and Keyhive pair an informal specification with an unverified reference implementation. In this work, we follow a bottom-up approach towards constructing formally verified authorization algorithms for Byzantine fault-tolerant local-first systems. As intermediate target for formal verification, we contribute semantics and invariants of a replicated data type for managing simplified collaboration groups, based on capabilities for access control and hash chronicles for replication. To enable future integration into local-first systems like Matrix and Keyhive, we strive for accessibility to system engineers by using the Rust programming language for formal specification, verification, and implementation, enabled by the Verus framework using the Z3 theorem prover at zero runtime cost. We report on our experience and preliminary results following this approach, and discuss next steps towards scaling up access control expressiveness. Whether this approach can be scaled up to the complexity of real-world local-first access control systems like Matrix or Keyhive remains future work, but our findings demonstrate the potential of system-oriented formal verification with Verus.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper proposes a bottom-up, system-oriented approach to formal verification of authorization in Byzantine fault-tolerant local-first systems. As an intermediate target, it defines semantics and invariants for a simplified replicated data type managing collaboration groups, using capabilities for access control and hash chronicles for replication. The model is specified, partially verified, and implemented in Rust via the Verus framework (with Z3), and the authors report preliminary results while explicitly deferring scaling to full systems such as Matrix or Keyhive to future work.

Significance. If the invariants hold for the simplified model, the work demonstrates the practicality of embedding machine-checked verification directly in a systems language (Rust/Verus) at zero runtime cost. This lowers the barrier for distributed-systems engineers to adopt formal methods for CRDT-based access control and provides a concrete stepping stone toward verified authorization in large-scale local-first applications. The explicit acknowledgment of the preliminary scope and the focus on accessibility are strengths.

major comments (2)
  1. [Semantics and invariants section (and verification results)] The central claim rests on the contributed semantics and invariants for the simplified RDT, yet the manuscript provides only high-level descriptions without the explicit state transitions, operation definitions, or the concrete invariant formulas that were checked in Verus. This makes it impossible to evaluate whether the invariants are non-trivial or whether the verification succeeded without manual intervention.
  2. [Discussion and future work] The abstract and conclusion state that scaling to Matrix/Keyhive complexity remains future work, but the paper does not identify which specific features of the simplified model (e.g., group membership dynamics, capability revocation, or Byzantine message handling) are the primary obstacles. Without this mapping, the intermediate-target claim cannot be assessed for its utility as a foundation.
minor comments (2)
  1. A diagram or pseudocode listing the core RDT operations and the hash-chronicle structure would improve readability for systems-oriented readers.
  2. The paper should cite the Verus documentation or prior Verus case studies to contextualize the zero-runtime-cost claim.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive feedback on our manuscript. We address each of the major comments point by point below, indicating where revisions will be made to strengthen the paper.

read point-by-point responses

  1. Referee: [Semantics and invariants section (and verification results)] The central claim rests on the contributed semantics and invariants for the simplified RDT, yet the manuscript provides only high-level descriptions without the explicit state transitions, operation definitions, or the concrete invariant formulas that were checked in Verus. This makes it impossible to evaluate whether the invariants are non-trivial or whether the verification succeeded without manual intervention.

    Authors: We agree that providing more explicit details is necessary for readers to fully evaluate the contribution. The current manuscript focuses on the high-level approach and preliminary results to maintain accessibility, but we will revise the semantics and invariants section to include the explicit state transitions, operation definitions, and the concrete invariant formulas verified in Verus. This will demonstrate the non-trivial nature of the invariants and clarify the verification process without manual intervention. revision: yes

  2. Referee: [Discussion and future work] The abstract and conclusion state that scaling to Matrix/Keyhive complexity remains future work, but the paper does not identify which specific features of the simplified model (e.g., group membership dynamics, capability revocation, or Byzantine message handling) are the primary obstacles. Without this mapping, the intermediate-target claim cannot be assessed for its utility as a foundation.

    Authors: We concur that a more detailed mapping of the obstacles would better support the claim that the simplified model serves as a useful foundation. In the revised discussion and future work section, we will explicitly identify the primary obstacles, including handling dynamic group membership with capability revocation, Byzantine fault tolerance in message handling and ordering, and scaling the access control expressiveness. We will explain how the current model abstracts these aspects and outline the steps needed for extension. revision: yes

Circularity Check

0 steps flagged

No significant circularity; constructive model from standard concepts

full rationale

The paper defines a new replicated data type for simplified collaboration groups using capabilities for access control and hash chronicles for replication. It contributes semantics and invariants, implemented and verified in Verus. No equations, predictions, or derivations are present that reduce by construction to fitted parameters or self-citations. The work explicitly positions itself as an intermediate, simplified target with scaling to real systems as future work. All load-bearing steps are self-contained definitions and verifications without circular reduction to inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The model rests on standard assumptions from distributed-systems and access-control literature; no new free parameters or invented entities are introduced in the abstract.

axioms (2)
  • domain assumption CRDT convergence and conflict resolution properties hold for the replication mechanism using hash chronicles
    Invoked to ensure replicated state remains consistent across Byzantine participants.
  • domain assumption Capabilities grant fine-grained, revocable access rights that can be checked locally
    Used as the basis for the authorization rules in the group-management data type.

pith-pipeline@v0.9.0 · 5540 in / 1232 out tokens · 48418 ms · 2026-05-08T05:25:42.685746+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

40 extracted references · 19 canonical work pages

  1. [1]

    Paulo Sérgio Almeida. 2024. Approaches to conflict-free replicated data types.ACM Comput. Surv.57, 2 (Nov. 2024), 51:1–51:36. doi:10. 1145/3695249

    2024

  2. [2]

    Paulo Sérgio Almeida and Ehud Shapiro. 2025. The Blocklace: A Byzantine-repelling and Universal Conflict-free Replicated Data Type. doi:10.48550/arXiv.2402.08068arXiv:2402.08068 [cs]

    work page doi:10.48550/arxiv.2402.08068arxiv:2402.08068 2025

  3. [3]

    2026.Automerge: Version Control for Your Data.https://automerge.org/

    Automerge Contributors. 2026.Automerge: Version Control for Your Data.https://automerge.org/

    2026

  4. [4]

    Franklin, Ali Ghodsi, Joseph M

    Peter Bailis, Alan Fekete, Michael J. Franklin, Ali Ghodsi, Joseph M. Hellerstein, and Ion Stoica. 2014. Coordination Avoidance in Database Systems. 8, 3 (2014), 185–196. doi:10.14778/2735508.2735509

    work page doi:10.14778/2735508.2735509 2014

  5. [5]

    McMillan, Kedar S

    David Basin, Nate Foster, Kenneth L. McMillan, Kedar S. Namjoshi, Cristina Nita-Rotaru, Jonathan M. Smith, Pamela Zave, and Lenore D. Zuck. 2025. It takes a village: bridging the gaps between current and formal specifications for protocols.Commun. ACM68, 8 (Aug. 2025), 50–61. doi:10.1145/3706572

    work page doi:10.1145/3706572 2025

  6. [6]

    2024.Design and verification of Byzantine fault tolerant CRDTs

    Liangrun Da. 2024.Design and verification of Byzantine fault tolerant CRDTs. Master’s thesis. TUM.https://github.com/TUM- DSE/research-work-archive/blob/main/archive/2024/winter/docs/ msc_liangrun_da_design_and_verification_of_byzantine_fault_ tolerant_crdts.pdf

    2024

  7. [7]

    Kegan Dougal. 2025. Project Hydra: improving state resolution in Matrix.https://matrix.org/blog/2025/08/project-hydra-improving- state-res/

    2025

  8. [8]

    2025.Matrix in Germany.https://element

    Element Software GmbH. 2025.Matrix in Germany.https://element. io/matrix-in-germany

    2025

  9. [9]

    Element Software GmbH. 2024. NATO NI2CE Messen- ger utilises the power of decentralised communication. https://element.io/blog/nato-ni2ce-messenger-utilises-the-power- of-decentralised-communication/

    2024

  10. [10]

    Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, and Alastair R. Beresford. 2017. Verifying strong eventual consistency in distributed systems.Proceedings of the ACM on Programming Lan- guages1, OOPSLA (Oct. 2017), 1–28. doi:10.1145/3133933

    work page doi:10.1145/3133933 2017

  11. [11]

    Sergio Gusmeroli, Salvatore Piccione, and Domenico Rotondi. 2013. A Capability-Based Security Approach to Manage Access Control in the Internet of Things.Mathematical and Computer Modelling58, 5 (2013), 1189–1205. doi:10.1016/j.mcm.2013.02.006

    work page doi:10.1016/j.mcm.2013.02.006 2013

  12. [12]

    Hellerstein and Peter Alvaro

    Joseph M. Hellerstein and Peter Alvaro. 2020. Keeping CALM: When Distributed Consistency Is Easy.Commun. ACM63, 9 (2020), 72–81. doi:10.1145/3369736

    work page doi:10.1145/3369736 2020

  13. [13]

    Maurice Herlihy. 1991. Wait-Free Synchronization.ACM Transactions on Programming Languages and Systems13, 1 (1991), 124–149. doi:10. 1145/114005.102808

    work page arXiv 1991

  14. [14]

    Florian Jacob, Carolin Beer, Norbert Henze, and Hannes Hartenstein

  15. [15]

    doi:10.1109/ACCESS.2021.3058576

    Analysis of the Matrix Event Graph Replicated Data Type.IEEE Access9 (2021), 28317–28333. doi:10.1109/ACCESS.2021.3058576

    work page doi:10.1109/access.2021.3058576 2021

  16. [16]

    Florian Jacob and Hannes Hartenstein. 2024. Logical Clocks and Mono- tonicity for Byzantine-Tolerant Replicated Data Types. InProceedings of the 11th Workshop on Principles and Practice of Consistency for Dis- tributed Data. ACM, Athens Greece. doi:10.1145/3642976.3653034

    work page doi:10.1145/3642976.3653034 2024

  17. [17]

    Florian Jacob and Hannes Hartenstein. 2025. To the Best of Knowledge and Belief: On Eventually Consistent Access Control. InProceedings of the 15th ACM Conference on Data and Application Security and Privacy. Association for Computing Machinery (ACM), 107–118. doi:10.1145/ 3714393.3726520

    work page arXiv 2025

  18. [18]

    2015.A Critique of the CAP Theorem

    Martin Kleppmann. 2015.A Critique of the CAP Theorem. arXiv:1509.05393 [cs] doi:10.48550/arXiv.1509.05393

    work page doi:10.48550/arxiv.1509.05393 2015

  19. [19]

    Martin Kleppmann. 2025. Keynote: Byzantine eventual consistency and local-first access control(12th Workshop on Principles and Practice of Consistency for Distributed Data (PaPoC ’25)). ACM.https://martin. kleppmann.com/2025/03/31/papoc-keynote-byzantine.html

    2025

  20. [20]

    Martin Kleppmann. 2024. The Past, Present, and Future of Local- First. (2024).https://martin.kleppmann.com/2024/05/30/local-first- conference.html

    2024

  21. [21]

    Martin Kleppmann. 2022. Making CRDTs Byzantine fault tolerant. InProceedings of the 9th Workshop on Principles and Practice of Con- sistency for Distributed Data (PaPoC ’22). Association for Computing Machinery, New York, NY, USA, 8–15. doi:10.1145/3517209.3524042

    work page doi:10.1145/3517209.3524042 2022

  22. [22]

    Martin Kleppmann, Adam Wiggins, Peter Van Hardenberg, and Mark McGranaghan. 2019. Local-first software: you own your data, in spite of the cloud. InProceedings of the 2019 ACM SIGPLAN In- ternational Symposium on New Ideas, New Paradigms, and Reflec- tions on Programming and Software. ACM, Athens Greece, 154–178. doi:10.1145/3359591.3359737

    work page doi:10.1145/3359591.3359737 2019

  23. [23]

    Lorch, Oded Padon, and Bryan Parno

    Andrea Lattuada, Travis Hance, Jay Bosamiya, Matthias Brun, Chan- hee Cho, Hayley LeBlanc, Pranav Srinivasan, Reto Achermann, Tej Chajed, Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Oded Padon, and Bryan Parno. 2024. Verus: a practical foundation for systems verification. InProceedings of the ACM SIGOPS 30th Symposium on Operating Systems Principles. AC...

    work page doi:10.1145/3694715.3695952 2024

  24. [24]

    Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, and Chris Hawblitzel

  25. [25]

    Verus: Verifying Rust Programs using Linear Ghost Types

    Verus: verifying Rust programs using linear ghost types.Pro- ceedings of the ACM on Programming Languages7, OOPSLA1 (April 2023), 286–315. doi:10.1145/3586037

    work page doi:10.1145/3586037 2023

  26. [26]

    Matsakis and Felix S

    Nicholas D. Matsakis and Felix S. Klock. 2014. The Rust Language. InProceedings of the 2014 ACM SIGAda annual conference on High integrity language technology. ACM. doi:10.1145/2663171.2663188

    work page doi:10.1145/2663171.2663188 2014

  27. [27]

    2026.p2panda: building blocks for peer-to-peer applications.https://p2panda.org/

    p2panda Contributors. 2026.p2panda: building blocks for peer-to-peer applications.https://p2panda.org/

    2026

  28. [28]

    2024.Access control mechanisms for collaborative systems without central authority

    Pierre-Antoine Rault. 2024.Access control mechanisms for collaborative systems without central authority. Ph. D. Dissertation. Université de Lorraine.https://hal.univ-lorraine.fr/tel-05079538

    2024

  29. [29]

    Pierre-Antoine Rault, Claudia-Lavinia Ignat, and Olivier Perrin. 2023. Access Control Based on CRDTs for Collaborative Distributed Appli- cations.https://inria.hal.science/hal-04224855

    2023

  30. [30]

    Sandhu and P

    R.S. Sandhu and P. Samarati. 1994. Access Control: Principle and Practice.IEEE Communications Magazine32, 9 (1994), 40–48. doi:10. 1109/35.312842

    1994

  31. [31]

    2020.Merkle-CRDTs: Merkle-DAGs Meet CRDTs

    Hector Sanjuan, Samuli Poyhtari, Pedro Teixeira, and Ioannis Psaras. 2020.Merkle-CRDTs: Merkle-DAGs Meet CRDTs. arXiv:2004.00107 [cs] doi:10.48550/arXiv.2004.00107

    work page doi:10.48550/arxiv.2004.00107 2020

  32. [32]

    Marc Shapiro, Nuno Preguiça, Carlos Baquero, and Marek Zawirski

  33. [33]

    Conflict-free replicated data types

    Conflict-Free Replicated Data Types. InStabilization, Safety, and Security of Distributed Systems(Berlin, Heidelberg, 2011), Xavier Défago, Franck Petit, and Vincent Villain (Eds.), Vol. 6976. Springer Berlin Heidelberg, 386–400. doi:10.1007/978-3-642-24550-3_29

    work page doi:10.1007/978-3-642-24550-3_29 2011

  34. [34]

    Johanna Stuber and Florian Jacob. 2026. Towards System- Oriented Formal Verification of Local-First Access Control: Source Code.https://codeberg.org/kit-dsn/towards-formal-verification- local-first-access-control

    2026

  35. [35]

    The Matrix.org Foundation CIC. 2025. Matrix Specification v1.16. https://spec.matrix.org/v1.16/

    2025

  36. [36]

    The Matrix.org Foundation CIC. 2025. Room Version 12.https: //spec.matrix.org/v1.16/rooms/v12/

    2025

  37. [37]

    D. Turner. 2004. Total Functional Programming.JUCS - Journal of Universal Computer Science10, 7 (2004), 751–768. Issue 7. doi:10.3217/ jucs-010-07-0751

    2004

  38. [38]

    Mathias Weber, Annette Bieniusa, and Arnd Poetzsch-Heffter. 2016. Access Control for Weakly Consistent Replicated Information Systems. InSecurity and Trust Management(2016)(Lecture Notes in Computer Science). doi:10.1007/978-3-319-46598-2_6

    work page doi:10.1007/978-3-319-46598-2_6 2016

  39. [39]

    2022.Designing Data Structures for Collaborative Apps.https://mattweidner.com/2022/02/10/collaborative-data-design

    Matthew Weidner. 2022.Designing Data Structures for Collaborative Apps.https://mattweidner.com/2022/02/10/collaborative-data-design. html

    2022

  40. [40]

    2025.Keyhive: Local-first Access Control.https://www.inkandswitch.com/keyhive/notebook/

    Brooklyn Zelenka and Alex Good. 2025.Keyhive: Local-first Access Control.https://www.inkandswitch.com/keyhive/notebook/

    2025