Argo: An efficient verification framework for distributed in-network computing
Abstract
Distributed in-network programs are increasingly deployed in data centers for their performance benefits, but shifting application logic to switches also enlarges the failure domain. Ensuring their correctness before deployment is thus critical for reliability. While prior verification frameworks can efficiently detect bugs for programs running on a single switch, they overlook the common interactive behaviors in distributed settings, thereby missing related bugs that can cause state inconsistencies and system failures. This paper presents Procurator, a verification framework that efficiently captures interactive behaviors in distributed in-network programs. Procurator introduces a formal model combining the actor paradigm with Communicating Sequential Processes (CSP), translating pipeline execution into reactive, event-driven actors and unifying their interactions as message passing. To support flexible specification of distributed properties, it provides a unified intent language. Additionally, it incorporates a semantic-aware state pruner to reduce verification complexity, thus ensuring system scalability. Evaluation results show that Procurator efficiently uncovers 10 distinct bugs caused by interactive behaviors across five real-world in-network systems. It also reduces verification time by up to 913.2x and memory consumption by up to 1.9x compared to the state-of-the-art verifier.
Cite
@article{arxiv.2511.08189,
title = {Argo: An efficient verification framework for distributed in-network computing},
author = {Mingyuan Song and Huan Shen and Jinghui Jiang and Qiang Su and Qingyu Song and Lu Tang and Wanjian Feng and Fei Yuan and Qiao Xiang and Jiwu Shu},
journal= {arXiv preprint arXiv:2511.08189},
year = {2025}
}