A proof assistant has essentially this structure. So, we use the user, the outside world is the user, the output is a verified statement, the inputs are uner's specifications. The user also inputs tactics to this proof development system. This actually produces the proof object which is checked by the proof checker.
So, this is the general structure. And notice that an error in the checker invalidates the whole approach. Here therefore we have the brown (Bruijn principle, which says that it is preferable to use systems with a small reliable checker, rather than having elaborate proof checkers.