Ursus

Formal Verification Platform for Smart Contracts

Ursus is a comprehensive ecosystem for writing, verifying, and proving smart contracts with mathematical certainty. Build secure contracts that are provably correct.

Documentation →Ursus Guide APISoon

Components

Ursus Language

Production Ready

Domain-specific language embedded in Coq/Rocq for writing verifiable smart contracts with familiar Solidity-like syntax.

Learn more →

Ursus Proof

Production Ready

Verification system with Coq tactics language for proving properties of Ursus smart contract functions.

Ursus Guide

Final Development Stage

VS Code plugin for writing, translating, specifying, and proving contracts. AI-first approach with full automation.

https://ursus-guide.ursus-tools.devSoon

Ursus Specification

In Development

Visual graph editor for creating smart contract specifications with intuitive interface.

Ursus Async

In Development

Asynchronous contract system representation with Ursus Script for temporal and scenario properties.

Key Advantages

✓Mathematical proof of correctness — not just testing
✓Familiar syntax for Solidity/C++ developers
✓Full Coq integration for formal proofs
✓Multi-language target support (Solidity, C++, Rust)
✓Automated boilerplate generation via Elpi
✓Strong type system with panic tracking
✓Battle-tested by Pruvendo security audits