불변성
프로그램이 실행되는 동안 항상 참으로 유지되어야 하는 논리적 조건이나 제약이다. 이를 명세에 명시하고 자동 검증 계층에서 체크함으로써 시스템의 아키텍처적 일관성을 보장할 수 있다.