Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion skill/ecosystem.md
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,14 @@ Formal verification for Soroban — first WASM platform supported by Certora.

#### Runtime Verification — Komet
Formal verification and testing tool designed for Soroban (SCF-funded).
- **Blog**: https://runtimeverification.com/blog/introducing-komet-smart-contract-testing-and-verification-tool-for-soroban-created-by-runtime-verification
- **Docs**: https://docs.runtimeverification.com/komet
- **Repo**: https://github.com/runtimeverification/komet
- **Spec Language**: Rust — property-based tests written in the same language as Soroban contracts
- **Operates at**: WASM bytecode level via [KWasm semantics](https://github.com/runtimeverification/wasm-semantics) (eliminates compiler trust assumptions)
- **Features**: Fuzzing, testing, formal verification
- **Reports**: https://github.com/runtimeverification/publications
- **Example**: [TokenOps audit and verification report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/TokenOps.pdf)
- **Blog**: [Introducing Komet](https://runtimeverification.com/blog/introducing-komet-smart-contract-testing-and-verification-tool-for-soroban-created-by-runtime-verification)

#### Soroban Security Portal (Inferara)
Community security knowledge base (SCF-funded).
Expand Down
9 changes: 8 additions & 1 deletion skill/security.md
Original file line number Diff line number Diff line change
Expand Up @@ -456,7 +456,14 @@ Purpose-built formal verification for Soroban — first WASM platform supported

#### Runtime Verification — Komet
Formal verification and testing tool built specifically for Soroban (SCF-funded).
- **Blog**: https://runtimeverification.com/blog/introducing-komet-smart-contract-testing-and-verification-tool-for-soroban-created-by-runtime-verification
- **Docs**: https://docs.runtimeverification.com/komet
- **Repo**: https://github.com/runtimeverification/komet
- **Spec language**: Rust — property-based tests written in the same language as Soroban contracts
- **Operates at**: WASM bytecode level via [KWasm semantics](https://github.com/runtimeverification/wasm-semantics) (eliminates compiler trust assumptions)
- **Features**: Fuzzing, testing, formal verification
- **Reports**: [RV publications](https://github.com/runtimeverification/publications)
- **Example**: [TokenOps audit and verification report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/TokenOps.pdf)
- **Blog**: [Introducing Komet](https://runtimeverification.com/blog/introducing-komet-smart-contract-testing-and-verification-tool-for-soroban-created-by-runtime-verification)

### Security Knowledge Base

Expand Down