Many complex software-based systems must be certified in order to be deployed in safety-critical environments. Modern software certification processes require trustworthy evidence supporting the verification claims. While verification tools have made tremendous gains in power, they lack the ability to generate concise and independently checkable evidence. The V Kernel project develops a practical approach to reconciling trust and automation. The claims generated by the fast but untrusted front-line verification tools are certified offline by slower but verified back-end checkers. The front-line analyzers can provide hints and certificates that assist the back-end tools. The verification of the checkers can be carried out by untrusted tools as long as the end result can be independently certified. Our approach does not constrain front-line tools by requiring them to produce proof objects. A wide variety of verification tools including SAT solvers, decision procedures, model checkers, static analyzers, and theorem provers can be validated using this approach.
