증명 포함 코드
실행 가능한 코드와 함께 해당 코드가 안전 속성을 만족한다는 형식적 증명을 패키지로 묶어 전달하는 기술이다. 수신자는 코드를 실행하기 전 증명을 검증하여 안전성을 확인한다.
