Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2609.34881

Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking

Ioana Silaş·Adrian Crăciun
View original source ↗Read source document ↗Export metadata ↓

Abstract

In distributed systems, model checking is usually used at design time for specifying an abstract model of the system and then exhaustively checking all possible behaviors. TLA+ is commonly used in this way as a specification language, together with the TLC model checker. In this paper, we present a monitoring tool that, at its core, utilizes TLA+ specifications in a different way. The tool utilizes a TLA+ trace-checking specification to detect violations in behavior inferred from Kubernetes audit logs. Our primary use case focuses on multitenancy violations; however, the pipeline is not limited to that setting. Specifically, it demonstrates how formal reasoning can be incorporated into live Kubernetes environments to improve monitoring and correctness checking.

Explore related subjects

cs.LOcs.DC

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Ioana Silaş, Adrian Crăciun. 2026-09-28. Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking. https://doi.org/10.4204/eptcs.452.4

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Implication Problems over Positive Semirings

We study various notions of dependency in semiring team semantics. Semiring teams are essentially database relations, where each tuple is annotated with some element from a positive semiring. We consider semiring generalizations of several dependency notions from database theory and probability theory, including functional and inclusion dependencies, marginal identity, and (probabilistic) independence. We examine axiomatizations of implication problems, which are rule-based characterizations for the logical implication and inference of new dependencies from a given set of dependencies. Semiring team semantics provides a general framework, where different implication problems can be studied simultaneously for various semirings. The choice of the semiring leads to a specific semantic interpretation of the dependencies, and hence different semirings offer a way to study different semantics (e.g., relational, bag, and probabilistic semantics) in a unified framework.

cs.LO↗
arXiv2026

A programming language combining quantum and classical control

The two main notions of control in quantum programming languages are often referred to as "quantum control" and "classical control". With the latter, the control flow is based on classical information, potentially resulting from a quantum measurement, and this paradigm is well-suited to mixed state quantum computation. Whereas with quantum control, we are primarily focused on pure quantum computation and there the "control" is based on superposition. The two paradigms have not mixed well traditionally and they are almost always treated separately. In this work, we show that the paradigms may be combined within the same system. The key ingredients for achieving this are: (1) syntactically: a modality for incorporating pure quantum types into a mixed state quantum type system; (2) operationally: an adaptation of the notion of "quantum configuration" from quantum lambda-calculi, where the quantum data is replaced with pure quantum primitives; (3) denotationally: suitable (sub)categories of Hilbert spaces, for pure computation and von Neumann algebras, for mixed state computation in the Heisenberg picture of quantum mechanics.

cs.LO↗
arXiv2026

Encoder-Decoder Transformers: Logical Characterizations and Periodicity

We give logical characterizations of encoder-decoder transformers, the foundational architecture for LLMs that also sees use in various settings that benefit from cross-attention, in the practical setting of floating-point numbers and soft attention. First, we characterize such transformers via a new temporal logic that extends propositional logic with a counting global modality over the encoder input and a past modality over the decoder input, as well as via a type of distributed automata. We consider three frameworks: with and without a final softmax step in the transformer, and in the setting where each model generates tokens via autoregression. Second, we show that both autoregressive transformers and sentences of counting propositional logic - the fragment of the previous logic obtained by omitting the past modality - recognize exactly the commutative star-free languages. Finally, we find that the sequences of tokens the transformers generate are ultimately periodic (and each token appears in the period at most once). This allows us to characterize autoregressive transformers via sentences of counting propositional logic that generate tokens without autoregression, i.e., we can effectively eliminate recursion from the transformers.

cs.LO↗