The language is low-level, typed, functional, native MAST language. It is designed to operate at the consensus layer and comes with formal denotational semantics and formal operational semantics which are both formalized in the Coq proof assistant and proven equivalent. O'Connor used Simplicity's formal semantics to prove correct an implementation of the SHA-256 compression function written in Simplicity. He also implemented a variant of ECDSA signature verification in Simplicity and plans to formally validate its correctness 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. Nodes operators can know the costs before evaluation and smart-contract participants can know the costs of their contracts before committing to them. Simplicity is still in research and development phase. 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.