arXiv subjects

George Pîrlea

Publications and source records attributed to George Pîrlea.

6 recordsLinked to original sources

arXiv2026

Scenario Proofs for Verification of Distributed Protocols

Formal verification of distributed protocols is still dominated by inductive-invariant proofs, whose central challenge is discovering strengthening assertions that rule out unreachable states. This burden is often misaligned with how protocol designers reason: they explain correctness by following representative executions, causal histories, and phase-structured interactions among nodes. This paper introduces scenario proofs, a verification methodology that makes such execution-oriented reasoning formal. A scenario is a structured expression describing representative protocol executions, enriched with ghost variables. Rather than enumerate all possible interleavings, a scenario describes canonical executions and uses a sound semi-commutation relation to account for reorderings that preserve feasibility and final states. Verification then factors into two main obligations. Coverage shows that every feasible protocol execution is equivalent, up to semi-commutation, to one described by the scenario; this obligation is independent of the safety property and serves as a reusable behavioral characterization of the protocol. Correctness proves the desired safety property only over the representative executions, using Hoare-style weakest-precondition reasoning along the scenario structure. We formalize the scenario language, its layered semantics, and proof rules for coverage and correctness. Through case studies of ring leader election, two-phase commit, a decentralized lock, two variants of multi-signature payment, and single-decree Paxos, we show how scenario proofs capture the causal and phase-based arguments used informally by protocol designers. These examples illustrate that scenario proofs can replace monolithic invariant discovery with structured reasoning over representative executions, while retaining a rigorous connection to all feasible protocol behaviors.

cs.PL↗

arXiv2026

Certified Program Synthesis with a Multi-Modal Verifier

Certified program synthesis (aka vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of their alignment from a natural-language description. Two challenges make vericoding difficult. First, specifications synthesised from natural language are often either too weak to be meaningful or too strong to be implementable, yet existing approaches lack systematic means to detect such defects. Second, the landscape of program verifiers is fragmented: each tool supports a particular reasoning mode -- auto-active (e.g., Dafny, Verus) or interactive (e.g., Coq, Lean) -- with its own trade-off between automation and expressivity. This forces every synthesis methodology to be tailored to a single verification paradigm, limiting the class of tasks it can handle effectively. We overcome both challenges by structuring the certified synthesis workflow around a multi-modal verifier -- a single tool combining dynamic validation, automated proofs, and interactive proof scripting in one foundational framework. We realise this idea in LeetProof, an agentic pipeline built on Velvet, a multi-modal verifier embedded in Lean. Multi-modality enables LeetProof to validate generated specifications via randomised property-based testing before any code is synthesised, decompose the synthesis task into sub-problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised for Lean. We evaluate LeetProof on benchmarks derived from prior work on certified synthesis. Our specification validation uncovers defects in existing reference benchmarks, and LeetProof's staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same budget -- consistently across two frontier LLM backends.

cs.SE↗

arXiv2026

Inductive First-Order Formula Synthesis by ASP: A Case Study in Invariant Inference

We present a framework for synthesising formulas in first-order logic (FOL) from examples, which unifies and advances state-of-the-art approaches for inference of transition system invariants. To do so, we study and categorise the existing methodologies, encoding techniques in their formula synthesis via answer set programming (ASP). Based on the derived categorisation, we propose orthogonal slices, a new technique for formula enumeration that partitions the search space into manageable chunks, enabling two approaches for incremental candidate pruning. Using a combination of existing techniques for first-order (FO) invariant synthesis and the orthogonal slices implemented in our framework FORCE, we significantly accelerate a state-of-the-art algorithm for distributed system invariant inference. We also show that our approach facilitates composition of different invariant inference frameworks, allowing for novel optimisations.

cs.PL↗

arXiv2024

Small Scale Reflection for the Working Lean User

We present the design and implementation of the Small Scale Reflection proof methodology and tactic language (a.k.a. SSR) for the Lean 4 proof assistant. Like its Coq predecessor SSReflect, our Lean 4 implementation, dubbed LeanSSR, provides powerful rewriting principles and means for effective management of hypotheses in the proof context. Unlike SSReflect for Coq, LeanSSR does not require explicit switching between the logical and symbolic representation of a goal, allowing for even more concise proof scripts that seamlessly combine deduction steps with proofs by computation. In this paper, we first provide a gentle introduction to the principles of structuring mechanised proofs using LeanSSR. Next, we show how the native support for metaprogramming in Lean 4 makes it possible to develop LeanSSR entirely within the proof assistant, greatly improving the overall experience of both tactic implementers and proof engineers. Finally, we demonstrate the utility of LeanSSR by conducting two case studies: (a) porting a collection of Coq lemmas about sequences from the widely used Mathematical Components library and (b) reimplementing proofs in the finite set library of Lean's mathlib4. Both case studies show significant reduction in proof sizes.

cs.PL↗

arXiv2023

Greybox Fuzzing of Distributed Systems

Grey-box fuzzing is the lightweight approach of choice for finding bugs in sequential programs. It provides a balance between efficiency and effectiveness by conducting a biased random search over the domain of program inputs using a feedback function from observed test executions. For distributed system testing, however, the state-of-practice is represented today by only black-box tools that do not attempt to infer and exploit any knowledge of the system's past behaviours to guide the search for bugs. In this work, we present Mallory: the first framework for grey-box fuzz-testing of distributed systems. Unlike popular black-box distributed system fuzzers, such as Jepsen, that search for bugs by randomly injecting network partitions and node faults or by following human-defined schedules, Mallory is adaptive. It exercises a novel metric to learn how to maximize the number of observed system behaviors by choosing different sequences of faults, thus increasing the likelihood of finding new bugs. Our approach relies on timeline-driven testing. Mallory dynamically constructs Lamport timelines of the system behaviour and further abstracts these timelines into happens-before summaries, which serve as a feedback function guiding the fuzz campaign. Subsequently, Mallory reactively learns a policy using Q-learning, enabling it to introduce faults guided by its real-time observation of the summaries. We have evaluated Mallory on a diverse set of widely-used industrial distributed systems. Compared to the start-of-the-art black-box fuzzer Jepsen, Mallory explores more behaviours and takes less time to find bugs. Mallory discovered 22 zero-day bugs (of which 18 were confirmed by developers), including 10 new vulnerabilities, in rigorously-tested distributed systems such as Braft, Dqlite, and Redis. 6 new CVEs have been assigned.

cs.SE↗

arXiv2020

Compiling a Higher-Order Smart Contract Language to LLVM

Scilla is a higher-order polymorphic typed intermediate level language for implementing smart contracts. In this talk, we describe a Scilla compiler targeting LLVM, with a focus on mapping Scilla types, values, and its functional language constructs to LLVM-IR. The compiled LLVM-IR, when executed with LLVM's JIT framework, achieves a speedup of about 10x over the reference interpreter on a typical Scilla contract. This reduced latency is crucial in the setting of blockchains, where smart contracts are executed as parts of transactions, to achieve peak transactions processed per second. Experiments on the Ackermann function achieved a speedup of more than 45x. This talk abstract is aimed at both programming language researchers looking to implement an LLVM based compiler for their functional language, as well as at LLVM practitioners.

cs.PL↗