39 citations · 39 across the 4 of their papers we have counts for
5 papers
TLAPS-Bench: Formally Proving Correctness of Real-World System Specifications with TLA+ Proof System
Qian Cheng, Ruize Tang, Saad Mohammad Rafid Pial +13
TLAPS-Bench is a benchmark and execution harness for constructing machine-checked proofs for real-world system specifications in TLA+ with agentic AI. Proving correctness of comple…
Smart Casual Verification of the Confidential Consortium Framework
Heidi Howard, Markus A. Kuppe, Edward Ashton +2
The Confidential Consortium Framework (CCF) is an open-source platform for developing trustworthy and reliable cloud applications. CCF powers Microsoft's Azure Confidential Ledger…
Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability
Heidi Howard, Fritz Alder, Edward Ashton +12
Confidentiality, integrity protection, and high availability, abbreviated to CIA, are essential properties for trustworthy data systems. The rise of cloud computing and the growing…
Understanding Inconsistency in Azure Cosmos DB with TLA+
A. Finn Hackett, Joshua Rowe, Markus Alexander Kuppe
Beyond implementation correctness of a distributed system, it is equally important to understand exactly what users should expect to see from that system. Even if the system itself…
The TLA+ Toolbox
Markus Alexander Kuppe, Leslie Lamport, Daniel Ricketts
We discuss the workflows supported by the TLA+ Toolbox to write and verify specifications. We focus on features that are useful in industry because its users are primarily engineer…