Mohsen Lesani

Shubham Agarwal, Alexander Krentsel, Shu Liu et al.

AI agents increasingly excel at generating, testing, and refining code. However, they fall short on tasks requiring formal guarantees of full coverage that testing alone cannot provide. Distributed systems are a prime example: properties such as consistency between reads and writes must hold under every possible interleaving of events. Mechanized formal verification can guarantee such correctness, but typically demands months to years of expert effort. As evidence, even SOTA coding agents (Codex with GPT-5.4 and Claude Code with Opus 4.6) succeed on only 2/7 distributed key-value-store specifications. In this paper, we present the first effective approach to addressing this gap, Inductive Deductive Synthesis (IDS), which jointly and incrementally synthesizes implementation and proof, and learns from failed attempts to systematically try promising strategies. Built as an agentic LLM system, IDS achieves 7/7 in about 6.8 hours and $106 per spec on average, roughly 200x faster than expert effort and 17% cheaper than SOTA agents. IDS further incorporates performance feedback into the same loop, yielding implementations up to 3x faster than published verified systems.

Javad Saberlatibari, Prithviraj Yuvaraj, Mohsen Lesani et al.

Data replication is a critical aspect of data center design, as it ensures high availability, scalability, and fault tolerance. However, replicas need to be coordinated to maintain convergence and database integrity constraints under transactional workloads. Commutative Replicated Data Types (RDTs) provide convergence for conflict-free objects using relaxed consistency, and Well-coordinated Replicated Data Types (WRDTs) provide convergence and integrity for general objects using a hybrid model, relaxed when possible and strong when necessary. While state-of-the-art hardware acceleration of RDT uses Remote Direct Memory Access (RDMA), we observe that trends towards lower latency and higher throughput have driven recent data center architectures to leverage FPGAs as application accelerators. In contrast to deploying an FPGA-based Smart NIC, this paper connects an FPGA accelerator card directly to the network, which allows a complete redesign of the NIC to match the needs of the FPGA-hosted application. We co-design a network-attached FPGA replication engine with an FPGA-resident network interface, enabling near-network execution of replicated transactions and direct invocation of FPGA-resident operators. Following this approach, we introduce SafarDB, FPGA-accelerated Conflict-Free Replicated Data Types (CRDTs) and WRDTs. SafarDB accelerates both relaxed and strongly ordered replication paths; when strong ordering is required, SafarDB accelerates the underlying consensus control path. SafarDB improves CRDT latency and throughput by 7.0X and 5.3X, and WRDT latency and throughput by 12X and 6.8X compared to a state-of-the-art RDMA-based implementation. Further, experiments demonstrate that SafarDB is more resilient to crash-failures than existing CPU/RDMA-based CRDT and WRDT implementations, and SafarDB can detect leader failures and elect new leaders much faster than previously possible.