Ultra-low-latency trading systems demand runtime verification (RV) that is both expressive and fast, with processing budgets measured in hundreds of nanoseconds. We present ChronosRV, a framework that compiles specifications written in a bounded fragment of Metric Temporal Logic (MTL) extended with a SERE-style (regular sequence) subset and lightweight aggregations, into highly optimized C++ monitors integrated in a zero-copy, lock-free, NUMA-aware event engine. We formalize a discrete-time, three-valued prefix semantics that supports bounded memory and robust verdicts in the presence of bounded out-of-order (OOO) arrivals via watermarks. Our synthesis pipeline maps logic to an operator network of bounded timers, counters, and small DFAs, with per-key sharding to exploit data parallelism. On synthetic workloads reflecting equity trading pipelines, ChronosRV sustains >1–4M events/s with median per-event processing in the sub-microsecond range, and detects injected violations with high accuracy under bounded OOO jitter. We provide a proof sketch of soundness and bounded completeness under watermarking, and report detailed ablations for property complexity, sharding, and OOO robustness.
Modern type-theory-based proof assistants/languages are increasingly supporting general-purpose programming, making them both practical and formally rigorous. This dual nature aligns well with the needs of safety-critical embedded system design. It is hence promising that such a language can be employed as a proper meta-language for building an embedded system design framework that integrates reasoning and programming. In this paper, we demonstrate a unified framework for synchronous embedded system design, which leverages both aspects of the quantitatively typed language Idris2, with a focus on an embedded domain-specific language (EDSL), named SynQ, in the framework. Specifically, we show that the leveraging of the expressiveness of quantitative type theory and the tagless final embedding allows synchronous systems to be properly modelled by SynQ. This then enables a systematic usage of Idris2 for facilitating both design and verification of synchronous systems, demonstrating an initial step towards a correct-by-construction embedded system design process.
Multiprecision arithmetic is required in many applications, notably safety critical areas. It carries, however, a substantial performance impact compared to fixed precision arithmetic. Since a significant part of this is due to allocation and memory fragmentation, a substantial speed up can be obtained by optimising for small numbers by storing them inline on the stack rather than on the heap. Libraries implementing such an optimisation typically fix the range of numbers considered small. However, optimal performance requires customising this range depending on the problem. The contribution of this tool paper is to introduce MPL, a library for arbitrary fixed precision and multiprecision arithmetic, which allows developers to customise the range of small numbers based on the knowledge of their problem at compile time. We experimentally demonstrate that MPL can deliver significant speed-ups when benchmarked against GMP and CLN, both running microbenchmarks on our library. MPL is released under a permissive BSD license, and we also provide a full integration of MPL with cvc5, enabling using MPL as a back end in cvc5.
This paper proposes a machine-checked and interface-based formal verification for the k-center problem. This formal architecture is built with four modules (Metric, FiniteSet, Radius, and Feasible). These modules separate the abstract metric view from graph, tree, and Euclidean backends, so that proofs can be reused across these spaces without modification. The algorithms are certificate-based. First, the greedy algorithm returns a farthest-first solution and is also a packing and covering witness. Second, the tree decision routine returns traces that show when a radius is feasible. Third, the graph backend offers multisource breadth-first search oracles that support these proofs. As a result, composable machine-checked proofs of classical results are obtained, and specialized versions for new settings are easy to add. The farthest-first constant factor approximation is formalized with a simple separation invariant. An exact tree oracle, called checkR, is given by binary search over a finite set of radii. A graph formal method is also designed that uses a packing-based witness to show that a target radius is not feasible. The greedy template is also combined with symmetric epsilon coresets, so the constant factor bound is kept under a controlled error from the coreset. For online input, a template is proposed to keep maximal packing. This template provides a radius within a factor of 2 of the best possible radius at each step. The framework is independent of one proof assistant and can be used in Lean. It is built for extension, since capacities and outliers are added by changing only the feasibility part. Low doubling and planar cases reuse the same basic lemmas, and Euclidean backends can link to tools for nets and coresets. By using one simple and witness-based template for the relation between packing and covering and for search over the radius, long approximation proofs are turned into small and verifiable pieces. These pieces can be combined to build algorithms for dynamic data, streaming data, and networked systems.
We propose Separation Logic with Heap Variables (SLHV), an extension of separation logic which introduces explicit heap variables in conjunction with separating conjunction and classical Boolean operations. We provide a decision procedure for the satisfiability of SLHV by reducing to the satisfiability of quantifier-free linear integer arithmetic. We implement a prototype solver for SLHV based on Z3, which, together with the encoding of heap-manipulating C programs as SLHV formulas, gives rise to a new bounded model checker for heap-manipulating C programs. The experimental results show the efficacy of our approach.
