It has been designed to operate at the consensus layer and comes with formal denotational semantics and formal operational semantics which have both been proven equivalent in the Coq proof assistant. The formal denotational semantics have been used to prove correct an implementation of the SHA-256 compression function written in Simplicity. Additionally, it comes with easy-to-compute static analyses that can compute bounds on the space and time resources needed for evaluation. As a native MAST language, unused branches of Simplicity programs are pruned at redemption time, which enhances privacy, reduces block weight used, and can reduce space and time resource costs needed for evaluation. To make Simplicity practical, jets replace common Simplicity expressions (identified by their MAST root) and directly implement them with C code. The plan is to use Luke's fail-success-on-unknown-operation in Simplicity. When new jets are wanted they can be soft-forked into the protocol and the list of known discounted jets grows. If one half of a pair contains an assertion failure (fail-closed), and the other half contains an unknown jet (fail-open), then the program is automatically successful making it anyone-can-spend. Jets could include cryptographic operations including hashing and digital signature validation. The final design includes extensions not covered in the paper, including full convent support, allowing access to all transaction data; support for signature aggregation; and support for delegation. After an SDK is complete 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.