[junon]

This. We use Hoare logic verification in software in very similar ways, to assert on symbol intervals to make sure arithmetic and memory operations can succeed in e.g. C.