> How would such a proof checker know the intent of the code of not having backdoor/insecurity? How do you define security in a logical sense? As you surely kn

> How would such a proof checker know the intent of the code of not having backdoor/insecurity? How do you define security in a logical sense? As you surely know, there is no such thing as secure/insecure, but a set of properties that are considered in IT security, which might even not be fullfillable all at the same time. The exact words vary depending on the book, but a popular classification in a German standard reference on IT Security is General protection goals: - Integrity - Confidentiality - Availability Further goals are - Authenticity - Acountability - Non Repudiation - Sometimes Anonymity So you first begin to formulate your protection goals. Next you can begin to forumulate this in a logical sense. Again there can exist quite different axiomatic implementations of a general protection goal. But since you want to see examples: A common model in literature for integrity is the Biba model: https://en.wikipedia.org/wiki/Biba_Model https://en.wikipedia.org/wiki/Biba_Model Another common model for integrity is the Clark-Wilson model: https://en.wikipedia.org/wiki/Clark%E2%80%93Wilson_model https://en.wikipedia.org/wiki/Clark%E2%80%93Wilson_model The mathematical dual of the Biba Model is the Bell–LaPadula Model for ensuring confidentiality: https://en.wikipedia.org/wiki/Bell%E2%80%93LaPadula_model https://en.wikipedia.org/wiki/Bell%E2%80%93LaPadula_model A model that ensures that the access rules will be free of conflict of interest (this of cause involves privacy and integrity aspects) is the Chinese Wall Model: https://www.cs.purdue.edu/homes/ninghui/readings/AccessControl/brewer_nash_89.pdf https://www.cs.purdue.edu/homes/ninghui/readings/AccessContr...