It uses basic combinators and is expected to be the target of front-end languages. The language comes with formal denotational semantics and formal operational semantics, which are both formalized in the Coq proof assistant and proven equivalent. Easy-to-compute static analyses can compute bounds on the space and time resources needed for evaluation. Simplicity uses jets to replace common expressions and directly implements them with C code. Jets cover arithmetic operations, elliptic curve operations, and cryptographic operations including hashing and digital signature validation. Simplicity supports full covenant support, allowing access to all transaction data, signature aggregation, and delegation. Unused branches of Simplicity programs are pruned at redemption time, thus enhancing privacy, reducing the block weight used, and reducing space and time resource costs needed for evaluation. Russell O'Connor plans to produce an SDK that includes the formal semantics and correctness proofs in Coq, a Haskell implementation for constructing Simplicity programs, and a C interpreter for Simplicity. After the SDK is completed, the next step will be making Simplicity available in the Elements project so that anyone can start experimenting with Simplicity in sidechains. Only after extensive vetting would it be suitable to consider Simplicity for inclusion in Bitcoin.