Introduction

Here is describing Ursus. Ursus is language which is embeded to Coq. This language was created for describing solidity smart contracts. It has some key features such as: easy descirbing and understanding logic of programs, translators (from/to solidity). Ursus is interesting as lanaguage because it allows you to write smart contracts verification driven development (for example, ursus code -> verification -> translation to solidity -> deploy).