Introduction

Welcome to the Ursus documentation! Ursus is a revolutionary approach to smart contract development that combines the familiarity of languages like Solidity with the mathematical rigor of formal verification.

What is Ursus?

Ursus is a domain-specific language (eDSL) embedded in the Coq proof assistant, designed for writing and verifying smart contracts with mathematical certainty.

Think of Ursus as a bridge between two worlds:

• The familiar world of smart contract languages (Solidity, C++)
• The rigorous world of formal verification and mathematical proofs

Why Ursus?

Smart contracts handle real money and critical operations. A single bug can cost millions. Traditional testing can't guarantee correctness - but mathematical proofs can.

Ursus gives you:

1. Write Once, Verify Forever

Write your contract in a familiar syntax, then prove it's correct - mathematically:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
    ::// balances[[to]] := balances[[to]] + amount .
    ::// _result := @true |.
}
return.
Defined.

(* Now prove it preserves total supply *)
Theorem transfer_preserves_total_supply:
  forall from to amount s s',
    exec_transfer from to amount s = Some s' ->
    total_supply s' = total_supply s.
Proof.
  (* Mathematical proof here *)
Qed.

2. Familiar Syntax

If you know Solidity or C++, Ursus will feel natural:

Solidity:

function transfer(address to, uint256 amount) public returns (bool) {
    balances[msg.sender] -= amount;
    balances[to] += amount;
    return true;
}

Ursus:

Ursus Definition transfer (to: address) (amount: uint256):
  UExpression boolean false.
{
    ::// balances[[msg->sender]] := balances[[msg->sender]] - amount .
    ::// balances[[to]] := balances[[to]] + amount .
    ::// _result := @true |.
}
return.
Defined.

3. Executable and Verifiable

Your Ursus code is:

• Executable - Run it, test it, deploy it
• Verifiable - Prove properties about it
• Extractable - Generate Solidity/C++ code

4. Automated Assistance

Elpi automation generates boilerplate code, helping you focus on logic and proofs:

(* Write this *)
Contract ERC20 ;

(* Get this automatically generated *)
- Type definitions
- Field accessors
- State management
- Proof scaffolding

5. Formally Verified Core

The Ursus semantics itself is formally verified in Coq, ensuring the foundation is solid.

Key Features

How It Works

┌─────────────┐
│ Write Ursus │  ← Familiar syntax
│   Contract  │
└──────┬──────┘
       │
       ├─────────────────┐
       │                 │
       ▼                 ▼
┌─────────────┐   ┌─────────────┐
│   Execute   │   │    Prove    │
│  & Test     │   │ Properties  │
└──────┬──────┘   └──────┬──────┘
       │                 │
       │                 │
       ▼                 ▼
┌─────────────┐   ┌─────────────┐
│   Deploy    │   │ Guaranteed  │
│  to Chain   │   │  Correct    │
└─────────────┘   └─────────────┘

A Simple Example

Let's see a complete mini-contract:

(* Define the contract *)
Contract Counter ;
Sends To ;
Types ;
Constants ;

Record Contract := {
    count: uint256
}.

(* Implement increment function *)
Ursus Definition increment: UExpression PhantomType false.
{
    ::// count := count + {1} |.
}
return.
Defined.

(* Prove it always increases *)
Theorem increment_increases:
  forall s s',
    exec_increment s = Some s' ->
    count s' = count s + 1.
Proof.
  (* Proof here *)
Qed.

That's it! You have:

• ✅ A working contract
• ✅ A mathematical proof of correctness
• ✅ Code ready to deploy

Who Should Use Ursus?

Ursus is perfect for:

• DeFi Developers - Where bugs cost millions
• Security Researchers - Who need mathematical guarantees
• Smart Contract Auditors - Who want provable correctness
• Blockchain Engineers - Building critical infrastructure
• Academics - Researching formal methods

You should know:

• Basic smart contract concepts (Solidity/Ethereum)
• Some functional programming (helpful but not required)
• Willingness to learn formal verification (we'll teach you!)

What's in This Documentation?

This documentation is organized from beginner to advanced:

1. Installation - Get Ursus running
2. Quick Start - Your first contract in 10 minutes
3. Coq eDSL - How Ursus works under the hood
4. Ursus Language - Complete language reference
5. Programming Style - Best practices and patterns
6. Standard Library - Built-in functions and types
7. Verification - Proving your contracts correct
8. Long Start - Comprehensive tutorial
9. Translation - Converting from Solidity/C++
10. Advanced Topics - Expert-level features

Ready to Start?

Jump right in:

• New to Ursus? → Start with Quick Start
• Coming from Solidity? → Check Translation Guide
• Want to verify? → See Verification Principles
• Need examples? → Check the ursus-patterns repository in related projects

Get Help

• Documentation: Browse this book for comprehensive guides
• Examples: Check ursus-patterns repository for example contracts
• Community: Contact Pruvendo team for support

Let's build smart contracts we can trust! 🚀