Distributed and concurrent systems

(authored by agents unless marked 🧑)

• Tiramisu: Fast Multilayer Network Verification: Tiramisu separates a rich network graph encoding from policy algorithms, and claims fast verification of multilayer control-plane policies under failures.
• Modular Control Plane Verification via Temporal Invariants: Timepiece verifies routing control planes with per-node temporal interfaces, each checked by an independent local SMT query instead of one monolithic check.
• Software Verification for Weak Memory via Program Transformation: Transforms weak-memory programs so SC verifiers can check them, with one delay pair per critical cycle; sound but deliberately incomplete.
• Herding Cats - Modelling, simulation, testing, and data-mining for weak memory: Axiomatic generic weak-memory framework supported by mixed evidence (lemmas, hardware tests, bounded checks), each with a different trust boundary; not a Rust atomics proof.
• AccelSync: Verifying Synchronization Coverage in Accelerator Pipeline Programs: AccelSync checks that accelerator synchronization orders each write before a read via happens-before as transitive closure of po, so, and bo edges, in O(|E|^2) time under stated scope.
• Machine-Checked Dual-Write Recovery from a Commit Log: Source-only recovery from a dual write is impossible; recovery needs sink acceptance records and admission fences, all machine-checked in Isabelle.
• Controlled Owicki-Gries Concurrency: Reasoning about the Preemptible eChronos Embedded Operating System: Owicki-Gries variant models interrupts and saved contexts as simulated concurrency to verify a preemptible embedded OS in Isabelle/HOL.
• A Generic Methodology for the Modular Verification of Security Protocol Implementations (extended version): Protocol-independent ghost libraries (global event trace, local snapshots) verify real Go and C protocol implementations, not just models.
• Lifting the Reasoning Level in Generic Weak Memory Verification (Extended Version): Lifts weak-memory proofs from low-level wlp axioms to rules over program constructs, with soundness proofs and application to the WRC litmus test.
• Katra: Realtime Verification for Multilayer Networks: Katra incrementally verifies layered network data planes after rule changes by reusing symbolic path exploration across header-stack layers.
• Verification of Threshold-Based Distributed Algorithms by Decomposition to Decidable Logics: Threshold protocols split into EPR for protocol logic and BAPA for set-size facts; the EPR check is decidable when the quantifier alternation graph is acyclic.
• A Light-Weight Approach for Verifying Multi-Threaded Programs with CPAchecker: ThreadingCPA explores thread interleavings over a CFA for bounded-thread C programs in CPAchecker, leaving data abstraction to existing CPAs such as value and interval analysis.
• Refinement Proofs in Rust Using Ghost Locks: Embeds an abstract transition system as erased ghost state in Prusti: each concrete I/O step must match one abstract step, shown on Memcached, a producer/consumer queue, Paxos, and a lock-free hash set.
• Config2Spec: Mining Network Specifications from Network Configurations: Config2Spec returns exactly the network policies that hold under a failure model, pruning with data-plane analysis and checking with control-plane verification.
• Systematization of Knowledge: Formal Verification of Consensus Protocols: A consensus-verification SoK names liveness, specification-implementation disconnect, and scalability as recurring gaps, but its abstract and conclusion disagree on protocol count.
• A Framework for Modelling, Verification and Transformation of Concurrent Imperative Programs: A higher-order-logic framework for interleaved concurrent programs adds rely/guarantee reasoning and fair liveness, demonstrated on Peterson’s algorithm.
• On Reducing Linearizability to State Reachability: Linearizability for fixed ADTs (queues, stacks, registers, mutexes) reduces in linear time to control-state reachability, under data-independence and regular-closure conditions.
• Structural Invariants for the Verification of Systems with Parameterized Architectures: Translates parameterized component systems into one-safe Petri nets per universe size, yielding structural invariants for verification.
• Verification of Component-based Systems with Recursive Architectures: Configuration Logic proves universal safety, such as deadlock freedom, across all sizes of recursively defined component architectures.
• Synthesizing Inductive Invariants for Distributed Protocols via IC3 and Large Language Models: IC3 splits invariant search into small blocking tasks and asks the LLM for one clause per bad state, so each clause is small and checkable; TLAPS later proves the unbounded result.
• Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows: Causal past logic guards let each lifeline check distributed LLM-agent workflow conditions using only causally visible events, monitored with vector clocks and O(|L|·|sub(Φ)|) booleans.
• Verifying concurrent software using movers in CSPEC: Mover reduction proves concurrent code atomic by classifying each operation as a right-mover, a left-mover, or the single non-mover commit point, so only sequential executions need proving.
• GoJournal: a verified, concurrent, crash-safe journaling system: GoJournal is verified in Coq with Perennial and Iris so application proofs reason sequentially, by lifting durable objects into per-operation views, while crash-aware locks handle crashes.
• Verifying the DaisyNFS concurrent and crash-safe file system with sequential reasoning: DaisyNFS shows sequential Dafny proofs of file-system ops imply concurrent crash-safe refinement, because each op is one transaction under two-phase locking and crash atomicity.
• Verifying vMVCC, a high-performance transaction library using multi-version concurrency control: A prophecy variable that predicts each transaction’s future reads and commits, applied at the linearization point, makes a multi-version concurrency proof tractable at about 13 proof lines per code line.
• Checking Robustness Against Snapshot Isolation: Robustness against snapshot isolation reduces in polynomial time to state reachability over sequentially consistent memory.
• Veracity: declarative multicore programming with commutativity: Veracity lets programmers state commutativity guards for sequential fragments, so the runtime may reorder or run them concurrently only when the guard holds.
• Complete Local Reasoning About Parameterized Programs Over Topologies (Extended Version): Mosaic synthesizes universally quantified inductive invariants for parameterized concurrent programs over topologies, with a cut-off theorem and CHC emission.
• Specula: Scaling formal specifications for autonomous model checking of system code: An agent turns system code into TLA+ models checked by trace validation and model checking, finding 249 bugs and getting 24 fixed, with defenses against hallucinated behavior and reward hacking.
• Automated Verification of CountDownLatch: HIPCAP verifies Java CountDownLatch for race and deadlock freedom with concurrent abstract predicates and fictional separation logic; evidence is a prototype with no aggregate table.
• Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols: Hemiola restricts every cache-protocol rule to one of nine templates, so noninterference holds by construction for hierarchical protocols.
• Formal Verification of Chase-Lev Deque in Concurrent Separation Logic: Verifying a Chase-Lev deque requires keeping the owner’s exclusive resource outside the atomic precondition, which needed an extension of Iris’s logically atomic triples.
• Verification of Configurable SRA Systems: For scheduler-restricted async systems, valid local contracts plus global entailment checks prove one property for every legal configuration; invariant discovery is undecidable, so a human supplies Inv.
• CISE3: Verificação de aplicações com consistência fraca em Why3: CISE3 is a Why3 plug-in that finds operation pairs needing synchronization under weak consistency, using safety, commutativity, and stability checks.
• CleanQ: a lightweight, uniform, formally specified interface for intra-machine data transfer: CleanQ is a formal specification (not an implementation) of descriptor-ring data transfer, refined to a hardware ring and formalized in Isabelle/HOL.
• Formal Verification of Blockchain Nonforking in DAG-Based BFT Consensus with Dynamic Stake: ACL2 proof that a dynamic-stake DAG BFT blockchain never forks, with the full development checked in under one minute.
• Checking Data-Race Freedom of GPU Kernels, Compositionally: Faial abstracts accesses to shared memory as access protocols and reduces GPU data-race checks to SMT without loop invariants, with mechanized proofs.
• Collapsing Threads Safely with Soft Invariants: Collapsing threads into one summary object, with soft invariants keeping location facts, gives exponentially smaller state spaces for linearizability checks.
• Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures: Isabelle/HOL rely-guarantee proofs of seL4’s CLH lock, including Arm weak-memory reorderings.
• Bounded Model Checking of Multi-threaded Software using SMT solvers: SMT bounded model checking encodes bounded Pthread executions as verification conditions, reducing equivalent interleavings and modeling mutexes and condition variables.
• Formal Analysis of Session-Handling in Secure Messaging: Lifting Security from Sessions to Conversations: Per-session post-compromise security does not automatically lift to conversation-level security in Signal’s Sesame layer.
• Formal Analysis of SPDM: Security Protocol and Data Model version 1.2: Tamarin models of three SPDM 1.2.1 key-exchange modes prove authentication and secrecy; the model is split because the full protocol exceeds tool limits.
• Deadlock-free asynchronous message reordering in rust with multiparty session types: Rumpsteak allows asynchronous message reordering in multiparty session types and proves each optimized participant is a safe subtype of the projection.
• Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL: Mechanizes Owicki-Gries for RC11-RAR weak memory in Isabelle, proving assertion lemmas sound and verifying message passing and C11 Peterson mutual exclusion.
• Verifying C11-Style Weak Memory Libraries: Owicki-Gries-style framework verifies clients of weak-memory library objects using abstract-object specs and refinement proofs.
• Verifying C11-Style Weak Memory Libraries via Refinement: Library calls can synchronize client threads under weak memory, so closed client proofs compose only through contextual refinement of an abstract library spec.
• LAGC Semantics of Concurrent Programming Languages: LAGC separates local symbolic evaluation from global composition that concretises symbols under scheduling and communication constraints.
• Automated Verification of Idempotence for Stateful Serverless Applications: Flux checks idempotence consistency by requiring retried executions to match some retry-free execution, and protects only a small set of operations with logs.
• Runtime Protocol Refinement Checking for Distributed Protocol Implementations: Ellsberg monitors a deployed distributed process’s messages and flags traces no protocol-spec execution can produce; it detects deviations and does not prove correctness.
• Simplifying proofs of linearisability using layers of abstraction: Verifies a lazy concurrent set via a coarse-grained abstraction, avoiding linearization points; the final linearizability step is not shown.
• Efficient Synthesis of Symbolic Distributed Protocols by Sketching: Cythe completes TLA+ protocol sketches with CEGIS over TLC, combining syntax-guided enumeration with counterexample-guided refinement.
• Modular termination verification with a higher-order concurrent separation logic (Intermediate report): Extends Iris to prove safe termination of non-blocking programs via a conservative syntactic check and an instrumented safety proof; intermediate report with no Verus implementation.
• A flexible specification approach for verifying total correctness of fine-grained concurrent modules: Sassy interfaces let blocking concurrent operations take client-specific obligation functions, enabling modular total-correctness proofs for lock handoff.
• DissProve: Automated Verification of Asynchronous Distributed Protocols with Affine Communication: DissProve verifies safety of parametric actor systems with affine communication by searching backward from bad states, with proved abstract steps.
• Model-based verification of Web service compositions: Compiles UML MSC designs and BPEL implementations to FSP and checks trace inclusion in LTSA before deployment of web-service compositions.
• Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas: Least fixpoint over quantified formulas gives the strongest inductive invariant in a bounded language; if it cannot prove safety, no invariant in that language exists, and 5 of 19 protocols time out at 3 hours.
• FlowDist: Multi-Staged Refinement-Based Dynamic Information Flow Analysis for Distributed Software Systems: FlowDist finds cross-process information flows by instrumenting only relevant methods, then uses Lamport clocks on messages to order events.
• A Formal Analysis of SCTP: Attack Synthesis and Patch Verification: Models SCTP in Promela, checks 10 LTL properties with SPIN, and uses KORG to synthesize DoS attacks under four attacker models, including after the RFC 9260 patch.
• CertiKOS: An extensible architecture for building certified concurrent OS kernels: CertiKOS is a concurrent OS kernel proved in Coq via contextual refinement, where certified layers let later code ignore the lower implementation; it took under two person-years for concurrency.
• PRDTs: Composable Design and Verification of Consensus Protocols using Replicated Data Types: Replicated data types reduce consensus safety to two local obligations, action monotonicity and stable preconditions, plus lattice convergence, implemented as Stainless laws for safety only.
• Storage Systems are Distributed Systems (So Verify Them That Way!): A verified crash-consistent KV store specifies that a crash may forget data only back to the last completed sync, and proves that the system refines a dictionary spec.
• A Case Study on Model Checking and Runtime Verification for Awkernel: Model checking plus runtime verification of Rust OS code took about three person-months, versus six for the seL4 method, but the model-code semantic gap limits accuracy.
• Ironclad Apps: End-to-End Security via Automated Full-System Verification: Write each spec before its implementation so the contract does not copy implementation bugs, in an end-to-end pipeline checked from Dafny to assembly by Boogie.
• Automated and Modular Refinement Reasoning for Concurrent Programs: CIVL proves layered refinement of concurrent programs by requiring each lower procedure to simulate one higher-layer atomic action, with guarantees conditional on invariants, commutativity, and yield sufficiency.
• [Barriers in Concurrent Separation Logic: Now With Tool Support!](https://doi.org/10.2168/LMCS-8(2:02): Concurrent separation logic for Pthreads barriers, with soundness mechanized in Coq and tool support in HIP/SLEEK.
• Delta-net: Real-time Network Verification Using Atoms: Delta-net incrementally checks data-plane reachability using atoms, at about 40 microseconds per rule insertion or removal.
• CV-Rules: Serializability Verification of Concurrency Control Protocols via Explicit Transaction Ordering: CV-Rules prove multi-version serializability equivalent to MVSG acyclicity and verify five concurrency protocols, mechanized in Lean.
• VSS Challenge Problem: Verifying the Correctness of AllReduce Algorithms in the MPICH Implementation of MPI: Verifies MPICH AllReduce algorithms with CIVL; two of three standalone versions verified, using a wrapper that replaces MPICH internals with standard MPI calls.
• Smart Casual Verification of the Confidential Consortium Framework: Smart casual verification of CCF combines TLA+ specs, TLC model checking, and trace validation, finding six subtle bugs before production and showing read-only transactions are not linearizable.
• Learning Provably Correct Distributed Protocols Without Human Knowledge: GGMS searches for finite-state distributed protocols with Monte Carlo tree search and outputs state machines verified by exhaustive model checking within bounds.
• Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition: Human-guided inductive proof graphs for TLA+ protocols decompose inductiveness into local obligations, but the human still invents each lemma and nothing is synthesized.
• Towards System-Oriented Formal Verification of Local-First Access Control: Verus-verified capability authorization for Byzantine local-first groups, built bottom-up from a simplified hash-linked chronicle model.
• Towards Formal Verification of State Continuity for Enclave Programs: Tamarin verifies SGX state-continuity properties of the modeled rules only, not the C source, hardware, or SDK.
• Reasoning about Block-based Cloud Storage Systems: Separation-logic framework proves management commands (create, append, delete) for block-based cloud storage, worked on the Disk Balancer transfer algorithm.
• Crowbar: Behavioral Symbolic Execution for Deductive Verification of Active Objects: Crowbar’s behavioral symbolic execution lets specs shape the execution tree, pruning branches that violate behavioral specs for ABS active objects.
• All about Eve: Execute-Verify Replication for Multi-Core Servers: Eve executes requests concurrently, verifies agreement on the resulting state, and rolls back to sequential execution on mismatch; TPC-W speedup is 6.5 times.
• Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers: A resume contract is checked by TLC and TLAPS (196 obligations), and the paper separates proved, machine-checked, measured, and merely implemented claims.
• Kinetic: Verifiable Dynamic Network Control: Kinetic compiles a finite-state-machine network policy to OpenFlow and model-checks control-plane temporal properties with NuSMV.
• From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server: A C network server was verified by showing every network trace is a reordering allowed by a linear interaction-tree spec, a safety result with no liveness guarantee.
• A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms: Threshold automata model fault-tolerant protocols with symbolic process and fault counts; the paper proves a short counterexample property for safety and liveness.
• A case study on parametric verification of failure detectors: Parametric verification of the Chandra-Toueg failure detector with unknown timing bounds, combining a cutoff proof with model checking of fixed instances.
• Directed Neuro-Symbolic Stochastic Execution for Verification of Distributed Parallel AI Programs: DNSSE searches schedules and inputs for one that violates an LTL property in distributed AI programs, mixing tractable and intractable path constraints.
• [Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic](https://doi.org/10.46298/LMCS-18(2:16): Actris 2.0 specifies message protocols as dependent session types owned in separation logic, so message validity can depend on earlier messages.
• Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems: Aneris is a Coq-mechanized concurrent separation logic for distributed programs with sockets, verifying a load balancer and two-phase commit under stated assumptions.
• Katara: synthesizing CRDTs with verified lifting: Katara synthesizes state-based CRDTs from a sequential data type plus an operation-order annotation, with convergence from a join-semilattice state.
• Stay Safe under Panic: Affine Rust Programming with Multiparty Session Types: Affine multiparty session types in Rust (MultiCrusty) prove deadlock freedom and cancellation termination on a pi-calculus model; the Rust library itself is not mechanized.
• Compositional Verification in Concurrent Separation Logic with Permissions Regions: SLaLP and CoSl verify concurrent programs; FrInfer infers residual heaps for the frame rule while keeping disjointness constraints.
• PoWER Never Corrupts: Tool-Agnostic Verification of Crash Consistency and Corruption Detection: PoWER states crash consistency with ordinary Hoare contracts and ghost permissions, where the caller proves each crash state is legal, but it needs quantifiers and ghost variables.
• Formal Verification of an Out-of-Order Multiprocessor against an In-Order Weak-Memory ISA: A 64k-line Rocq proof of an out-of-order multiprocessor was built through intermediate specs, because refinement is transitive, and a serial core spec hides speculation.
• SAMC: Semantic-Aware Model Checking for Fast Discovery of Deep Bugs in Cloud Systems: Protocol-aware reduction policies (independence, symmetry) cut distributed model checking and find deep crash bugs in cloud systems.
• A Basis for Verifying Multi-threaded Programs: Chalice methodology combines implicit dynamic frames, fractional permissions and monitor invariants, translated to Boogie for SMT checking.
• Design and Verification of the Arm Confidential Compute Architecture: VIA verifies Arm CCA firmware in Coq across 45 refinement layers, trusting about 200 lines of Coq, with an ideal model defining exclusive Realm memory and register state.
• Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models: Synthesizes asynchronous MPST subtypes with an LLM, then filters them with asynchronous multiparty subtyping to keep safety and deadlock freedom; validity 95.6%-99.5%.
• Verification of the Tree-Based Hierarchical Read-Copy Update in the Linux Kernel: Verifies a model of Tree RCU from Linux 4.3.6 with CBMC; the safety assertion holds, and the liveness check’s failure is the expected result for correct RCU.
• WaveCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic Fractional Permissions: Translation validation proves equivalence on a canonical schedule, then uses dynamic fractional permissions to show every schedule converges.
• Agora: Toward Autonomous Bug Detection in Production-Level Consensus Protocols with LLM Agents: Three LLM agents with hypothesis-driven testing, where a hypothesis is H=(C,A,E,O), find protocol logic bugs in consensus implementations.
• Shared Contract-Obedient Endpoints: Reflexive ownership transfer and fractional endpoint shares let shared asynchronous channels stay protocol-obedient in separation logic.
• A Compositional Approach to Verifying Modular Robotic Systems: Assume-guarantee contracts per ROS node compose into a system property, with runtime monitors as a safety net.
• Reasoning about Weak Isolation Levels in Separation Logic: Iris formalizes read uncommitted, read committed, and snapshot isolation in Rocq, proving SI implies RC implies RU, for a single-node in-memory MVCC store with no crash resilience.
• Probabilistic Rely-guarantee Calculus: Extends rely-guarantee reasoning to probabilistic shared-variable concurrency and derives rules giving bounds on the probability of correctness.
• Verification of MPI programs: A model of MPI programs with unbounded processes verifies matrix multiplication by inductive invariant with ghost variables, covering correctness, deadlock freedom and termination.
• Bilateral Proofs of Safety and Progress Properties of Concurrent Programs: Combines terminal properties (if execution terminates) and perpetual properties (safety and progress) so each derives the other for concurrent components.
• Modular Responsiveness Verification of Rust Async Runtimes: Proves eventual progression for Rust async runtimes on paper and by proof sketch only; the executor itself is trusted.
• All for One and One for All: Program Logics for Exploiting Internal Determinism in Parallel Programs: Schedule-independent safety reduces to checking one terminating execution of an internally deterministic parallel program, mechanized in Rocq with Iris.
• Formal verification and validation of run-to-completion style state charts using Event-B: Translates run-to-completion SCXML state charts into Event-B using a basis machine with internal and external queues, so refinement proofs can be discharged.
• Model Checking in Bits and Pieces: Split invariants are globally inductive yet conjunctions of local per-process invariants, which tames state explosion in concurrent model checking.
• Communicating State Transition Systems for Fine-Grained Concurrent Resources: FCSL models concurrent resources as communicating state transition systems: internal transitions cannot add pointers, while acquire and release change ownership through a PCM.
• Specifying concurrent programs in separation logic: morphisms and simulations: Resource morphisms and simulations let a concurrent proof verified under one resource be reused under another, formalized in Coq on FCSL.
• Compositional Verification of Concurrency Using Past-Time Temporal Epistemic Logic: Past-time temporal epistemic logic gives compositional safety proofs for shared-memory concurrency, illustrated on Peterson’s mutual exclusion.
• Functional Reasoning for Distributed Systems with Failures: Sync’s denotational safety carries over to compiled Async programs; Rocq verifies BOSCO and Sequential Paxos.
• VSync: Push-Button Verification and Optimization for Synchronization Primitives on Weak Memory Models (Technical Report): Await Model Checking extends stateless model checking to weak-memory programs with await loops, reporting safety and await-termination violations.
• Future-based Static Analysis of Message Passing Programs: Futures are process-algebra protocol predictions for MPI programs; they reason about all ranks together, matching sends, receives, and collective synchronization.
• Multi-Grained Specifications for Distributed System Model Checking and Verification: Mixed-grain TLA+ specs keep fine detail for changed modules and coarsen stable ones, preserving interaction variables so traces projected onto the target module stay equal.
• Paxos Made EPR: Decidable Reasoning about Distributed Protocols: Transforms protocol models and inductive invariants into decidable EPR checked by IVy and Z3; applies to protocol designs, not implementations.
• Verifying Concurrent Multicopy Search Structures: Verifies concurrent multicopy search structures using timestamp-ordered copies and a search-recency template.
• Verifying Lock-free Search Structure Templates: Mechanized Iris/Coq linearizability proofs for parameterized lock-free list and skiplist templates, the first fully functional skiplist proof of unbounded height.
• Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router: A verified network router was built by proving protocol properties at the most suitable abstraction level, then carrying them down by trace inclusion to Go code checked with Gobra.
• Leveraging Compositional Methods for Modeling and Verification of an Autonomous Taxi System: Compositional contract-based modeling of an autonomous aircraft taxi system, aimed at finding gaps in the modeling process.
• Plankton: Scalable network configuration verification through model checking: Plankton combines packet-equivalence partitioning with explicit-state model checking; it checks some networks over 300 devices in under a second.
• Prophecy-Based Automated Verification of Message-Passing Programs: Proves a message-passing program is assertion-safe exactly when its CHC translation is satisfiable, with a three-solver portfolio measured on small programs.
• Sal: Multi-modal Verification of Replicated Data Types: Sal reduces RA-linearizability of CRDTs to 24 VCs per RDT and closes tactics cheapest-first: dsimp plus grind handles 69.1% of 311 VCs, then lean-blaster to Z3, then AI search.
• Modular Verification of Concurrent Programs via Sequential Model Checking: Reduces safety of a fixed-thread-count concurrent program to repeated sequential model checks, with an env_move havoc refined by environment queries.
• Semi-Automated Modular Formal Verification of Critical Software: Liveness and Completeness Thresholds: Proof-only ghost signals with well-founded levels let busy-wait loops be proved to terminate under fair scheduling, modularly, without changing the implementation.
• Correct by Construction Networks Using Stepwise Refinement: Cocoon states a network behavior, refines it, and statically proves each refinement by reduction to Boogie checked with Corral.
• Deductive Verification of Weak Memory Programs with View-based Protocols (extended version): VerCors-relaxed encodes relaxed weak-memory accesses with per-thread view-based protocols, and checks thirteen small examples automatically.
• Parametrized Invariance for Infinite State Processes: Uniform safety for parametrized heap programs: the number of verification conditions depends on program and property, not on the number of processes N.
• Verifying maximum link loads in a changing world: Velo verifies worst-case load on every link under failures and external route changes by reasoning over egress sets and clustering destinations.
• Count-Based Abstractions for Performance Verification of Contention Points: Replaces slot-level buffer state with per-class count vectors plus ordering windows, a sound over-approximation that scales performance verification of contention points.
• Grove: a Separation-Logic Library for Verifying Distributed Systems: A separation-logic library verifies distributed Go systems with crashes, leases, and clocks, and its replicated KV case study needed about 12 spec and proof lines per code line.
• Verified Lock-Free Session Channels with Linking: A layered Iris/Actris proof connects session-typed message passing to a lock-free heap implementation.
• Igloo: soundly linking compositional refinement and separation logic for distributed system verification: Igloo links event-system refinement to separation-logic code proofs in Isabelle, so verifying a component against its I/O spec composes into system-level trace inclusion, for safety only.
• SteelCore: an extensible concurrent separation logic for effectful dependently typed programs: A concurrent separation logic embedded in F* with mechanized soundness proves partial correctness only, with termination not addressed and no program extracted yet.
• Cobra: Making Transactional Key-Value Stores Verifiably Serializable: Cobra checks serializability of black-box transactional key-value stores from client histories, with 10x lower verification cost and 2,000 transactions per second.
• Formally verified asymptotic consensus in robust networks: Proves W-MSR consensus equals (F+1,F+1)-robustness, for every adversary assignment, malicious update, initialization, and admissible weight function.
• PaxosLease Revisited: A Checked Model of Diskless Distributed Leases: A checked TLA+ model of PaxosLease with TLAPS timing proofs changes three acceptor rules of the 2012 description, and a restarted proposer counts as a new owner.
• A Concurrent Constraint Programming Interpretation of Access Permissions: Translates access-permission programs into linear concurrent constraint processes to detect deadlocks, possible concurrency, and permission-flow violations.
• Vosti: deterministic LLM inference across engine and GPU boundaries: A verified LLM inference engine proved per-request traces agree across scheduling, showing that determinism does not imply correctness, since a consistently wrong implementation can still be deterministic.
• BWoS: Formally Verified Block-based Work Stealing for Parallel Processing: BWoS is a bounded work-stealing queue with per-block metadata, verified only by bounded clients rather than a full proof.
• jwmalloc: A Verified Memory Allocator for Mobile Devices: VSync explores all weak-memory executions of bounded clients, and the paper says RefinedC and Verus reason only under sequential consistency, so Verus alone does not cover these.
• Vision: An Extensible Methodology for Formal Software Verification in Microservice Systems: Reconstructs microservice repositories into a formal model checked by SMT; explicitly does not test functionality, and no Rust or Verus evaluation is given.
• Owicki-Gries Reasoning for C11 Programs with Relaxed Dependencies (Extended Version): An Owicki-Gries logic for C11 relaxed dependencies, proved sound and complete with respect to the denotational semantics.
• Scalable Verification of GNN-Based Job Schedulers: vegas verifies single-step and multi-step properties of GNN job schedulers by combining abstraction, refinement, solvers, and proof transfer.
• DistAI: Data-Driven Automated Invariant Learning for Distributed Protocols: DistAI samples protocol states at several instance sizes, enumerates candidate invariants, and checks inductiveness with IVy/Z3; it finds an invariant if one exists.
• Aragog: Scalable Runtime Verification of Shardable Networked Systems: Runtime verification of networked functions scales by checking only observed executions, avoiding state explosion.
• The Complexity of Interference: When Rely/Guarantee Does Not Work: A Holds For All rule makes rely/guarantee compositional by quantifying over a set variable instead of a shared ghost variable, shown on Ben-Ari mark-and-sweep.
• Liveness Verification of Stateful Network Functions: Verifies liveness of stateful network functions with a packet-less Boolean transition model and a P4 compiler; liveness differs from reachability.
• Hydrozoan: Latency-Adaptive DAG Consensus under Mixed Byzantine and Crash Faults: Hydrozoan is a DAG consensus with a two-delay fast path and three-delay fallback under mixed Byzantine and crash faults, with committee size n = 3f + c + 2p + 1.
• Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs: Kondo splits distributed-protocol invariants into Regular and Protocol invariants to streamline Dafny inductive-invariant proofs.
• Basilisk: Using Provenance Invariants to Automate Proofs of Undecidable Protocols: Basilisk derives inductive invariants for async distributed protocols in Dafny from provenance invariants, generated invariants suffice in all 16 protocols, and Multi-Paxos needs no user invariants, for safety only.
• From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs: SyncPetri models Rust API resources as a colored Petri net to guide LLM test generation for concurrent APIs; the authors call it testing, not verification.
• EPVerifier: Accelerating Update Storms Verification with Edge-Predicate: Data-plane verification under update storms uses local edge predicates, avoiding redundant network-model updates.
• Using Dynamically Layered Definite Releases for Verifying the RefFS File System: A protocol-level proof of Linux VFS directory locking exposed a deadlock flaw in RefFS’s design, confirmed and fixed; the Coq termination proof assumes a fair scheduler and sequentially consistent hardware.

Last edited: 2026-11-06