diff --git a/README.md b/README.md index aa08f4b..4d26e1a 100644 --- a/README.md +++ b/README.md @@ -1,23 +1,179 @@ -# komet +
+# 🌠 Komet -## Installation +**Formal Verification & Fuzzing for Soroban Smart Contracts** -Prerequsites: `python >= 3.10`, `pip >= 20.0.2`, `poetry >= 1.3.2`. +[![Install](https://img.shields.io/badge/install-kup-blue)](https://kframework.org/install) +[![Documentation](https://img.shields.io/badge/docs-komet-green)](https://docs.runtimeverification.com/komet) +[![Discord](https://img.shields.io/badge/discord-join-7289da)](https://discord.gg/CurfmXNtbN) +[![License](https://img.shields.io/badge/license-BSD--3-orange)](LICENSE) + +[Quick Start](#-quick-start) β€’ [Documentation](#-documentation) β€’ [Community](#-community) + +
+ +--- + +## 🌟 Overview + +**Komet** is a cutting-edge formal verification and fuzzing framework specifically designed for [Soroban](https://stellar.org/soroban) smart contracts on the Stellar blockchain. Built on Runtime Verification's powerful K Semantics framework, Komet enables developers to write property tests in Rust and verify their contracts' correctness across **all possible inputs**, not just a sample. + +![Komet in action](media/komet-fuzzing.gif) + +### Why Komet? + +In the high-stakes world of decentralized finance (DeFi), a single bug can cost millions. Traditional testing only covers scenarios you think of. **Komet goes beyond** by: + +- πŸ” **Fuzzing**: Automatically generating randomized test inputs to find edge cases +- βœ… **Formal Verification**: Symbolically executing contracts to prove correctness across **all** possible scenarios +- πŸ¦€ **Rust-Native**: Write property tests in the same language as your Soroban contracts + +--- + +## πŸš€ Quick Start + +### Installation + +Install Komet in two simple steps using `kup`, Runtime Verification's Nix-based package manager: ```bash -make build -pip install dist/*.whl +# 1. Install kup package manager +bash <(curl https://kframework.org/install) + +# 2. Install Komet +kup install komet + +# 3. Verify installation +komet --help ``` +### Your First Property Test + +```rust +use soroban_sdk::{contract, contractimpl, Env}; + +#[contract] +pub struct Adder; + +#[contractimpl] +impl Adder { + pub fn add(env: Env, a: i32, b: i32) -> i32 { + a + b + } +} + +// Property: Addition should be commutative +#[komet::property] +fn test_addition_commutative(a: i32, b: i32) { + let env = Env::default(); + let contract = AdderClient::new(&env, &env.register_contract(None, Adder)); + + assert_eq!( + contract.add(&a, &b), + contract.add(&b, &a) + ); +} +``` + +Run your tests: + +```bash +# Fuzzing mode +komet test + +# Formal verification mode +komet prove run +``` + +--- + +## 🎯 How It Works + +### Fuzzing vs. Formal Verification + +| Approach | Coverage | Speed | Guarantees | +|----------|----------|-------|------------| +| **Unit Tests** | Sample inputs | Fast | Limited | +| **Fuzzing** | Random inputs | Fast | Probabilistic | +| **Formal Verification** | **All possible inputs** | Slower | **Mathematical proof** | + +### The Komet Advantage + +Fuzzing is a powerful upgrade from unit testingβ€”it automatically explores thousands of randomized inputs to uncover edge cases quickly. However, traditional fuzzing struggles with complex nested conditions and may miss critical edge cases. **Komet's symbolic execution** systematically explores all feasible code paths using symbolic variables, providing: + +- βœ… Comprehensive path coverage +- βœ… Automatic postcondition verification +- βœ… Guaranteed correctness proofs +- βœ… Detection of subtle logical errors + +Fuzzing mode provides fast feedback during active development, helping catch bugs quickly as you write code, while prove mode ensures complete correctness before deployment by verifying all possible execution paths. + +--- + +## πŸ“š Documentation + +- **[Official Documentation](https://docs.runtimeverification.com/komet)** - Complete guides and API reference +- **[Komet Example Tutorial](https://docs.runtimeverification.com/komet/guides/komet-example)** - Step-by-step walkthrough +- **[Cheat Functions](https://docs.runtimeverification.com/komet/guides/cheat-functions)** - Advanced testing utilities +- **[Video Demo](https://www.youtube.com/watch?v=76VD0aKPXGE)** - Real-world fxDAO contract verification + +--- + +## πŸ—οΈ Technical Architecture + +Komet is built on a solid foundation of formal methods: + +- **K Semantics Framework**: Industry-standard formal semantics and verification technology +- **KWasm**: WebAssembly semantics for precise execution modeling +- **Rust Integration**: Native toolchain compatibility +- **Soroban SDK**: First-class support for Stellar smart contracts + +--- + +## 🀝 Community + +Join the Komet community and get help from experts: + +- πŸ’¬ **[Discord](https://discord.gg/CurfmXNtbN)** - Chat with the team and other developers +- 🌐 **[Homepage](https://komet.runtimeverification.com)** - Latest news and updates +- πŸ“– **[Resources](https://docs.runtimeverification.com/komet/learn-more/resources)** - Additional learning materials +- πŸ› **[Issues](../../issues)** - Report bugs or request features + +--- + +## πŸ› οΈ Development Status + +Komet is actively maintained by [Runtime Verification](https://runtimeverification.com), a leader in formal verification technology. We're continuously improving the tool based on community feedback and real-world usage. + +### Roadmap + +- Advanced Soroban Wasm debugger with Soroban-specific state inspection and IDE integrations +- Enhanced symbolic execution performance +- Additional cheat functions for testing +- IDE integrations and tooling improvements +- Expanded example library + +--- + +## πŸ“„ License + +Komet is released under the BSD-3-Clause License. See [LICENSE](LICENSE) for details. + +--- + +## πŸ™ Acknowledgments + +Built with ❀️ by [Runtime Verification](https://runtimeverification.com) + +Special thanks to the Stellar Foundation and the Soroban developer community for their support and feedback. + +--- -## For Developers +
-Use `make` to run common tasks (see the [Makefile](Makefile) for a complete list of available targets). +**[Get Started Now](https://docs.runtimeverification.com/komet)** | **[Join Discord](https://discord.gg/CurfmXNtbN)** | **[Report Issues](../../issues)** -* `make build`: Build wheel -* `make check`: Check code style -* `make format`: Format code -* `make test-unit`: Run unit tests +Made with the K Framework | Securing the Future of Smart Contracts -For interactive use, spawn a shell with `poetry shell` (after `poetry install`), then run an interpreter. +
diff --git a/media/komet-fuzzing.gif b/media/komet-fuzzing.gif new file mode 100644 index 0000000..02867d8 Binary files /dev/null and b/media/komet-fuzzing.gif differ diff --git a/package/version b/package/version index 8076b7d..416eb55 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.72 +0.1.73 diff --git a/pyproject.toml b/pyproject.toml index a16b48d..d11ad4f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "komet" -version = "0.1.72" +version = "0.1.73" description = "K tooling for the Soroban platform" authors = [ "Runtime Verification, Inc. ",