automaton/contracts/verification.md

Acceptance Criteria

• All VALID bugs are fixed or justified
• No new issues introduced
• Code matches SPEC.md line-by-line

Stop Condition

When all checkboxes are checked, output "CONTRACT_MET" and stop.