pith. sign in

arxiv: 2605.31475 · v2 · pith:2TRP65UVnew · submitted 2026-05-29 · 💻 cs.DB · cs.LO

A Theoretical Study of DBLog: Certified Virtual Cuts for a Snapshot-Equivalent Replay of Live Databases

Andreas Andreakis This is my paper

Pith reviewed 2026-06-28 19:50 UTC · model grok-4.3

classification 💻 cs.DB cs.LO
keywords DBLogvirtual cutchange data capturesnapshot equivalent replayreplay certificateper-key equalitywellformed runfrontier
0
0 comments X

The pith

DBLog constructs a certified virtual cut that achieves snapshot-equivalent per-key replay of a live database without a single physical snapshot read.

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

The paper formalizes the correctness object of the DBLog change-data-capture mechanism for backfilling and streaming from a live source. It establishes that DBLog produces a finite evidence bundle called a certified virtual cut, whose replay reaches the same per-key state as the source at a chosen frontier and key scope. This equality holds for every wellformed run, and an accepted certificate evaluated against faithful source observations witnesses the cut. The work further shows two algebra facts on the same scope: cuts advance by appending the filtered faithful CDC segment between frontiers, and cuts restrict to sub-scopes. All results are conditional on the premises stated at each theorem.

Core claim

DBLog constructs a snapshot-equivalent replay certificate without requiring a single physical snapshot read. The central formal object is a certified virtual cut: a finite evidence bundle whose certified replay reaches the same per-key state as the source at a chosen frontier on a chosen key scope. The paper proves per-key replay equality for every wellformed DBLog run at its frontier and scope, and that an accepted certificate, evaluated against faithful source observation, witnesses such a run and yields a virtual cut. It also proves that on the same scope a cut advances to later frontiers by appending the scope-filtered faithful CDC segment committed in between, and that a cut restricts t

What carries the argument

The certified virtual cut, a finite evidence bundle whose certified replay equals the source per-key state at a frontier and scope.

If this is right

  • Per-key replay equality holds for every wellformed DBLog run at its frontier and scope.
  • An accepted certificate against faithful observations yields a virtual cut.
  • On the same scope a cut advances to a later frontier by appending the scope-filtered faithful CDC segment.
  • A cut on a given scope restricts to any sub-scope while preserving the equality property.

Where Pith is reading between the lines

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

  • The virtual-cut construction may apply to other chunked CDC mechanisms that interleave range scans with log reads.
  • The restriction and advancement facts could support incremental maintenance of multiple overlapping scopes in a single deployment.
  • Machine-checked proofs in Isabelle/HOL make the conditional results amenable to reuse in verified CDC implementations.

Load-bearing premise

The run must be wellformed and the source observation must be faithful for the per-key equality and certificate acceptance results to hold.

What would settle it

A concrete wellformed DBLog run at its frontier and scope where the replayed per-key state differs from the faithful source state at that frontier.

Figures

Figures reproduced from arXiv: 2605.31475 by Andreas Andreakis.

