Abstract The application of formal methods in an industrial context remains a delicate and time-consuming task, and each successful project contributes to improving productivity. This experience report summarizes five years of applying formal verification for Common Criteria-based security certification of a JavaCard Virtual Machine at Thales. Since the first successful formal verification—directly over the source code with the verification platform—was achieved in 2021, five highest-level Common Criteria certifications (at EAL6 and EAL7 levels) have been obtained during the past five years. The strong guarantees of functional correctness and security provided by source code-based verification are essential for security-critical products such as smart cards. This paper traces the evolution of the project from an initial success to the continuous application of formal verification, and discusses the main challenges, applied solutions, and opportunities for further improvement.

Abstract Modern deductive verification tools succeed in automatically proving the great majority of program annotations thanks in particular to constantly evolving SMT solvers they rely on. The remaining proof goals still require interactively created proof scripts. This tool demo paper presents a new solution for an automatic creation of proof scripts in /, a popular deductive verifier for C programs. The verification engineer defines a proof strategy describing several initial proof steps, from which proof scripts are automatically generated and applied. Our experiments on a large real-life industrial project confirm that the new proof strategy engine strongly facilitates the verification process by automating the creation of proof scripts, thus increasing the potential of industrial applications of deductive verification on large code bases.