Researchers analyze the past, present, and future of proof scores, providing possible solutions to open issues

Proof scores are a promising technique in software engineering for verifying the properties of a software system. While proof scores offer the key advantage of following the same syntax as the specification language they are implemented in, they also have several disadvantages that have limited their wide acceptance. In a new study, researchers study the past, present, and future of proof scores to understand their weaknesses and future directions to overcome them.

In software engineering, it is important to ensure that a software system behaves correctly and reliably. This is especially crucial for critical systems, such as online banking, e-commerce, and real-time systems. One promising technique for verifying the properties of such systems is called proof scores, which uses a method called term rewriting. A proof score is composed of declarations and rewritings such that if all components evaluate as desired, then the problem is solved. This method strikes a balance between automation and manual effort: machines handle routine tasks like substitution, simplification, and reduction, while humans focus on the most interesting tasks, such as deciding proof strategies. Additionally, even partially completed proofs can yield valuable feedback, often indicating what to try next.

This technique has been put into practice through algebraic specification languages, particularly the OBJ family, such as OBJ3, CafeOBJ, and Maude, which are designed to be executable via term rewriting. A key advantage of proof scores is that they use the same syntax and evaluation mechanisms as the language used to specify the system, making the verification process smooth and tightly integrated. Hence, this method has been successfully applied to a wide range of systems and protocols. However, this method also has several disadvantages, which have limited it to mostly academic environments.

To understand this gap, a research team led by Professor Kazuhiro Ogata, along with Assistant Professor Duong Dinh Tran from the Japan Advanced Institute of Science and Technology (JAIST), conducted a deep dive into the past, present, and future of proof scores. "Proof scores have proven their capability to verify that systems, including those we rely on every day, meet their designs. In this study, we analyze the past and present of proof scores to understand their current challenges and find ways to improve their applicability," explain Prof. Ogata and Asst. Prof. Tran. Their study was published in the journal ACM Computing Surveys on April 9, 2025.

Proof scores were first proposed in the 1990s by the researcher Joseph A. Goguen. Since then, it has been implemented across multiple OBJ languages. In the study, the researchers explored the theoretical foundations of proof scores and analyzed their implementations in different OBJ languages. The researchers also studied several cases where proof scores were successfully applied, including communication, authentication and e-commerce protocols, real-time systems, modern cryptographic protocols, in post-quantum cryptographic protocols, which are encryption methods designed to be secure against the upcoming powerful quantum computers.

This analysis revealed the strong points of proof scores. Most notably, the same syntax used to specify a system can also be used to prove the properties of the system. Unlike traditional theorem-proving methods, which can be highly abstract, this property of proof scores ensures that every step in the proof is grounded in the formal definition of the system, making the proof more transparent and accessible. Furthermore, proof scores are written as programs and, therefore, are as flexible as programs.

However, this analysis also revealed their main weak point, i.e., proof scores are programmed by humans, who must ensure that all possible cases have been addressed, making them subject to human errors. None of the previous implementations warned the users if a case had been missed, which is especially problematic with large proofs. This is one of the main reasons why proof scores have not been more widely adopted. While proof assistants have been developed to address this weakness, they usually weaken the advantages of proof scores. However, there is one proof assistant called CiMPG for CafeOBJ, which also retains the merits of proof scores.

The researchers also highlighted other open issues, including the need for easier, human-readable proofs, accessible to a wider audience beyond researchers, as well as for more public libraries. To solve these open issues, the researchers suggest that modern systems should provide an Integrated Development Environment, like those used for popular programming languages, that would provide graphical, interactive support for writing and managing proof scores. They also suggest looking into the latest features of Maude.

"Proof scores will prove critical for emerging safety-critical systems that will shape our future society," say Prof. Ogata and Asst. Prof. Tran. "From the communication protocols used in online banking and e-commerce to blockchain and post-quantum cryptography, their potential for creating reliable systems is significant."

Overall, this study not only highlights the critical role of proof scores but also lays out a roadmap for making them more practical and widely accessible.

Image title: Proof Scores for Reliable and Safer Software
Image caption: Proof scores are a promising method for verifying the properties and reliability of software systems. From online banking and e-commerce to blockchain and post-quantum cryptography, their potential to improve software reliability is immense.
Image credit: Blogtrepreneur from Openverse.
Image link: https://openverse.org/image/f0cb4280-f872-46fa-b034-2959a4672c6c?q=Digital+security&p=14
Image license: CC BY 2.0
Usage restrictions: Credit must be given to the creator.

Reference

May 7, 2025