The sKizzo/ozziKs couple (here) allows you to produce and verify certificates of satisfiability for QBFs (see Item 1 below). A certificate of satisfiability for a QBF is a compact representation of one of its models providing solver-independent evidence of satisfiability (see Item 2). In addition, it can be inspected to gather explicit information about the semantics of the formula (see Item 3). Within the sKizzo suite, instance evaluation is decoupled from model reconstruction, with almost no overhead for the former, and a clear semantics for the latter. The two meshes of the chain are connected through an inference log, produced by the solver (sKizzo), and subsequently read by the model/certificate reconstructor (ozziKs). The log contains all the information necessary to perform the inductive model reconstruction procedure (as published here): rollback/commit entries to trace the status of the transactional inference engine of sKizzo, a detailed representation of all the (ground and symbolic) instantiations of inference rules exercised, context switches among inference styles, working hypotheses addition/withdrawal for branching reasoning, a representation of inverse groundization functions to interpret propositional models of SAT sub-instances, and more. The validity of a certificate can be verified by whoever is knowledgeable about the evaluation apparatus of the logic (deductive capabilities are unnecessary), independently of how it was obtained. The meaning of a successful verification is twofold: we are ensured (1) that the formula is SAT, and (2) that the certificate encodes a model. A few experimental results on the certification of satisfiable fomulas in the QBFLIB repository are reported below. For each family/instance we report the time taken to solve the instance (Ts), to reconstruct a certificate/model (Tr), and to verify the certificate against the formula (Tv). The size of the inference log (number of entries) and the size of the representation for the model/certificate (number of internal nodes in the forest of BDDs) are given as well. SAT families (sKizzo v0.6.1, ozziKs v0.1, P4 2.6GHz 1GB) (see them all) # Family #inst avg #var avg #clause avg #alt tot Ts tot Tr tot Tv avg |log| avg |model| 1 Adder2 5/8 2538 2599 3.1 434.8s 133.3s 0.1s 3898 13100 2 adder 8/8 2775 3743 3 2114.2s 3890.6s 2s 1312 63248 3 blocks 3/3 296 3030 2 0.4s 0.1s 0s 86 65 4 chain 12/12 1998 11174 2 1.4s 0.5s 0.3s 1450 19 5 comp 4/4 300 816 3 0.3s 0.1s 0s 167 29 6 counter 47/64 316 831 9.8 2421.5s 143.7s 0.3s 24856 63 7 k_d4_n 8/8 1056 3744 31.3 51s 430.6s 1.4s 6832 28429 8 k_grz_n 8/8 542 1987 16 203.4s 2.7s 0.1s 1154 1845 9 k_ph_n 7/8 787 10293 3.1 91.3s 1.8s 0.5s 1725 464 10 k_poly_n 8/8 701 1582 55.5 12.3s 20.9s 0.1s 2108 724