Jason is a platform for agent-based software development that is characterised both by being based on a programming language with formal semantics as well as having many language and platforms features that are very useful for practical programming, but not fully formalised. In this paper, we make significant progress in the direction of formalising the aspects of the variant of AgentSpeak that is interpreted by Jason that were not included in previous work on giving formal semantics to AgentSpeak. In particular, we give semantics to the plan failure handling mechanism which is unique to Jason, and also for some of the predefined internal actions that can alter an agent's mental state. Such internal actions are essential for some aspects of BDI-based programming, such as checking or dropping current goals or intentions, and therefore need to be formally defined within the operational semantics of the language.