Assurance cases (ACs) are often required to certify critical systems. Use of integrated formal methods (FMs) in assurance can improve automation, increase confidence, and overcome ambiguity and faulty reasoning. However, ACs can rarely be fully formalised, as the use of FMs is contingent on models validated by informal processes. Consequently, we need assurance techniques that support both formal and informal artifacts, with explicated inferential links between them. In this paper, we contribute a formal machine-checked interactive language for the computer-assisted construction of ACs called Isabelle/SACM. The framework guarantees well-formedness, consistency, and traceability of ACs, and allows a tight integration of formal and informal evidence of various provenance. To validate Isabelle/SACM, we define a novel formalisation of the Tokeneer benchmark, verify its security requirements, and form a mechanised AC that combines the resulting formal evidence with informal artifacts.