ETAS는 모델 기반 에이전트 (model-backed agents), 도구 호출 (tool calls), 프롬프트 (prompts), 타입화된 메모리 (typed memory), 인간의 승인 (human approvals), 정책 (policies), 그리고 실행 트레이스 (execution traces)를 단순한 라이브러리 관례가 아닌 의미론적 프로그램 요소 (semantic program elements)로 취급하는 에이전트 시스템용 프로그래밍 언어입니다. ETAS는 직접적인 프로그래밍 스타일을 유지하면서 결정론적 계산 (deterministic computation)을 에이전트의 비결정론 (agentic nondeterminism) 및 외부로 노출되는 동작 (externally visible actions)과 분리합니다. 본 논문에서는 ETAS의 핵심 설계를 제시합니다. ETAS의 정적 의미론 (static semantics)은 명세 준수 (spec conformance)를 통해 일반적인 타입을 할당하며, 각 계산을 두 가지 행동 인덱스(behavioral indices)로 추적합니다: 탈출하는 효과 행 (escaping effect row)과 해당 계산이 요청할 수 있는 타입화된 액션 트레이스 (typed action trace)의 지속적인 추상화 (persistent abstraction)입니다. 명세 (Specs)는 종료되는 컴파일 타임 제약 조건 계산법 (terminating compile-time constraint calculus)을 형성합니다: 타입 명세 (type specs)는 다형성 (polymorphism)과 리소스 사실 (resource facts)에 대한 증거를 제공하고, 호출 가능한 명세 (callable specs)는 함수 및 스테이지 형태 (function and stage shapes)를 제약하며, 트레이스 명세 (trace specs)는 허용 (allow), 거부 (deny), 그리고 시간적 제약 (temporal constraints)을 표현합니다. 타이핑 (Typing) 과정은 요청된 트레이스를 컴파일된 모니터 (compiled monitors)와 대조하여 확인하며, 동적 리소스가 완전한 정적 증명을 방해할 경우 잔여 의무 (residual obligations)를 방출합니다. 동적 의미론 (dynamic semantics)은 요청됨 (requested), 처리됨 (handled), 거부됨 (denied), 그리고 커밋됨 (committed) 이벤트를 구분합니다. 핸들러 (handlers)는 타입화된 액션을 해석하되, 그 요청이 권한 부여 (authorization)나 감사 (audit) 과정에서 보이지 않게 만들지 않습니다. 우리는 핵심 계산법 (core calculus)과 상태 보존 (state preservation), 진행 (progress), 타입/효과 건전성 (type/effect soundness), 핸들러 트레이스 투명성 (handler trace-transparency), 그리고 정책 안전성 (policy safety)을 정형화합니다. 또한 우리는 명령줄 인터페이스 (command-line interface), 타입화된 HIR 체크, 효과 및 정책 진단 (effect and policy diagnostics), 핸들러 체크, 그리고 트레이스 인식 실행 훅 (trace-aware execution hooks)을 갖춘 ETAS를 Rust로 구현했습니다. ETAS는 에이전트 실행 전과 실행 중에 권한 부여, 비결정론, 복구 (recovery), 그리고 감사 증거 (audit evidence)에 대해 추론할 수 있는 프로그래밍 언어 기반을 제공합니다.