Plutus Core Specification

The formal specification provides a comprehensive mathematical foundation for understanding the semantics and behavior of Plutus smart contracts.

This specification is periodically updated to reflect changes and improvements to the language and its cost model.

This specification document includes:

Syntax and Semantics: Complete formal definition of the Plutus Core language syntax and operational semantics
Type System: Detailed description of the type system and typing rules
Evaluation Rules: Precise specification of how Plutus Core programs are evaluated
Builtin Functions: Formal treatment of builtin functions and their semantics
Cost Model: Mathematical framework for the cost model used in script execution

The formal specification serves as the authoritative reference for: