Got it, thanks for the reply. Are you familiar at all with Cardano / IOHK's IELE?

I get the impression from their documentation (https://developers.cardano.org/en/virtual-machines/iele/abou...) that it's intended to address that, but I'm no expert in this area.

I actually hadn't considered this issue at all until you mentioned it, but was aware that one of Cardano's selling points is a focus on verifiability (e.g. via their Haskell-based Plutus language for smart contracts), and came across this IELE after a quick search through their materials.