수학적 추론 - bug, vulnerability, unintended behavior 등으로 부터 자유롭게 해줌 → 속성을 엄격하게 검증하였기에, 이는 contract의 trust(신뢰)와 confidence(확신)를 증가시켜줌.