For over half a century, the core paradigm of query optimization has been defined by a monotonic, scalar minimization convergence model aimed at suppressing computational resource consumption. This paper presents a radical paradigm shift that fundamentally subverts this traditional framework by establishing the Axiomatic Topological Inverse Query and Complexity Maximization Theory (ATIQ-CMT). Instead of pursuing local or global minima within discrete equivalence graphs, we reconstruct the relational algebra space into a non-Hausdorff, locally compact topological space governed by five foundational axioms. By introducing the Inverse Lipschitz Affine Expansion Mapping (ILAEM) under operator braid transformations, we demonstrate how compact query plans can be inversely dilated into divergent flows across high-dimensional complex affine varieties, creating irreversible mathematical obstructions for traditional gradient-based cost models. To maximize computational complexity natively, we execute a non-commutative extension of the relational algebra core via algebraically twisted join operators embedded in infinite-dimensional Lie algebras, effectively destroying the classic commutative-associative symmetry. We further inject un-decidable Diophantine predicates and 3-SAT arithmetical homomorphic graphs as computational obstructions, rigorously proving a non-polynomial exponential lower bound for physical query execution times. Utilizing sheaf theory and de Rham cohomology on chain complexes, we provide a definitive topological proof that the absolute semantic integrity of the query remains invariant throughout this chaotic dilation. Finally, we formulate a deterministic chaotic operator execution flow driven by high-order Lorenz mappings, maximizing the algebraic Shannon entropy of intermediate states. ATIQ-CMT bridges declarative relational logic and high-level structural topology, unlocking revolutionary potentials in zero-knowledge proof circuit synthesis, active cybersecurity defense, and the theoretical computational limits of neuro-symbolic and quantum systems.
Omer Aziz, Muhammad Shoaib Farooq, Adel Khelifi, Abdullah Khalid Omer
<title>Abstract</title> The digital preservation of cultural heritage has advanced considerably through blockchain technologies , offering secure, immutable, and decentralized management of museum records. However, traditional blockchain frameworks suffer from scalability limitations, leading to high transaction costs, network congestion, and inefficient resource utilization—particularly in virtual museum environments with dynamic user activity. To address these challenges, we propose VERAONET (Virtual Ecosystem for Rewards and Archaeological Operations Network), a novel Layer-2 blockchain framework designed specifically for digital heritage applications. VERAONET introduces a pluggable consensus architecture, enabling dynamic switching between Proof of Work (PoW), Adjustable PoW (APoW), Proof of Stake (PoS), and Delegated Proof of Stake (DPoS) mechanisms in response to real-time network conditions. The framework was evaluated in two experimental environments: a Ganache-based local simulation (10–500 users) and a Geth virtual testbed (50–10,000 users). Results indicate that PoS and DPoS significantly outperformed PoW and APoW under high-load conditions, reducing latency, gas consumption, and chain bloat. Conversely, PoW and APoW proved effective in low-traffic, high-security scenarios. The adaptive consensus algorithm enhanced transaction finality and resource efficiency, demonstrating strong suitability for dynamic virtual museum ecosystems. VERAONET thus provides a scalable, sustainable, and cost-effective blockchain infrastructure tailored for cultural heritage preservation. Future work will focus on integrating AI-driven optimizations, supporting cross-chain interoperability, and embedding decentralized governance models.
WebAssembly linear memory is an untyped byte array shared across module boundaries. When independently compiled modules — potentially from different source languages — read and write the same memory regions, no existing type system covers the cross-module interface. We present typed-wasm, a type system that applies a 12-level progressive type safety framework, originally developed for database query languages, to Wasm linear memory. The system treats contiguous memory segments as typed region schemas and load/store operations as typed projections verified against those schemas at compile time. We formalise the system in Idris 2 using Quantitative Type Theory (QTT), providing proofs of bounds safety, aliasing freedom, effect purity, lifetime validity, linearity, cost boundedness, and epistemic freshness — all erased before code generation, yielding zero runtime overhead. Our principal contribution is multi-module schema agreement: a static verification that independently compiled Wasm modules agree on the layout, types, alignment, and invariants of shared memory regions — a property that no source-level type system, and no existing Wasm proposal, can express. We further extend the framework with two novel levels: tropical cost-tracking (Level 11), which proves that memory access patterns have bounded cost via a min-plus semiring, and epistemic safety (Level 12), which prevents modules from acting on stale knowledge of shared state.
Este artigo analisa o design de contratos inteligentes orientados a eventos como estratégia para maximizar a eficiência de indexação off‑chain em protocolos Web3. Em plataformas como Ethereum, eventos são registrados como logs com topics indexados, permitindo que indexadores filtrem rapidamente transações relevantes sem precisar reexecutar o estado completo do contrato, o que torna a indexação por eventos uma abordagem muito mais eficiente do que consultas frequentes ao estado on‑chain via eth_call. Frameworks de indexação como The Graph organizam esses eventos em subgraphs, definidos por manifests que especificam quais contratos e eventos acompanhar, e por esquemas que mapeiam logs para entidades armazenadas em bancos de dados otimizados para consulta via GraphQL. Boas práticas de desenvolvimento orientado a eventos recomendam projetar contratos de modo que toda transição de estado relevante para a aplicação gere um evento completo (com dados suficientes para reconstruir o contexto off‑chain), reduzindo a necessidade de chamadas adicionais à cadeia, o que melhora desempenho de indexing e diminui custos de infraestrutura. Técnicas como uso de entidades imutáveis em subgraphs, cache inteligente de eth_call e cálculo de derivadas off‑chain a partir de eventos (em vez de leitura repetida de storage) podem acelerar indexação e consultas em ordens de grandeza, especialmente em cenários de histórico extenso e baixa densidade de eventos relevantes. Conclui‑se que contratos orientados a eventos, aliados a arquiteturas de indexação especializadas, são fundamentais para tornar dados on‑chain consultáveis em escala, suportando experiências de usuário ricas e composabilidade DeFi com menor custo operacional.<br>
Transaction flow networks are crucial in detecting illicit activities such as wash trading, credit card fraud, cashback arbitrage fraud, and money laundering. Our collaborator, Grab, a leader in digital payments in Southeast Asia, faces increasingly sophisticated fraud patterns in its transaction flow networks. In industry settings such as Grab's fraud detection pipeline, identifying fraudulent activities heavily relies on detecting dense flows within transaction networks. Motivated by this practical foundation, we propose theS-T densest flow(STDF) query. Given a transaction flow networkG, a source setS, a sink setT, and a size thresholdk, the query outputs subsets$S^{\prime}\subseteq S$and$T^{\prime}\subseteq T$such that the maximum flow from$S^{\prime}$to$T^{\prime}$is densest, with$\vert S^{\prime}\cup T^{\prime}\vert\geq k$. Recognizing the NP-hardness of the STDF query, we develop an efficient divide-and-conquer algorithm,$\mathsf{Conan}$. Driven by industry needs for scalable and efficient solutions, we introduce an approximate flow-peeling algorithm to optimize the performance of$\mathsf{Conan}$, enhancing its efficiency in processing large transaction networks. Our approach has been integrated into Grab's fraud detection scenario, resulting in significant improvements in identifying fraudulent activities. Experiments show that$\mathsf{Conan}$, outperforms baseline methods by up to three orders of magnitude in runtime and more effectively identifies the densest flows. We showcase$\mathsf{Conan}$'s applications in fraud detection on transaction flow networks from our industry partner, Grab, and on non-fungible tokens (NFTs).
Traditional Byzantine Fault Tolerance (BFT) consensus algorithms effectively tolerate node behavioral faults but lack the ability to verify the quality of input data. This makes them vulnerable to security risks from low-quality or “compliant yet malicious” data in data-driven applications. To address this gap, we propose a Data-Quality-Driven Byzantine Fault Tolerance algorithm based on Zero-Knowledge Proofs, called Q-BFT. The algorithm introduces a “quality gate” prior to classic BFT consensus—an on-chain verification phase that uses zk-SNARKs and is automated by smart contracts. This allows nodes to prove in zero-knowledge that their data meets predefined thresholds for accuracy, completeness, and consistency without exposing raw data. Passing the verification becomes a prerequisite for joining consensus voting. We design a two-layer smart contract architecture that efficiently orchestrates off-chain proof generation and on-chain automated verification. Experiments show that in a 100-node network with 30% malicious nodes, Q-BFT improves the consensus success rate from 41.5% (with PBFT) to 96.4%, while maintaining federated learning global model accuracy above 88%, in contrast to the model collapse (< 20% accuracy) observed under a traditional BFT protocol. The system achieves an average verification latency below 0.65 s and a throughput of 735 TPS(Transactions Per Second), striking an effective balance among security, privacy preservation, and operational efficiency. By enforcing privacy-preserving data quality verification as a mandatory gate before consensus, Q-BFT thus provides a high-assurance foundation for data-sensitive and privacy-critical applications. It addresses the core vulnerability of traditional consensus in scenarios like federated learning, where model integrity depends on participant data quality, and trustworthy data markets, where transaction validity requires assured data authenticity without exposing the data itself.
For most distributed financial systems, the constraints imposed by the CAP (Consistency, Availability, Partition Tolerance) theorem must be reconciled against the ordering constraints needed to satisfy regulatory requirements and meet the performance requirements of real-time transaction processing. This paper presents the Temporal Sequence Barrier consistency model for asynchronous high-throughput ledger systems. Combining logical vector clocks with epoch-based orchestration patterns imposes a strict causal ordering of events across multiple geographic regions without sacrificing availability. Its database-centric architecture allows stateful routing and selective replication of entities in order to achieve linearizability of causally related transactions while allowing independent sets of entities to be processed in parallel. We provide a detailed evaluation that shows that we can provide causal consistency at latency bounds equal to or better than existing systems using clever buffering and adaptive timeouts, while also addressing the classic challenges in distributed transaction management and operator complexity.
Transaction flow networks are crucial in detecting illicit activities such as wash trading, credit card fraud, cashback arbitrage fraud, and money laundering. \revise{Our collaborator, Grab, a leader in digital payments in Southeast Asia, faces increasingly sophisticated fraud patterns in its transaction flow networks. In industry settings such as Grab's fraud detection pipeline, identifying fraudulent activities heavily relies on detecting dense flows within transaction networks. Motivated by this practical foundation,} we propose the \emph{\(S\)-\(T\) densest flow} (\SDMF{}) query. Given a transaction flow network \( G \), a source set \( \Src \), a sink set \( \Dst \), and a size threshold \( k \), the query outputs subsets \( \Src' \subseteq \Src \) and \( \Dst' \subseteq \Dst \) such that the maximum flow from \( \Src' \) to \( \Dst' \) is densest, with \(|\Src' \cup \Dst'| \geq k\). Recognizing the NP-hardness of the \SDMF{} query, we develop an efficient divide-and-conquer algorithm, CONAN. \revise{Driven by industry needs for scalable and efficient solutions}, we introduce an approximate flow-peeling algorithm to optimize the performance of CONAN, enhancing its efficiency in processing large transaction networks. \revise{Our approach has been integrated into Grab's fraud detection scenario, resulting in significant improvements in identifying fraudulent activities.} Experiments show that CONAN outperforms baseline methods by up to three orders of magnitude in runtime and more effectively identifies the densest flows. We showcase CONAN's applications in fraud detection on transaction flow networks from our industry partner, Grab, and on non-fungible tokens (NFTs).
Sungmin Lee, Kichang Lee, Gyeongmin Han, JeongGil Ko
Many location-based services rely on a point-in-polygon test ( PiP ), checking whether a point or a trajectory lies inside a geographic zone. Since geometric operations are expensive in zero-knowledge proofs, privately performing the PiP test is challenging. In this paper, we answer the research questions of how different ways of encoding zones affect accuracy and proof cost by exploiting grid-based lookup tables under a fixed STARK execution model. Beyond a Boolean grid-based baseline that marks cells as in- or outside, we explore a distance-aware encoding approach that stores how far each cell is from a zone boundary and uses interpolation to reason within a cell. % Our experiments on real-world data demonstrate that the proposed distance-aware approach achieves higher accuracy on coarse grids with only a moderate verification overhead, making zone encoding the key lever for efficient zero-knowledge spatial checks. Our experiments on real-world data demonstrate that the proposed distance-aware approach achieves higher accuracy on coarse grids (max. % 60%p 60%p accuracy gain) with only a moderate verification overhead (approximately 1.4×), making zone encoding the key lever for efficient zero-knowledge spatial checks.
Blockchain is often referred to as a Distributed Ledger Technology or DLT. One could argue that there are two-components to ledger-keeping: the ledger itself (the data) and the process of “keeping” it or amending the data.
Jordan, Herbert, Jezek, Kamil, Subotic, Pavle, Scholz, Bernhard
The State Database of a blockchain stores account data and enables authentication. Modern blockchains use fast consensus protocols to avoid forking, improving throughput and finality. However, Ethereum's StateDB was designed for a forking chain that maintains multiple state versions. While newer blockchains adopt Ethereum's standard for DApp compatibility, they do not require multiple state versions, making legacy Ethereum databases inefficient for fast, non-forking blockchains. Moreover, existing StateDB implementations have been built on key-value stores (e.g., LevelDB), which make them less efficient. This paper introduces a novel state database that is a native database implementation and maintains Ethereum compatibility while being specialized for non-forking blockchains. Our database delivers ten times speedups and 99% space reductions for validators, and a threefold decrease in storage requirements for archive nodes.
Today's distributed payment systems must function correctly despite the inherent presence of asynchrony, partial failures, and third-party integrations. Unlike typical RPC-based workflows used in software development, payment flows are heavily influenced by external delays, retries, timeouts, and nondeterministic state changes across multiple systems of record. A fault-tolerant ledger abstraction that decouples payment intent from execution enables safe retries and supports service events that may arrive out of order. Correctness and safety depend on distributed transaction constructs such as outbox/inbox patterns, compensation workflows, and time-bounded state machines to contain the effects of race conditions, double submissions, and ambiguous or indeterminate outcomes. A declarative reconciliation framework continuously verifies consistency between internal and external systems, enabling real-time anomaly detection and facilitating orchestration and recovery. These pragmatic engineering approaches, validated through simulations and production-level benchmarks, offer guidance for building resilient payment infrastructures in naturally asynchronous and failure-prone environments.
The Monty-Hall (parameterized strategist-host) Theorem along with a constructive proof is presented, by solving the corresponding Monty-Hall Problem, wherein the host plays a parameterized strategy on the guest. It establishes the limits on the range of values for the probability of winning the prize. Eight extreme strategies (corresponding to the set of extreme values for the three perturbation parameters) have been well characterized. It is shown that there does not exist any strategy wherein a switched-choice will always (irrespective of the placement of the prize and irrespective of the initial-choice of the guest) lead to an enhancement in the chances of winning the prize. The classical Monty-Hall Problem is a special case with zero-value for each of the three perturbation parameters. This paper is an attempt to correct the errors (of long-standing historical significance) in the application of statistical methodology in solving the classical Monty-Hall Problem - one of them being the erroneous use of conditional probabilities for updating the knowledge to facilitate the decision-making by the guest, based on the information about a losing-choice, which itself is dependent on the initial-choice of the guest. Similar scenarios in data science, machine learning & artificial intelligence can have serious far-reaching consequences.
Decentralized exchanges (DEXs) form a cornerstone of the decentralized finance (DeFi) ecosystem, processing token trades worth billions of dollars daily. Yet, a significant fraction of these trades are suboptimal: alternative routing paths could yield more target tokens. Addressing this inefficiency is both practically urgent and theoretically compelling. Building on the linear line-graph-based routing method of Zhang et al. (2025), we propose three key extensions that better capture real-world trading complexity. First, we introduce a breadth-first search (BFS) link iteration rule that reduces computational cost and average execution time without sacrificing profitability. Second, we design a route-splitting strategy that divides large trades into smaller ones, alleviating price slippage and increasing average trader profits, albeit at the cost of higher computational overhead. Third, we generalize the method beyond a single DEX to a multi-DEX aggregator setting, reflecting actual trading environments. Using empirical data from Uniswap V2 and Sushiswap V2, we demonstrate that these extensions substantially improve both computational efficiency and profitability, establishing a foundation for future routing enhancements.
The use of Enterprise Data Warehouse (EDWs) has been experienced as the analytical backbone of risk management, financial reporting and regulatory reporting of the data in very regulated sectors like banking, insurance, and capital markets. They were based on batch-oriented Extract Transform Load (ETL) paradigms, tight coupled schema and monolithic governance models that are better suited to stability than agility. Nevertheless, the increasing regulatory complexity, impacts of the near-real time risk visibility requirements, and increasing cost of infrastructure have emanated inherent weaknesses of the legacy EDW architectures. At the same time, the emergence of hybrid cloud platforms, scalable object storage, distributed query engines, and workflow orchestration system has made it possible to make the paradigm shift toward Extract–Load–Transform (ELT), domain-driven data products, and decentralized ownership models. In spite of these developments, in numerous organizations, the pressure to modernize reporting pipes based on strong backward compatibility criteria, audit limitations and the operational risks of massive data migrations makes this a challenge. This paper gives a detailed blueprint of modernization in the process of moving the old EDW centric ETL architectures to the hybrid cloud ELT platforms to suit the risk, finance, and regulatory reporting. Its proposed solution integrates domain-driven data products and ELT pushdown transformations orchestrating control planes and explicit data contracts that is applied in an incremental fashion with a strangler pattern. The framework focuses on retrogressively compatible schemas, reconcilability determinacy, the rollback safety nets, and regulated cutover plans to provide continuous regulatory compliance. Using a well-organized migration roadmap, cost and performance metrics and an official risk register, the paper will show how organizations can shorten report delivery cycles, enhance service-level agreement (SLA) compliance and minimize the overall cost of ownership without sacrificing auditability and strict governance. The findings have shown that hybrid cloud ELT systems may cut the latency in report by more than 40%, cut compute expenditure by up to 35, and become much more responsive to regulatory cases without infection of information integrity or resilience.
To cater to the needs of (Zero Knowledge) proofs for (mathematical) proofs, we describe a method to transform formal sentences in 2x2-matrices over multivariate polynomials with integer coefficients, such that usual proof-steps like modus-ponens or the substitution are easy to compute from the matrices corresponding to the terms or formulas used as arguments. By evaluating the polynomial variables in random elements of a suitably chosen finite field, the proof is replaced by a numeric sequence. Only the values corresponding to the axioms have to be computed from scratch. The values corresponding to derived formulas are computed from the values corresponding to their ancestors by applying the homomorphic properties. On such sequences, various Zero Knowledge methods can be applied.
Financial institutions increasingly rely on sophisticated database architectures to gain competitive advantages in high-frequency trading and analytics environments. This article examines optimal database technologies for financial applications, comparing in-memory, columnar, time-series, and distributed ledger architectures across standardized financial workloads. Multiple case studies demonstrate how different architectures excel in specific contexts: in-memory processing delivers superior performance for order processing, columnar storage enables faster analytical queries for market analysis, while time-series databases efficiently handle pattern recognition for fraud detection. Performance bottlenecks, consistency trade-offs, regulatory compliance challenges, and security considerations are explored in depth. The results indicate that no single architecture provides optimal performance across all financial application requirements; instead, financial institutions must select technologies based on specific use cases, with heterogeneous architectures often delivering superior results. The article concludes by examining emerging technologies with potential to transform financial database landscapes, including persistent memory, hardware acceleration, specialized indexing structures, AI-integrated engines, and hybrid blockchain solutions.
This work explores the integration of Relationalmodel Multi-Agent System (RMAS) with Zero-Knowledge Proofs (ZKP) to enable verifiable computations in distributed systems. RMAS, based on relational algebra, simplifies multi-agent computations using active databases. By combining RMAS with zkSNARKs (Zero-Knowledge Succinct Non-Interactive Arguments of Knowledge), we provide a framework for privacy-preserving and verifiable operations in Cyber-Physical Systems (CPS). We demonstrate how SQL (Structured Query Language) queries can be transformed into relational algebra and compiled into ZoKrates Domain-Specific Language (DSL) for ZKP generation. A case study in sustainable food supply chains highlights the approach's potential to enhance trust, scalability, and security in collaborative environments.
The increasing demand for scalable blockchain has driven research into parallel execution models for smart contracts. Crystality is a novel smart contract programming language designed for parallel Ethereum Virtual Machines (EVMs), enabling fine-grained concurrency through Programmable Contract Scopes and Asynchronous Functional Relay. This paper presents the first formal structural operational semantics for Crystality, providing a rigorous framework to reason about its execution. We mechanize the syntax and semantics of Crystality in the theorem-proving assistant Coq, enabling formal verification of correctness properties. As a case study, we verify a simplified token transfer function, demonstrating the applicability of our semantics in ensuring smart contract correctness. Our work lays the foundation for formally verified parallel smart contracts, contributing to the security and scalability of blockchain systems.
Abstract This paper introduces semi-competitive differential game logic $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , which enables verification of safety-critical applications that involve interactions between two agents. In $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> , these interactions are specified as games on hybrid systems with two players that may collaborate with each other when helpful and may compete when necessary. The players in the hybrid games of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> have individual goals that may overlap, leading to nonzero-sum games. This makes $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> especially well-suited for verifying situations where players, e.g., share safety objectives but otherwise pursue different goals, so that zero-sum assumptions lead to overly conservative results. Additionally, $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> solves the subtlety that even though each player may benefit from knowledge of the other player’s goals, e.g., concerning shared safety objectives, unsafe situations might still occur if every player were to mutually assume the other player would act to avoid unsafety. The syntax and semantics, as well as a sound and relatively complete proof calculus are presented for $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> . The relationship between $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> and zero-sum differential game logic $$\textsf {dG}\mathcal {L}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:mi>L</mml:mi> </mml:mrow> </mml:math> is discussed and the purpose of $$\textsf {dG}\mathcal {L}_{sc}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>dG</mml:mi> <mml:msub> <mml:mi>L</mml:mi> <mml:mrow> <mml:mi>sc</mml:mi> </mml:mrow> </mml:msub> </mml:mrow> </mml:math> illustrated in a canonical example.
Security protocols, protocols to achieve consensus, those for maintaining memory consistency and coherence, distributed ledgers, multi-party computation, and many similar software systems are examples of distributed message-passing based computation. Ensuring correctness of such distributed systems is a challenging problem for many automatic verification approaches. The deductive verification approach for reasoning about such systems involves computing a program invariant, i.e., an expression evaluates to true for every reachable program state. Several approaches for synthesizing invariants are dynamic, i.e., runs of the program and ancillary information such as target safety properties are used to learn an invariant expression. However, most existing approaches invoke a model checker (or a theorem prover) within the synthesis loop, which makes these approaches depend on the scalability of the verification tools. In this paper, we propose a counterexample-guided inductive synthesis approach called RunVS which learns invariant expressions from program runs, but without information such as target safety properties, and without invoking a model checker/theorem prover for validation. The synthesis approach pairs a decision-tree (DT) based method with a data augmentation technique: DT-learning provides an expression that classifies observed states from augmented states that are speculated to be unreachable. Validation of the learned invariant is performed by sampling program runs and states; any run that invalidates the invariant results in counterexamples used to revises the invariant. As there is no formal proof that the learned artifact is a true invariant, we call such an expression a likely invariant. An important user input to synthesis is often the set of predicates that comprise the invariant expression; we use a novel integration with a large language model (LLM) and prompt it to provide likely predicates to be used. We show empirical results of our approach on several distributed protocols implemented in the Promela modeling language.