A procedure for "passively" certifying a proof would not certify inferences, but rather would simply involve collecting extant certifications of inference steps if possible. Passive certification of a proof would take as argument a rooted digraph of inference steps and a test for acceptability of inference certificates. It proceeds by checking to see that the children of the root inference have as their conclusions the premises of the root; also it checks to see that there is a certificate object verifying the root inference and which passes the test for acceptability; then the procedure is applied recursively to each of the subgraphs for the children of the root; if all this succeeds then build a proof certificate comprising the specification for acceptable inference certificates, references to an acceptable root certificate and to each of the recursively created proof certificates for the children of the root. Note that if this procedure terminates, then it describes a dag of inference certificates for inference steps with the right correspondence between parent premises and child conclusions. Obviously, rather than recursing perhaps forever, we would use a loop detecting variant that would fail on loops in the digraph.
A procedure for "actively" certifying a proof would be similar, taking as a further argument a procedure for certifying inferences for which no acceptable certificate exists. Instead of simply failing when it cannot find an appropriate inference certificate, it invokes on the uncertified inference the creation procedure specified for active proof certification. Indeed, the passive proof certification would simply be this active certification procedure where the procedure for certifying unacceptable inferences simply fails. At the other extreme, if the active procedure is employed with the stipulation that the only acceptable inference certificates are those it creates itself during that run, then its success would entail certifying anew every inference reachable from the root of the digraph.
The above method depends on little about how inference engines work, but this account is deficient with regard to inferences that cite lemmas, and we cannot expect a uniform solution independent of the inference engines that might be supplied by FDL clients because they may have been based on differing choices about how they treat