Proof Scores: A Survey (full version)

Abstract

Proof scores can be regarded as outlines of the formal verification of system properties. They have been historically used by the OBJ family of specification languages. The main advantage of proof scores is that they follow the same syntax as the specification language they are used in, so specifiers can easily adopt them and use as many features as the particular language provides. In this way, proof scores have been successfully used to prove properties of a large number of systems and protocols. However, proof scores also present a number of disadvantages that prevented a large audience from adopting them as proving mechanism. In this paper we present the theoretical foundations of proof scores; the different systems where they have been adopted and their latest developments; the classes of systems successfully verified using proof scores, including the main techniques used for it; the main reasons why they have not been widely adopted; and finally we discuss some directions of future work that might solve the problems discussed previously.

Proof Scores: A Survey. ACM Comput. Surv. (April 2025)

References in corpus (8)

• A formal proof of the four color theorem
• Extracting Smart Contracts Tested and Verified in Coq
• A Proof Tree Builder for Sequent Calculus and Hoare Logic
• Hardware/Software Co-Assurance using the Rust Programming Language and ACL2
• A drag-and-drop proof tactic
• Verification of GossipSub in ACL2s
• Using Counterexample Generation and Theory Exploration to Suggest Missing Hypotheses
• Verification of a Rust Implementation of Knuth's Dancing Links using ACL2