Manuscript Oai279-A@1 · Oai279-A.tex · section · a1abc73f
Interface 3: verified data and bounded transitions
Stage 1: audit the five interfaces without importing them › Interface 3: verified data and bounded transitions · lines 531–535
This verifies a supplied root list. It does not generate that list, verify every auxiliary process invariant, or factor arbitrary .