Thank you.
One possibility to consider is this: database-engines and SMT provers both use Unification… it is therefore possible to ‘factor’ this out and do a SPARK-proved “Verified Unification Engine” — then, using this, you could implement a prover-framework designed to be distributed (DSA), hierarchical, parameterizable (ie using the design of Generics as a template so that large portions of the module is proved, and all you have to do is check ‘detail’ “on instantiation”), and able to ‘import’/‘export’ via SMT-LIB 2… which then would allow a SPARK proved alternative implementation of SPARK along with a verified DB engine.