Searched, not verified

Abstract

Between "the model argued it is safe" and "a machine-checked proof exists" there is a wide and useful middle, and most organizational assurance questions live in it. This paper describes Soter, which puts an SMT solver into the convergence loop of our substrate to answer one shape of question: can any model exist that violates this encoded invariant? Encoding the negation and asking for satisfiability turns a safety claim into a search for a counterexample, and a counterexample — unlike an argument — is a concrete assignment an engineer can read. The contribution we care about is not the integration but the epistemics around it. An unsat result is recorded as searched evidence and never as verified, and we give the two reasons precisely: the encoding gap between an organizational invariant and a formula, and the checker gap between a solver’s claim and a proof an independent checker has validated. We argue that the most dangerous engineering error in this area is not an unsound solver but a status mapping that quietly reads timeout as unsat, and we show what the mapping must look like to prevent it. The path from searched to verified — proof certificates checked by a small independent kernel — is described and marked as not taken.