본 논문은 대규모 언어 모델(LLM)의 출력에 대한 검증 가능한 보장을 제공하지 못하는 문제점을 해결하기 위해, 디자인 바이 컨트랙트(DbC)와 타입 이론적 원리를 적용한 컨트랙트 계층을 제안한다. 이 계층은 모든 LLM 호출을 매개하며, 입력 및 출력에 대한 의미적 및 타입 요구 사항을 명시하고, 준수하도록 생성을 유도하는 확률적 수정 기능을 포함한다. LLM을 의미적 파서와 확률적 블랙박스 구성 요소라는 이중적 관점에서 제시하며, 컨트랙트 만족 여부는 확률적이며, 의미적 검증은 잘 정의된 데이터 구조에 대한 프로그래머가 지정한 조건을 통해 운영적으로 정의된다. 더 넓게는, 동일한 컨트랙트를 만족하는 두 에이전트는 그 컨트랙트와 관련하여 기능적으로 동등하다고 주장한다.