A formalisation of Cartesian Frames, a perspective on embedded agency, in the HOL theorem prover. - View it on GitHub