FOCAL is a first-order, constructive authorization logic. It has the first formal belief semantics of any authorization logic. It also has a Kripke semantics, which is subsumed by the belief semantics. The proof system of the logic has been proved sound w.r.t. to both semantics, and those proofs have been mechanized in Coq.

FOCAL is described in the following paper:

The Coq implementation of FOCAL can be downloaded here: focal.tar.gz.