Module init 

Initialization contract checks. Initialization contract checker.

This module verifies Init-style obligations from graph OTS state. For aggregate nodes it recursively checks modeled field nodes; for leaves it uses the node’s init flag.