We present the design and implementation of a Certified Core Policy Language (ACCPL) that can be used to express access-control policies. We define formal semantics for ACCPL and use the Coq Proof Assistant to state theorems about this semantics, to develop proofs for those theorems and to machine-check the proofs ensuring correctness guarantees are provided. The main design goal for ACCPL is the ability to reason about the policies written in ACCPL with respect to specific questions such as safety. In addition, ACCPL and the established proofs are integrated such that extensions to expressive power may be explored by also extending identifiable proof statements in the direction of the added expressivity. To this end, ACCPL is small (the syntax and the semantics of ACCPL only take a few pages to describe), although we believe ACCPL supports the core features of many access-control policy languages.