From b1bea3d54987cbf54e2c2daad86c978116022d15 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Fri, 13 Feb 2026 19:08:56 +0400 Subject: [PATCH 1/3] Update Komet description in `ecosystem.md`, `security.md` --- skill/ecosystem.md | 8 +++++++- skill/security.md | 9 ++++++++- 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/skill/ecosystem.md b/skill/ecosystem.md index 6637244..3e83e7f 100644 --- a/skill/ecosystem.md +++ b/skill/ecosystem.md @@ -213,7 +213,13 @@ 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**: [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). diff --git a/skill/security.md b/skill/security.md index 1aa7cac..f1e7deb 100644 --- a/skill/security.md +++ b/skill/security.md @@ -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 From d90796212e128d92704e08d967c270dabf2e9a73 Mon Sep 17 00:00:00 2001 From: Palina Date: Thu, 19 Feb 2026 19:06:12 +0400 Subject: [PATCH 2/3] Unify Reports between `ecosystem.md` and `security.md` Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- skill/ecosystem.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/skill/ecosystem.md b/skill/ecosystem.md index 3e83e7f..3346810 100644 --- a/skill/ecosystem.md +++ b/skill/ecosystem.md @@ -218,7 +218,8 @@ Formal verification and testing tool designed for Soroban (SCF-funded). - **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**: [TokenOps audit and verification report](https://github.com/runtimeverification/publications/blob/main/reports/smart-contracts/TokenOps.pdf) +- **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) From 267d944322d789ccb64e6f458a9e5b375bcba9ae Mon Sep 17 00:00:00 2001 From: Palina Date: Thu, 19 Feb 2026 19:06:59 +0400 Subject: [PATCH 3/3] Make capitalization consistent in `security.md` Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- skill/security.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/skill/security.md b/skill/security.md index f1e7deb..bc0004d 100644 --- a/skill/security.md +++ b/skill/security.md @@ -458,7 +458,7 @@ Purpose-built formal verification for Soroban — first WASM platform supported Formal verification and testing tool built specifically for Soroban (SCF-funded). - **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 +- **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)