> 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

Another common model for integrity is the Clark-Wilson 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

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/AccessContr...