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

Ishikawa, Japan -- 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.


###

Reference

Title of original paper:	Proof Scores: A Survey
Authors:	Adrián Riesco, Kazuhiro Ogata, Masaki Nakamura, Daniel Găină, Duong Dinh Tran, and Kokichi Futatsugi
Journal:	ACM Computing Surveys
DOI:	10.1145/3729166

About Japan Advanced Institute of Science and Technology, Japan
Founded in 1990 in Ishikawa prefecture, the Japan Advanced Institute of Science and Technology (JAIST) was the first independent national graduate university that has its own campus in Japan. Now, after 30 years of steady progress, JAIST has become one of Japan’s top-ranking universities. JAIST strives to foster capable leaders with a state-of-the-art education system where diversity is key; about 40% of its alumni are international students. The university has a unique style of graduate education based on a carefully designed coursework-oriented curriculum to ensure that its students have a solid foundation on which to carry out cutting-edge research. JAIST also works closely with both local and overseas communities by promoting industry–academia collaborative research.


About Professor Kazuhiro Ogata and Assistant Professor Duong Dinh Tran from Japan Advanced Institute of Science and Technology, Japan
Dr. Kazuhiro Ogata is currently a Professor at the Computing Science Research Area, Japan Advanced Institute of Science and Technology (JAIST). He obtained his Ph.D. in 1995 from Keio University. At JAIST, he leads the Laboratory on Formal Methods and Trustworthy Software. He has published over 250 articles that have received over 2,100 citations. His research is focused on formal verification methods for software systems, theorem proving, model checking, and rewriting, among others.
Dr. Duong Dinh Tran received his Ph.D. in Information Science in October 2023 under the supervision of Prof. Kazuhiro Ogata. He is currently a Research Assistant Professor at Japan Advanced Institute of Science and Technology. His research interests include theorem proving and model checking, with a focus on their practical applications in software engineering and real-world systems.