The de Bruijn factor measures how much bigger a formal proof is than its informal original. A similar construct could measure the gulf between building large-scale software and assuring it. It could be effort-orientated (assurance hours / build hours) or clock-orientated (elapsed time to assure / elapsed time to build). The difference between those two is organisational friction. Or, like margin in the mind of Bezos, opportunity.