Figure 1
Figure 1. Figure 1: Theorem ladder and post-core extension map. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Two chunk reads at different source-log coordinates assemble into a replay whose state at frontier [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The DBLog mechanism walked through the running example. Source writes become [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Physical cut vs. virtual cut. Left: a physical cut requires a single source-log coordinate at which every key in scope is observed — a monolithic vertical line. DBLog does not produce one; the values shown are the counterfactual “if it did” outcome on 𝐾. Right: a virtual cut requires only that replay-at-frontier equal source-at-frontier on the chosen scope; the chunk reads (as in [PITH_FULL_IMAGE:figures/… view at source ↗
Figure 5
Figure 5. Figure 5: Anchor domain and whole-table claim scope. The four numbered conjuncts of [PITH_FULL_IMAGE:figures/full_fig_p021_5.png] view at source ↗
read the original abstract

This paper is a theoretical follow-up to the 2020 DBLog paper, which described a change-data-capture (CDC) mechanism for backfilling a downstream system from a live source database and streaming its ongoing changes, while the source keeps accepting writes. DBLog reads the table in primary-key range scans (chunks) interleaved with the source change log: watermarks locate each chunk in log order, chunk rows become refresh events, and CDC events repair stale chunk observations. The mechanism requires no table lock, no pause in writes, and no global read transaction, and is now adopted by Debezium and Apache Flink CDC. The 2020 paper described the mechanism operationally but did not formalize its correctness object. This paper formalizes that object: DBLog constructs a snapshot-equivalent replay certificate without requiring a single physical snapshot read. The central formal object is a certified virtual cut: a finite evidence bundle whose certified replay reaches the same per-key state as the source at a chosen frontier on a chosen key scope. A virtual cut is extensional: replay equality at a frontier, not a physical snapshot read, and asserts no single source timestamp across chunk rows. The paper proves per-key replay equality for every wellformed DBLog run at its frontier and scope, and that an accepted certificate, evaluated against faithful source observation, witnesses such a run and yields a virtual cut. It also proves two source-side algebra facts: on the same scope, a cut advances to later frontiers by appending the scope-filtered faithful CDC segment committed in between, and a cut restricts to sub-scopes. Each result is Conditional on premises stated where it appears. Whole-table correctness, exactly-once delivery, sink-state convergence, and transfer to named deployments are not consequences of certificate acceptance alone. All proofs are machine-checked in Isabelle/HOL.

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

0 major / 0 minor

Summary. This paper is a theoretical follow-up to the 2020 DBLog work on change-data-capture. It formalizes the correctness object as a certified virtual cut: a finite evidence bundle whose certified replay reaches the same per-key state as the source at a chosen frontier on a chosen key scope. The central results are proofs that every wellformed DBLog run achieves per-key replay equality at its frontier and scope, and that an accepted certificate evaluated against faithful source observation witnesses such a run and yields a virtual cut. Two source-side algebra facts are also proved: on the same scope a cut advances by appending the scope-filtered faithful CDC segment, and a cut restricts to sub-scopes. All results are explicitly conditional on the stated premises, whole-table correctness and exactly-once delivery are not claimed as consequences, and every proof is machine-checked in Isabelle/HOL.

Significance. If the results hold, the work supplies a machine-checked formal foundation for the snapshot-equivalent replay property of DBLog without a physical snapshot read. The Isabelle/HOL proofs constitute direct evidence that the stated theorems follow from their premises and therefore strengthen confidence in the mechanism now used by Debezium and Apache Flink CDC. The explicit separation of what certificate acceptance does and does not imply adds precision that is valuable for subsequent formal work on CDC and streaming replication.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, for recognizing the value of the machine-checked proofs, and for recommending acceptance. The explicit separation of what the results do and do not imply is intentional and we are glad it was noted as a strength.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central results (per-key replay equality and certificate acceptance) are explicitly conditional on premises such as wellformed runs and faithful observations, and are machine-checked in Isabelle/HOL. This external verification makes the derivation self-contained and independent of any self-referential definitions or fitted inputs. No load-bearing self-citation reduces the claims to prior work by the same authors; the 2020 reference is only for operational context. With only the abstract available, no equations or reductions to inputs by construction are detectable.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The central claim rests on domain assumptions about wellformed runs and faithful observations plus the newly introduced entity of the certified virtual cut; no free parameters are mentioned.

axioms (2)
  • domain assumption Wellformed DBLog run
    Per-key replay equality is asserted only for every wellformed DBLog run at its frontier and scope.
  • domain assumption Faithful source observation
    Certificate acceptance yields a virtual cut only when evaluated against faithful source observation.
invented entities (1)
  • certified virtual cut no independent evidence
    purpose: A finite evidence bundle whose certified replay reaches the same per-key state as the source at a chosen frontier on a chosen key scope.
    New formal object introduced to certify replay equality without requiring a single physical snapshot read.

pith-pipeline@v0.9.1-grok · 5842 in / 1421 out tokens · 30855 ms · 2026-06-28T19:50:15.110341+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

53 extracted references · 19 canonical work pages · 1 internal anchor

  1. [1]

    DBLog: Awatermarkbasedchange-data-captureframe- work, 2019

    Andreas Andreakis and Ioannis Papapanagiotou. DBLog: Awatermarkbasedchange-data-captureframe- work, 2019. Preprint arXiv:2010.12597 (2020)

    work page arXiv 2019

  2. [2]

    IncrementalsnapshotsinDebez- ium

    DebeziumCommunity. IncrementalsnapshotsinDebez- ium. Debezium Blog, https://debezium.io/blog/2021/ 10/07/incremental-snapshots/, 2021

    2021

  3. [3]

    Flink CDC MySQL CDC connector: How incremental snapshot reading works

    Apache Flink Community. Flink CDC MySQL CDC connector: How incremental snapshot reading works. Apache Flink CDC documentation (release-3.6), https: //nightlies.apache.org/flink/flink-cdc-docs-release- 3.6/docs/connectors/flink-sources/mysql-cdc/#how- incremental-snapshot-reading-works, 2024

    2024

  4. [4]

    DBLog: A generic change-data-capture frame- work

    Andreas Andreakis and Ioannis Papapanagiotou. DBLog: A generic change-data-capture frame- work. Netflix Tech Blog, https://netflixtechblog. com/dblog-a-generic-change-data-capture-framework- 69351fb9099b, 2019

    2019

  5. [5]

    MySQL8.0referencemanual: The binary log

    OracleCorporation. MySQL8.0referencemanual: The binary log. https://dev.mysql.com/doc/refman/8.0/en/ binary-log.html; https://dev.mysql.com/doc/refman/8.0/ en/replication-gtids.html, 2026

    2026

  6. [6]

    MariaDB knowledge base: Bi- nary log; global transaction id

    MariaDB Foundation. MariaDB knowledge base: Bi- nary log; global transaction id. https://mariadb.com/kb/ en/binary-log/; https://mariadb.com/kb/en/gtid/, 2026

    2026

  7. [7]

    Chapter 49: Logical decoding

    PostgreSQL Global Development Group. Chapter 49: Logical decoding. https://www.postgresql.org/docs/ current/logicaldecoding.html; https://www.postgresql. org/docs/current/logicaldecoding-output-plugin.html, 2026

    2026

  8. [8]

    Lightweight Asynchronous Snapshots for Distributed Dataflows

    Paris Carbone, Gyula Fóra, Stephan Ewen, Seif Haridi, and Kostas Tzoumas. Lightweight asynchronous snapshots for distributed dataflows, 2015. Preprint arXiv:1506.08603

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  9. [9]

    Time,clocks,andtheorderingofevents in a distributed system.Communications of the ACM, 21(7):558–565, 1978

    LeslieLamport. Time,clocks,andtheorderingofevents in a distributed system.Communications of the ACM, 21(7):558–565, 1978

    1978

  10. [10]

    Mani Chandy and Leslie Lamport

    K. Mani Chandy and Leslie Lamport. Distributed snap- shots: Determining global states of distributed systems. ACM Transactions on Computer Systems, 3(1):63–75, 1985

    1985

  11. [11]

    Virtual time and global states of distributed systems

    Friedemann Mattern. Virtual time and global states of distributed systems. InParallel and Distributed Algorithms, pages 215–226. North-Holland, 1989

    1989

  12. [12]

    Colin J. Fidge. Timestamps in message-passing systems that preserve the partial ordering. InProceedings of the 11th Australian Computer Science Conference (ACSC), pages 56–66, 1988

    1988

  13. [13]

    On-the-fly,incremental,consistentreadingof entire databases.Algorithmica, 1(1–4):271–287, 1986

    CaltonPu. On-the-fly,incremental,consistentreadingof entire databases.Algorithmica, 1(1–4):271–287, 1986. doi: 10.1007/BF01840448

    work page doi:10.1007/bf01840448 1986

  14. [14]

    Fernández-Moctezuma, Reuven Lax, Sam McVeety, Daniel Mills, Frances Perry, Eric Schmidt, and Sam Whittle

    Tyler Akidau, Robert Bradshaw, Craig Chambers, Slava Chernyak, Rafael J. Fernández-Moctezuma, Reuven Lax, Sam McVeety, Daniel Mills, Frances Perry, Eric Schmidt, and Sam Whittle. The dataflow model: A practical approach to balancing correctness, latency, and cost in massive-scale, unbounded, out-of-order data processing.Proceedings of the VLDB Endowment, ...

    2015

  15. [15]

    Murray, Frank McSherry, Rebecca Isaacs, MichaelIsard,PaulBarham,andMartínAbadi.Naiad: A timelydataflowsystem

    Derek G. Murray, Frank McSherry, Rebecca Isaacs, MichaelIsard,PaulBarham,andMartínAbadi.Naiad: A timelydataflowsystem. InProceedingsofthe24thACM Symposium on Operating Systems Principles (SOSP), pages 439–455, 2013. doi: 10.1145/2517349.2522738

    work page doi:10.1145/2517349.2522738 2013

  16. [16]

    All aboard the Databus! LinkedIn’s scalable consistent change data capture platform

    ShirshankaDas,ChavdarBotev,KapilSurlaker,Bhaskar Ghosh, Balaji Varadarajan, Sunil Nagaraj, David Zhang, Lei Gao, Jemiah Westerman, Phanindra Ganti, Boris Shkolnik, Sajid Topiwala, Alexander Pachev, Naveen Somasundaram, and Subbu Subramaniam. All aboard the Databus! LinkedIn’s scalable consistent change data capture platform. InProceedings of the 3rd ACM S...

    work page doi:10.1145/2391229.2391247 2012

  17. [17]

    Li, Jun Li, Evgeniy Makeev, Kowshik Prakasam, Robbert van Re- nesse, Sabyasachi Roy, Pratyush Seth, Yee Jiun Song, BenjaminWester,KaushikVeeraraghavan,andPeterXie

    Yogeshwer Sharma, Philippe Ajoux, Petchean Ang, David Callies, Abhishek Choudhary, Laurent Demailly, Thomas Fersch, Liat Atsmon Guz, Andrzej Kotulski, Sachin Kulkarni, Sanjeev Kumar, Harry C. Li, Jun Li, Evgeniy Makeev, Kowshik Prakasam, Robbert van Re- nesse, Sabyasachi Roy, Pratyush Seth, Yee Jiun Song, BenjaminWester,KaushikVeeraraghavan,andPeterXie. W...

    2015

  18. [18]

    Kafka: A distributed messaging system for log processing

    Jay Kreps, Neha Narkhede, and Jun Rao. Kafka: A distributed messaging system for log processing. In Proceedings of the NetDB Workshop, 2011

    2011

  19. [19]

    JDBC source connector for Confluent Plat- form

    Confluent. JDBC source connector for Confluent Plat- form. https://docs.confluent.io/kafka-connectors/jdbc/ current/source-connector/overview.html; https://docs. confluent.io/kafka-connectors/jdbc/current/source- connector/source_config_options.html, 2026

    2026

  20. [20]

    Junqueira, and Benjamin Reed

    Patrick Hunt, Mahadev Konar, Flavio P. Junqueira, and Benjamin Reed. ZooKeeper: Wait-free coordination for internet-scale systems. InProceedings of the USENIX Annual Technical Conference, pages 145–158, 2010. 29

    2010

  21. [21]

    Chapter 29: Logical replication and architecture

    PostgreSQL Global Development Group. Chapter 29: Logical replication and architecture. https:// www.postgresql.org/docs/current/logical-replication. html; https://www.postgresql.org/docs/current/logical- replication-architecture.html, 2026

    2026

  22. [22]

    CockroachDB changefeeds: CRE- ATE CHANGEFEED, changefeed messages, how does a changefeed work

    Cockroach Labs. CockroachDB changefeeds: CRE- ATE CHANGEFEED, changefeed messages, how does a changefeed work. https://www.cockroachlabs. com/docs/stable/create-changefeed; https://www. cockroachlabs.com/docs/stable/changefeed-messages; https://www.cockroachlabs.com/docs/stable/how-does- a-changefeed-work, 2026

    2026

  23. [23]

    AmazonWebServices.AWSdatabasemigrationservice: Full-loadandCDCtasks. https://docs.aws.amazon.com/ dms/latest/userguide/CHAP_Task.CDC.html; https: //docs.aws.amazon.com/dms/latest/userguide/CHAP_ Tasks.CustomizingTasks.TaskSettings.FullLoad.html, 2026

    2026

  24. [24]

    Datastream: Manage backfill for the objects of a stream

    Google Cloud. Datastream: Manage backfill for the objects of a stream. https://docs.cloud.google.com/ datastream/docs/manage-backfill-for-the-objects-of-a- stream; https://docs.cloud.google.com/datastream/docs/ faq; https://docs.cloud.google.com/datastream/docs, 2026

    2026

  25. [25]

    Oracle GoldenGate online migration: Ini- tial load plus CDC

    Oracle. Oracle GoldenGate online migration: Ini- tial load plus CDC. https://docs.oracle.com/en- us/iaas/database-migration/doc/set-oracle-goldengate- online-migrations.html; https://blogs.oracle.com/ dataintegration/online-migration-leveraging-oracle- goldengate, 2026

    2026

  26. [26]

    Striim: Initial-load and CDC replication

    Striim. Striim: Initial-load and CDC replication. https: //www.striim.com/docs/en/getting-started.html; https: //www.cockroachlabs.com/docs/stable/striim, 2026

    2026

  27. [27]

    Materialize PostgreSQL CDC source: Ingest data

    Materialize. Materialize PostgreSQL CDC source: Ingest data. https://materialize.com/docs/ingest- data/postgres/; https://materialize.com/docs/ingest- data/postgres/postgres-debezium/, 2026

    2026

  28. [28]

    Lakeflow declarative pipelines: Change data capture and snapshots / AUTO CDC apis

    Databricks. Lakeflow declarative pipelines: Change data capture and snapshots / AUTO CDC apis. https:// docs.databricks.com/aws/en/ldp/what-is-change-data- capture; https://docs.databricks.com/aws/en/ldp/cdc, 2026

    2026

  29. [29]

    What is change data capture (CDC)? – SQL Server

    Microsoft. What is change data capture (CDC)? – SQL Server. https://learn.microsoft.com/en-us/sql/relational- databases/track-changes/about-change-data-capture- sql-server, 2025

    2025

  30. [30]

    ARIES: A transaction recovery method supporting fine- granularity locking and partial rollbacks using write-ahead logging.ACM Transactions on Database Systems, 17(1):94–162, 1992

    C.Mohan,DonHaderle,BruceLindsay,HamidPirahesh, and Peter Schwarz. ARIES: A transaction recovery method supporting fine- granularity locking and partial rollbacks using write-ahead logging.ACM Transactions on Database Systems, 17(1):94–162, 1992. doi: 10. 1145/128765.128770

    work page arXiv 1992

  31. [31]

    Contin- uous archiving and point-in-time recovery (PITR)

    PostgreSQL Global Development Group. Contin- uous archiving and point-in-time recovery (PITR). https://www.postgresql.org/docs/current/continuous- archiving.html, 2026

    2026

  32. [32]

    Abadi, and AlexanderThomson.Low-overheadasynchronouscheck- pointinginmain-memorydatabasesystems

    Kun Ren, Thaddeus Diamond, Daniel J. Abadi, and AlexanderThomson.Low-overheadasynchronouscheck- pointinginmain-memorydatabasesystems. InProceed- ings of the 2016 ACM SIGMOD International Confer- ence on Management of Data, pages 1539–1551, 2016. doi: 10.1145/2882903.2915966

    work page doi:10.1145/2882903.2915966 2016

  33. [33]

    InProceedings of the 1995 ACM SIGMOD International Conference on Management of Data, pages 1–10, 1995

    Hal Berenson, Phil Bernstein, Jim Gray, Jim Melton, ElizabethO’Neil,andPatrickO’Neil.AcritiqueofANSI SQL isolation levels. InProceedings of the 1995 ACM SIGMOD International Conference on Management of Data, pages 1–10, 1995. doi: 10.1145/223784.223785

    work page doi:10.1145/223784.223785 1995

  34. [34]

    General- izedisolationleveldefinitions.InProceedingsofthe16th International Conference on Data Engineering (ICDE), pages 67–78, 2000

    AtulAdya,BarbaraLiskov,andPatrickO’Neil. General- izedisolationleveldefinitions.InProceedingsofthe16th International Conference on Data Engineering (ICDE), pages 67–78, 2000. doi: 10.1109/ICDE.2000.839388

    work page doi:10.1109/icde.2000.839388 2000

  35. [35]

    Using oracle flashback technology: Flash- back query / AS OF SCN

    Oracle. Using oracle flashback technology: Flash- back query / AS OF SCN. https://docs.oracle.com/ en/database/oracle/oracle-database/19/adfns/flashback. html, 2026

    2026

  36. [36]

    gh-ost: GitHub’s online schema-migration tool for MySQL

    GitHub. gh-ost: GitHub’s online schema-migration tool for MySQL. https://github.com/github/gh-ost; https://github.blog/news-insights/company-news/gh- ost-github-s-online-migration-tool-for-mysql/, 2016

    2016

  37. [37]

    Online, asynchronous schema change in F1.Proceedings of the VLDB Endowment, 6(11): 1045–1056, 2013

    Ian Rae, Eric Rollins, Jeff Shute, Sukhdeep Sodhi, and Radek Vingralek. Online, asynchronous schema change in F1.Proceedings of the VLDB Endowment, 6(11): 1045–1056, 2013. doi: 10.14778/2536222.2536230

    work page doi:10.14778/2536222.2536230 2013

  38. [38]

    SLSM: An efficient strategy for lazy schema migra- tion on shared-nothing databases, 2024

    Tianxun Hu, Tianzheng Wang, and Qingqing Zhou. SLSM: An efficient strategy for lazy schema migra- tion on shared-nothing databases, 2024. Preprint arXiv:2404.03929

    work page arXiv 2024

  39. [39]

    The existence of refinementmappings.TheoreticalComputerScience,82 (2):253–284, 1991

    Martín Abadi and Leslie Lamport. The existence of refinementmappings.TheoreticalComputerScience,82 (2):253–284, 1991. doi: 10.1016/0304-3975(91)90224- P

    work page doi:10.1016/0304-3975(91)90224- 1991

  40. [40]

    Proof-carryingcode

    GeorgeC.Necula. Proof-carryingcode. InProceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 106–119, 1997. doi: 10.1145/263699.263712. 30

    work page doi:10.1145/263699.263712 1997

  41. [41]

    Trans- lation validation

    Amir Pnueli, Michael Siegel, and Eli Singerman. Trans- lation validation. InTools and Algorithms for the Con- structionandAnalysisofSystems(TACAS),volume1384 ofLecture Notes in Computer Science, pages 151–166,

  42. [42]

    doi: 10.1007/BFb0054170

    work page doi:10.1007/bfb0054170

  43. [43]

    Donaldson, John Wickerson, and Manuel Rigger

    Jack Clark, Alastair F. Donaldson, John Wickerson, and Manuel Rigger. Validating database system isolation level implementations with version certificate recovery. InProceedings of the Nineteenth European Conference on Computer Systems (EuroSys), pages 754–768, 2024. doi: 10.1145/3627703.3650080

    work page doi:10.1145/3627703.3650080 2024

  44. [44]

    ShabnamGhasemirad,SiLiu,ChristophSprenger,Luca Multazzu, and David A. Basin. VerIso: Verifiable isola- tion guarantees for database transactions.Proceedings of the VLDB Endowment, 18(5):1362–1375, 2025. doi: 10.14778/3718057.3718065

    work page doi:10.14778/3718057.3718065 2025

  45. [45]

    seL4: Formal verification of an OS kernel

    Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, DavidCock, PhilipDerrin, DhammikaElka- duwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. seL4: Formal verification of an OS kernel. InProceed- ings of the 22nd ACM Symposium on Operating Systems Principles (SOSP), pages 207–220, 2009

    2009

  46. [46]

    Formalverificationofarealisticcompiler

    XavierLeroy. Formalverificationofarealisticcompiler. Communications of the ACM, 52(7):107–115, 2009

    2009

  47. [47]

    Addison-Wesley, 2002

    Leslie Lamport.Specifying Systems: The TLA+ Lan- guage and Tools for Hardware and Software Engineers. Addison-Wesley, 2002. ISBN 978-0-321-14306-8

    2002

  48. [48]

    Verdi: Aframeworkforimplementingandformally verifyingdistributedsystems

    JamesR.Wilcox,DougWoos,PavelPanchekha,Zachary Tatlock,XiWang,MichaelD.Ernst,andThomasAnder- son. Verdi: Aframeworkforimplementingandformally verifyingdistributedsystems. InProceedingsofthe36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 357–368,

  49. [49]

    doi: 10.1145/2737924.2737958

    work page doi:10.1145/2737924.2737958

  50. [50]

    Lorch, Bryan Parno, Michael L

    ChrisHawblitzel,JonHowell,ManosKapritsos,JacobR. Lorch, Bryan Parno, Michael L. Roberts, Srinath Setty, and Brian Zill. IronFleet: Proving practical distributed systems correct. InProceedings of the 25th Symposium on Operating Systems Principles (SOSP), pages 1–17,

  51. [51]

    doi: 10.1145/2815400.2815428

    work page doi:10.1145/2815400.2815428

  52. [52]

    Alloy: A lightweight object modelling notation.ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002

    Daniel Jackson. Alloy: A lightweight object modelling notation.ACM Transactions on Software Engineering and Methodology (TOSEM), 11(2):256–290, 2002. doi: 10.1145/505145.505149

    work page doi:10.1145/505145.505149 2002

  53. [53]

    A Theoretical Study of DBLog

    Andreas Andreakis. DBLog_Virtual_Cuts: Is- abelle/HOL formal development for “A Theoretical Study of DBLog”, 2026. URL https://doi.org/10.5281/ zenodo.20389697. Software, BSD 3-Clause License. 31

    2026