formal top-level specification (FTLS)

A Top-Level Specification that is written in a formal mathematical language to allow theorems showing correspondence of the system specification to its formal requirements to be hypothesized and formally proven [TCSEC].