The language is designed to operate at the consensus layer and is expected to be the target of one or multiple front-end languages. Simplicity is a low-level, typed, functional, native MAST language where programs are built from basic combinators. It comes with formal denotational semantics and formal operational semantics that are both formalized in the Coq proof assistant and proven equivalent. Simplicity's formal semantics have been used to prove correct an implementation of the SHA-256 compression function written in Simplicity. Additionally, a variant of ECDSA signature verification has been implemented in Simplicity, and its correctness is planned to be formally validated along with the associated elliptic curve operations. Simplicity comes with easy-to-compute static analyses that can compute bounds on the space and time resources needed for evaluation, making it important for node operators and smart-contract participants. To make Simplicity practical, jets replace common Simplicity expressions identified by their MAST root and directly implement them with C code. This will anticipate developing a broad set of useful jets covering arithmetic operations, elliptic curve operations, and cryptographic operations including hashing and digital signature validation. Unused branches of Simplicity programs are pruned at redemption time as a native MAST language, enhancing privacy, reducing the block weight used, and can reduce space and time resource costs needed for evaluation.Simplicity is still in a research and development phase and does not intend to delay consideration of the various Merkelized Script proposals that are currently ongoing. After completing a bare-bones SDK, Simplicity will be available in the Elements project so that anyone can start experimenting with it in sidechains. Only after extensive vetting would it be suitable to consider Simplicity for inclusion in Bitcoin.