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 k_d4_n 8/8 1056 3744 31.3 51s 430.6s 1.4s 6832 28429 3 tree 5/5 40 38 1 0s 0.1s 0s 21 58 4 k_poly_n 8/8 701 1582 55.5 12.3s 20.9s 0.1s 2108 724 5 k_grz_n 8/8 542 1987 16 203.4s 2.7s 0.1s 1154 1845 6 k_ph_n 7/8 787 10293 3.1 91.3s 1.8s 0.5s 1725 464 7 counter 47/64 316 831 9.8 2421.5s 143.7s 0.3s 24856 63 8 blocks 3/3 296 3030 2 0.4s 0.1s 0s 86 65 9 toilet_g 7/7 50 204 2 0s 0.1s 0s 49 30 10 adder 8/8 2775 3743 3 2114.2s 3890.6s 2s 1312 63248 11 comp 4/4 300 816 3 0.3s 0.1s 0s 167 29 12 mutex 7/7 8890 4173 1 94.6s 103.6s 0.3s 3326 41616 13 chain 12/12 1998 11174 2 1.4s 0.5s 0.3s 1450 19 A certificate exemplifies a definite scenario in which QBF-encoded problems reveal their satisfiability. For example, a SAT-answer suffices to know that at least one winning strategy exists in a QBF-encoded two-player game, but it takes a certificate to exhibit an actual strategy. A proof-of-concept example for such strategy-synthesis-as-QBF-model-extraction approach is reported aside (click on the TicTacToe picture aside and give it a try!). A cgi script queries through the C library libQBM (soon available for download) a SAT-certificate providing evidence that the answer to the (QBF-encoded version of the) following question is ''YES'': Given the rules of TicTacToe, can the second (O) player always prevent the first player (X) from winning? One last thing: You are likely to find alternative names for referring to QBF certificates in the literature. A few of such names are: strategies, models, policies.