From 95353332fa91afa72f9650b92623fe7986584390 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 19 Feb 2026 21:37:08 +0100 Subject: [PATCH 1/7] docs: rewrite org profile around the verified toolchain narrative MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Feature Kiln, Meld, Loom, and Synth as the core pipeline with the actual compose→fuse→optimize→run/compile flow. Replace the flat catalog of projects with a narrative structure, compact ecosystem sections, and formal verification as the central differentiator. Co-Authored-By: Claude Opus 4.6 --- profile/README.md | 293 ++++++---------------------------------------- 1 file changed, 37 insertions(+), 256 deletions(-) diff --git a/profile/README.md b/profile/README.md index fdede67..da7a8b8 100644 --- a/profile/README.md +++ b/profile/README.md @@ -2,211 +2,67 @@ # PulseEngine -### Infrastructure for AI and WebAssembly +### Formally Verified WebAssembly Toolchain -*Exploring the intersection where AI agents interact safely with real-world systems through WebAssembly's security model* +*From component composition to native execution — every transformation proven correct*
![Rust](https://img.shields.io/badge/Rust-000000?style=flat&logo=rust&logoColor=white) ![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat&logo=webassembly&logoColor=white) ![Bazel](https://img.shields.io/badge/Bazel-43A047?style=flat&logo=bazel&logoColor=white) -![C++](https://img.shields.io/badge/C++-00599C?style=flat&logo=cplusplus&logoColor=white) - -[View Repositories](https://github.com/orgs/pulseengine/repositories) • [Documentation](#project-details) - -
-## What We're Building +[   Repositories   ](https://github.com/orgs/pulseengine/repositories)    [   Documentation   ](https://docs.rs/pulseengine-mcp-protocol) -PulseEngine develops infrastructure at the intersection of AI and WebAssembly, ranging from WASI proposals to production-tested implementations. Our work focuses on enabling AI systems to safely interact with real-world applications through WebAssembly's capability-based security model. +
-## Core Infrastructure +## The Toolchain - - - - - -
+We build infrastructure for running WebAssembly where correctness is non-negotiable — automotive, medical, industrial, aerospace. Four projects form a pipeline, each stage carrying formal proof of correctness. -### WebAssembly Runtime -**[wrt](https://github.com/pulseengine/wrt)** - -Safety-critical WebAssembly runtime with Component Model support. 22+ interconnected crates designed for automotive (ASIL-D), aerospace (DO-178C), and medical (IEC 62304) applications. - -**Architecture** -Core execution engine, formal verification with 227 Kani harnesses, capability-based memory system, no_std compatibility - -**Development Stage** -Advanced beta - foundational infrastructure production-grade, core execution engine under active development - - - -### MCP Framework -**[mcp](https://github.com/pulseengine/mcp)** - -Rust framework for building Model Context Protocol servers. Extracted from production home automation deployment with 30+ tools. 12 modular crates covering protocol, security, auth, and monitoring. - -**Features** -Complete MCP 2025-06-18 implementation, stdio/HTTP/WebSocket transports, 1,071 test functions, 80% code coverage - -**Development Stage** -Production-ready beta (v0.13.0) - actively used in real systems, published to crates.io - -
+``` + Components ───► Meld ───► Loom ───► Kiln execute + fuse optimize runtime + └──► Synth native ARM + compile +```
-## Build & Development Tools - - - - - -
-### Bazel Rules -**[rules_wasm_component](https://github.com/pulseengine/rules_wasm_component)** - -Modern Bazel rules for WebAssembly Component Model development. Supports Rust, Go, C++, and JavaScript with multi-profile builds and 73% faster compilation. - -**Highlights** -87 Starlark files, 415+ rule definitions, 30+ working examples, hermetic builds, OCI publishing, component signing - -**Development Stage** -Beta → production-ready (v1.0.0) - comprehensive CI/CD, suitable for production with v2.0 planned - - - -### WebAssembly Signing -**[wsc](https://github.com/pulseengine/wsc)** - -Enhanced WebAssembly signing toolkit with Rekor verification, based on wasmsign2. Bazel integration, keyless signing, WIT Component Model support. - -**Security** -Checkpoint-based verification, key fingerprint validation, origin verification, cross-shard attack prevention - -**Development Stage** -Active development - core signing/verification functional, Rekor validation operational - -
- -### WebAssembly Optimizer -**[loom](https://github.com/pulseengine/loom)** - -WebAssembly optimizer built with Cranelift's ISLE DSL. Declarative optimization rules with stateful dataflow analysis for constant propagation and memory optimization. +### [Kiln](https://github.com/pulseengine/kiln) -**Approach** -Novel contribution: extends ISLE's pure functional term rewriting with stateful tracking of locals and memory state - -**Development Stage** -Proof of concept - 40+ operations, demonstrates feasibility of ISLE-based WASM optimization +WebAssembly runtime for safety-critical systems. Full Component Model and WASI Preview 2 support with a modular `no_std` architecture built for embedded, automotive, medical, and aerospace environments. Memory safety guaranteed through Kani bounded model checking. -### File Operations -**[bazel-file-ops-component](https://github.com/pulseengine/bazel-file-ops-component)** - -Universal file operations for Bazel via WebAssembly components. Dual implementation (TinyGo for security, Rust for performance) with WASM sandboxing. - -**Cross-Platform** -Replaces platform-specific scripts with sandboxed components working identically on Linux, macOS, Windows +### [Meld](https://github.com/pulseengine/meld) -**Development Stage** -Active development - security model established, integration with rules_wasm_component ongoing +Statically fuses multiple WebAssembly components into a single core module. Eliminates runtime linking entirely — import resolution, index-space merging, and canonical ABI adapter generation happen at build time. Transformation correctness verified through Rocq formal proofs.
- -
- -## AI Integration - - - -
-### AI-Native Graphical Modeling -**[glsp-mcp](https://github.com/pulseengine/glsp-mcp)** +### [Loom](https://github.com/pulseengine/loom) -First implementation of Graphical Language Server Protocol using MCP. Enables AI agents to create and manipulate diagrams through natural language with WebAssembly component execution. - -**Stack** -Rust backend (23,722 lines), TypeScript frontend (39,571 lines), wasmtime 24.0 runtime, multi-database layer (PostgreSQL, InfluxDB, Redis) - -**Demo** -15+ ADAS components showing automotive system simulation with YOLOv5n neural network integration - -**Development Stage** -Advanced MVP/beta - core features functional, production path identified +Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass proven correct through Z3 SMT verification and Rocq mechanized proofs. Includes a fused mode purpose-built for Meld output. -### WASI-MCP Proposal -**[wasi-mcp](https://github.com/pulseengine/wasi-mcp)** - -Proposed WebAssembly System Interface API for Model Context Protocol, targeting WASI Preview3. Complete typed WIT interfaces mapping MCP protocol operations. - -**Coverage** -Full MCP 2025-06-18 specification - resources, tools, prompts, streaming, pagination, notifications - -**Approach** -Protocol-faithful design following successful WASI proposals (wasi-http, wasi-filesystem patterns) - -**Development Stage** -Phase 0 pre-proposal - WIT interfaces complete, seeking stakeholder feedback for Phase 1 - -
- -
- -## Production MCP Servers - - - - - - @@ -214,102 +70,31 @@ Automated template for creating MCP servers with PulseEngine framework. Example
-## Architecture Overview - -Our projects form an integrated ecosystem for AI-WebAssembly development: - -``` -┌─────────────────────────────────────────────────────────┐ -│ AI Integration Layer │ -│ • glsp-mcp: AI-native applications │ -│ • studio-mcp, timedate-mcp: Production servers │ -└─────────────────────────────────────────────────────────┘ - ↕ -┌─────────────────────────────────────────────────────────┐ -│ Protocol & Interface Layer │ -│ • mcp: Rust framework for MCP servers │ -│ • wasi-mcp: Standardization for WASI ecosystem │ -└─────────────────────────────────────────────────────────┘ - ↕ -┌─────────────────────────────────────────────────────────┐ -│ WebAssembly Runtime Layer │ -│ • wrt: Safety-critical WASM runtime │ -│ • loom: Optimization engine │ -│ • wsc: Component signing & verification │ -└─────────────────────────────────────────────────────────┘ - ↕ -┌─────────────────────────────────────────────────────────┐ -│ Build & Developer Tools │ -│ • rules_wasm_component: Bazel integration │ -│ • bazel-file-ops-component: Cross-platform operations │ -│ • template-mcp-server: Quick start templates │ -└─────────────────────────────────────────────────────────┘ -``` +> [!TIP] +> **Correctness at every layer** — Kani bounded model checking in the runtime, Rocq mechanized proofs for fusion and optimization, Z3 SMT verification for compilation. No transformation ships without a proof.
-## Vision & Focus Areas +## Ecosystem -We're exploring what becomes possible when AI systems can safely interact with real-world systems through WebAssembly's security sandbox. +#### Build & Verification -| Focus Area | What We're Building | -|------------|---------------------| -| **Safety-Critical Systems** | Infrastructure for automotive (ASIL-D), medical (IEC 62304), and industrial applications with formal verification and certification frameworks | -| **AI-Native Development** | Tools treating AI agents as first-class participants - from diagram generation to build system integration | -| **Secure Integration** | Capability-based security allowing AI to control physical systems in vehicles, factories, and homes with verifiable safety properties | -| **Universal Portability** | Same code from microcontrollers to cloud infrastructure through WebAssembly's platform independence | +- [**rules_wasm_component**](https://github.com/pulseengine/rules_wasm_component) — Bazel rules for WebAssembly Component Model across Rust, Go, C++, and JavaScript +- [**rules_rocq_rust**](https://github.com/pulseengine/rules_rocq_rust) — Bazel rules for Rocq theorem proving and Rust formal verification +- [**rules_moonbit**](https://github.com/pulseengine/rules_moonbit) — Bazel rules for MoonBit with hermetic toolchain support +- [**wsc**](https://github.com/pulseengine/wsc) — WebAssembly signing and verification with Sigstore/Rekor integration -
+#### AI & MCP -## Development Maturity +- [**mcp**](https://github.com/pulseengine/mcp) — Rust framework for building Model Context Protocol servers and clients +- [**glsp-mcp**](https://github.com/pulseengine/glsp-mcp) — AI-native graphical modeling with MCP integration and WebAssembly component execution +- [**wasi-mcp**](https://github.com/pulseengine/wasi-mcp) — Proposed WASI API for Model Context Protocol, targeting Preview 3 -Our projects span different maturity stages, from proposals to production: +#### Developer Tools -| Stage | Projects | Characteristics | -|-------|----------|-----------------| -| **🚀 Production** | mcp framework, studio-mcp, timedate-mcp | Published to registries, real-world deployments, comprehensive testing | -| **🔄 Advanced Beta** | wrt runtime, rules_wasm_component | Near-complete features, extensive infrastructure, production-quality tooling | -| **🚧 Active Development** | glsp-mcp, wsc, bazel-file-ops-component | Core features functional, integration ongoing, clear production path | -| **📝 Proposals & Research** | wasi-mcp, loom | Standards work, proof-of-concept implementations, seeking feedback | -| **🛠️ Developer Tools** | template-mcp-server | Onboarding and productivity tools | - -
- -## Project Metrics - -Based on comprehensive codebase analysis: - -| Repository | Language | Lines of Code | Commits | Test Coverage | Stage | -|------------|----------|---------------|---------|---------------|-------| -| wrt | Rust | 428,004 | 743 | 100+ test files, 227 Kani harnesses | Advanced Beta | -| mcp | Rust | 102,000 | 317 | 1,071 tests, 80% coverage enforced | Production Beta | -| glsp-mcp | Rust/TypeScript | 63,293 | 221 | Integration tests, UI demos | Advanced MVP | -| rules_wasm_component | Starlark/Rust | 252 files | 519 | 46 test builds, CI/CD | Beta → Production | -| wasi-mcp | WIT | - | - | Spec-complete | Phase 0 Proposal | -| studio-mcp | Rust | - | - | Production deployment | Production | -| wsc | Rust | - | - | Core functional | Active Dev | - -
- -## The Opportunity - -Traditional AI systems operate in isolation from real-world systems. WebAssembly's security model offers a path to safely bridge this gap. By treating AI agents as first-class citizens in our infrastructure, we're working toward systems where: - -- AI safely controls physical systems in vehicles, factories, and homes through verified WebAssembly components -- Developers build AI-aware applications with cryptographic security guarantees and formal verification -- Code runs consistently from embedded microcontrollers to cloud deployments with identical security properties -- Component composition enables complex AI workflows with modular, auditable security boundaries - -
- -## Technical Foundation - -**Languages:** Rust (primary), C++, Go, JavaScript/TypeScript -**WebAssembly:** Component Model, WASI Preview2/3, wasmtime runtime -**Build Systems:** Bazel (bzlmod), Cargo workspaces -**Safety:** Formal verification (Kani), ASIL-D compliance frameworks, capability-based security -**AI Integration:** Model Context Protocol, Ollama LLM, WASI-NN -**Standards:** Active participation in WASI standardization +- [**thrum**](https://github.com/pulseengine/thrum) — Gate-based pipeline orchestrator for autonomous AI-driven development +- [**temper**](https://github.com/pulseengine/temper) — GitHub App that hardens repositories to organizational standards +- [**wasm-component-examples**](https://github.com/pulseengine/wasm-component-examples) — Working examples for Component Model development in C, C++, Go, and Rust
@@ -317,10 +102,6 @@ Traditional AI systems operate in isolation from real-world systems. WebAssembly
-*Work in progress. All projects under active development.* - -**[Explore Repositories →](https://github.com/orgs/pulseengine/repositories)** | **[MCP Framework Docs](https://docs.rs/pulseengine-mcp-protocol)** - -Built with a focus on safety, security, and enabling new possibilities at the intersection of AI and WebAssembly +Rust · WebAssembly Component Model · WASI Preview 2/3 · Bazel · Rocq · Z3 · Kani
From b95fd188114bf04c978f6e9badbcd594466b7c04 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 19 Feb 2026 21:49:29 +0100 Subject: [PATCH 2/7] docs: correct pipeline flow, elevate WSC, refine visual style MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Fix the toolchain pipeline: Meld → Loom → Synth → Kiln (sequential, not parallel). Elevate WSC from a bullet point to a featured section covering attestation chains, SLSA policies, keyless signing, and hardware security. Add branded flat-square badges with consistent dark label backgrounds, verification method badges per project card, sup/h6 typography hierarchy, details sections for ecosystem, and WSC as the cryptographic backbone spanning the pipeline diagram. Co-Authored-By: Claude Opus 4.6 --- profile/README.md | 134 +++++++++++++++++++++++++++++++--------------- 1 file changed, 90 insertions(+), 44 deletions(-) diff --git a/profile/README.md b/profile/README.md index da7a8b8..a4b7629 100644 --- a/profile/README.md +++ b/profile/README.md @@ -2,106 +2,152 @@ # PulseEngine -### Formally Verified WebAssembly Toolchain +Formally verified WebAssembly toolchain for safety-critical systems -*From component composition to native execution — every transformation proven correct* +  -
+![Rust](https://img.shields.io/badge/Rust-CE422B?style=flat-square&logo=rust&logoColor=white&labelColor=1a1b27) +![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat-square&logo=webassembly&logoColor=white&labelColor=1a1b27) +![Bazel](https://img.shields.io/badge/Bazel-43A047?style=flat-square&logo=bazel&logoColor=white&labelColor=1a1b27) +![Formally Verified](https://img.shields.io/badge/Formally_Verified-00C853?style=flat-square&logoColor=white&labelColor=1a1b27) -![Rust](https://img.shields.io/badge/Rust-000000?style=flat&logo=rust&logoColor=white) -![WebAssembly](https://img.shields.io/badge/WebAssembly-654FF0?style=flat&logo=webassembly&logoColor=white) -![Bazel](https://img.shields.io/badge/Bazel-43A047?style=flat&logo=bazel&logoColor=white) +  -
+[   Repositories   ](https://github.com/orgs/pulseengine/repositories)    [   Documentation   ](https://docs.rs/pulseengine-mcp-protocol)    [   Examples   ](https://github.com/pulseengine/wasm-component-examples) -[   Repositories   ](https://github.com/orgs/pulseengine/repositories)    [   Documentation   ](https://docs.rs/pulseengine-mcp-protocol) +
+ Kiln + · + Meld + · + Loom + · + Synth + · + WSC +
-
+  -## The Toolchain +## The Pipeline -We build infrastructure for running WebAssembly where correctness is non-negotiable — automotive, medical, industrial, aerospace. Four projects form a pipeline, each stage carrying formal proof of correctness. +Meld fuses. Loom optimizes. Synth compiles. Kiln fires. WSC verifies every step. ``` - Components ───► Meld ───► Loom ───► Kiln execute - fuse optimize runtime - └──► Synth native ARM - compile + wsc ── attest · sign · verify + ┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈ + + .wasm ───► Meld ───► Loom ───► Synth ───► Kiln + fuse optimize compile fire + Rocq Rocq + Z3 Z3 Kani ``` -
+ 
- -### WindRiver Studio -**[studio-mcp](https://github.com/pulseengine/studio-mcp)** - -MCP server for WindRiver Studio CLI with Pipeline Management integration, intelligent caching, multi-instance authentication. - -**Status:** Production-ready -**Published:** npm (@pulseengine/studio-mcp-server) - - - -### Time & Date -**[timedate-mcp](https://github.com/pulseengine/timedate-mcp)** - -Comprehensive time operations with timezone support, format detection, timezone conversion, built with chrono-tz. - -**Status:** Production-ready -**Published:** npm (@pulseengine/timedate-mcp-server) +### [Synth](https://github.com/pulseengine/synth) - - -### Template Server -**[template-mcp-server](https://github.com/pulseengine/template-mcp-server)** - -Automated template for creating MCP servers with PulseEngine framework. Example tools, resources, CI/CD workflows. - -**Purpose:** Developer onboarding -**Features:** Auto-setup script, validation, multi-platform binaries +Compiles WebAssembly to native ARM for embedded Cortex-M targets. Not just translation — program synthesis: exploring equivalent implementations to find provably optimal native code. Z3 translation validation ensures compiled output faithfully preserves WebAssembly semantics.
-### [Kiln](https://github.com/pulseengine/kiln) +### [Meld](https://github.com/pulseengine/meld) -WebAssembly runtime for safety-critical systems. Full Component Model and WASI Preview 2 support with a modular `no_std` architecture built for embedded, automotive, medical, and aerospace environments. Memory safety guaranteed through Kani bounded model checking. +![Rocq](https://img.shields.io/badge/verified_with-Rocq-00C853?style=flat-square&labelColor=1a1b27) + +Statically fuses multiple WebAssembly P2/P3 components into a single core module. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time — runtime linking eliminated entirely. Every transformation carries Rocq mechanized proofs covering parsing, resolution, merging, and adapter correctness. -### [Meld](https://github.com/pulseengine/meld) +### [Loom](https://github.com/pulseengine/loom) -Statically fuses multiple WebAssembly components into a single core module. Eliminates runtime linking entirely — import resolution, index-space merging, and canonical ABI adapter generation happen at build time. Transformation correctness verified through Rocq formal proofs. +![Rocq + Z3](https://img.shields.io/badge/verified_with-Rocq_+_Z3-00C853?style=flat-square&labelColor=1a1b27) + +Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass proven correct through Z3 SMT translation validation and Rocq mechanized proofs. Includes a fused mode purpose-built for Meld output.
-### [Loom](https://github.com/pulseengine/loom) +### [Synth](https://github.com/pulseengine/synth) -Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass proven correct through Z3 SMT verification and Rocq mechanized proofs. Includes a fused mode purpose-built for Meld output. +![Z3](https://img.shields.io/badge/verified_with-Z3-00C853?style=flat-square&labelColor=1a1b27) + +Compiles WebAssembly to native ARM for embedded Cortex-M targets. Not just translation — program synthesis: exploring equivalent implementations for provably optimal native code. Pattern-based instruction selection, AAPCS calling conventions, and ELF generation. Z3 translation validation ensures the compiled output faithfully preserves WebAssembly semantics. -### [Synth](https://github.com/pulseengine/synth) +### [Kiln](https://github.com/pulseengine/kiln) -Compiles WebAssembly to native ARM for embedded Cortex-M targets. Not just translation — program synthesis: exploring equivalent implementations to find provably optimal native code. Z3 translation validation ensures compiled output faithfully preserves WebAssembly semantics. +![Kani](https://img.shields.io/badge/verified_with-Kani-00C853?style=flat-square&labelColor=1a1b27) +![no_std](https://img.shields.io/badge/no__std-compatible-654FF0?style=flat-square&labelColor=1a1b27) + +WebAssembly runtime for safety-critical systems. Full Component Model and WASI Preview 2 support with a modular `no_std` architecture for embedded, automotive, medical, and aerospace environments. Bounded allocations, deterministic execution, and memory safety guaranteed through Kani bounded model checking.
-
+  + +### [WSC](https://github.com/pulseengine/wsc) — Supply Chain Security + +![Sigstore](https://img.shields.io/badge/Sigstore-keyless_signing-654FF0?style=flat-square&labelColor=1a1b27) +![SLSA](https://img.shields.io/badge/SLSA-L4_provenance-00C853?style=flat-square&labelColor=1a1b27) + +The cryptographic backbone of the pipeline. Every stage — fusion, optimization, compilation — creates a signed transformation attestation recording what changed, which tool version ran, and cryptographic hashes of inputs and outputs. The full chain is verifiable end-to-end. + +Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool version and hash constraints. Hardware security via TPM 2.0. Offline verification for air-gapped embedded environments. IoT device provisioning with pre-provisioned trust bundles. All signatures embedded directly in WebAssembly modules — no external registry required. + +  + +> [!NOTE] +> **Correctness at every layer** — Kani bounded model checking in the runtime, Rocq mechanized proofs for fusion and optimization, Z3 SMT verification for compilation, and WSC attestation chains binding it all together. No transformation ships without a proof. + +  + +
+Build & Verification + +  + +- [**rules_wasm_component**](https://github.com/pulseengine/rules_wasm_component) — Bazel rules for WebAssembly Component Model across Rust, Go, C++, and JavaScript +- [**rules_rocq_rust**](https://github.com/pulseengine/rules_rocq_rust) — Bazel rules for Rocq theorem proving and Rust formal verification with hermetic Nix toolchains +- [**rules_moonbit**](https://github.com/pulseengine/rules_moonbit) — Bazel rules for MoonBit with hermetic toolchain support -> [!TIP] -> **Correctness at every layer** — Kani bounded model checking in the runtime, Rocq mechanized proofs for fusion and optimization, Z3 SMT verification for compilation. No transformation ships without a proof. +
-
+
+AI & MCP -## Ecosystem +  -#### Build & Verification +- [**mcp**](https://github.com/pulseengine/mcp) — Rust framework for building Model Context Protocol servers and clients, published to crates.io +- [**glsp-mcp**](https://github.com/pulseengine/glsp-mcp) — AI-native graphical modeling with MCP integration and WebAssembly component execution +- [**wasi-mcp**](https://github.com/pulseengine/wasi-mcp) — Proposed WASI API for Model Context Protocol, targeting Preview 3 standardization -- [**rules_wasm_component**](https://github.com/pulseengine/rules_wasm_component) — Bazel rules for WebAssembly Component Model across Rust, Go, C++, and JavaScript -- [**rules_rocq_rust**](https://github.com/pulseengine/rules_rocq_rust) — Bazel rules for Rocq theorem proving and Rust formal verification -- [**rules_moonbit**](https://github.com/pulseengine/rules_moonbit) — Bazel rules for MoonBit with hermetic toolchain support -- [**wsc**](https://github.com/pulseengine/wsc) — WebAssembly signing and verification with Sigstore/Rekor integration +
-#### AI & MCP +
+Developer Tools -- [**mcp**](https://github.com/pulseengine/mcp) — Rust framework for building Model Context Protocol servers and clients -- [**glsp-mcp**](https://github.com/pulseengine/glsp-mcp) — AI-native graphical modeling with MCP integration and WebAssembly component execution -- [**wasi-mcp**](https://github.com/pulseengine/wasi-mcp) — Proposed WASI API for Model Context Protocol, targeting Preview 3 +  -#### Developer Tools +- [**thrum**](https://github.com/pulseengine/thrum) — Gate-based pipeline orchestrator for autonomous AI-driven development +- [**temper**](https://github.com/pulseengine/temper) — GitHub App that hardens repositories to organizational standards +- [**wasm-component-examples**](https://github.com/pulseengine/wasm-component-examples) — Working examples for Component Model development in C, C++, Go, and Rust +- [**moonbit_checksum_updater**](https://github.com/pulseengine/moonbit_checksum_updater) — Native MoonBit checksum management with GitHub API integration -- [**thrum**](https://github.com/pulseengine/thrum) — Gate-based pipeline orchestrator for autonomous AI-driven development -- [**temper**](https://github.com/pulseengine/temper) — GitHub App that hardens repositories to organizational standards -- [**wasm-component-examples**](https://github.com/pulseengine/wasm-component-examples) — Working examples for Component Model development in C, C++, Go, and Rust +
-
+  ---
-Rust · WebAssembly Component Model · WASI Preview 2/3 · Bazel · Rocq · Z3 · Kani +Rust · WebAssembly Component Model · WASI Preview 2/3 · Bazel · Rocq · Z3 · Kani · Sigstore
From 69bf585becd81b86d651e63c22994217f9f6e88d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 19 Feb 2026 21:56:13 +0100 Subject: [PATCH 3/7] docs: replace ASCII pipeline with SVG diagram Clean SVG with rounded boxes, purple arrows, green verification labels, and WSC spanning dashed line. Adapts to dark/light mode via CSS prefers-color-scheme media query. Descriptive alt text for accessibility. Co-Authored-By: Claude Opus 4.6 --- profile/README.md | 11 ++---- profile/assets/pipeline.svg | 72 +++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+), 8 deletions(-) create mode 100644 profile/assets/pipeline.svg diff --git a/profile/README.md b/profile/README.md index a4b7629..287fe92 100644 --- a/profile/README.md +++ b/profile/README.md @@ -35,14 +35,9 @@ Meld fuses. Loom optimizes. Synth compiles. Kiln fires. WSC verifies every step. -``` - wsc ── attest · sign · verify - ┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈┈ - - .wasm ───► Meld ───► Loom ───► Synth ───► Kiln - fuse optimize compile fire - Rocq Rocq + Z3 Z3 Kani -``` +
+PulseEngine Pipeline: .wasm → Meld (fuse, Rocq) → Loom (optimize, Rocq+Z3) → Synth (compile, Z3) → Kiln (fire, Kani) — with WSC attestation at every stage +
  diff --git a/profile/assets/pipeline.svg b/profile/assets/pipeline.svg new file mode 100644 index 0000000..ce296d5 --- /dev/null +++ b/profile/assets/pipeline.svg @@ -0,0 +1,72 @@ + + + + + wsc · attest · sign · verify + + + + .wasm + + + + + + Meld + fuse + Rocq + + + + + + + + Loom + optimize + Rocq + Z3 + + + + + + + + Synth + compile + Z3 + + + + + + + + Kiln + fire + Kani + From 14174184bcd309dfcaadb7010421d444678ae452 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 19 Feb 2026 22:00:00 +0100 Subject: [PATCH 4/7] docs: rename WSC to Sigil across README and pipeline diagram MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Sigil — a seal of authenticity. Fits the forge metaphor: "Meld fuses. Loom weaves. Synth compiles. Kiln fires. Sigil seals." Links still point to pulseengine/wsc pending actual repo rename. Co-Authored-By: Claude Opus 4.6 --- profile/README.md | 10 +++++----- profile/assets/pipeline.svg | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/profile/README.md b/profile/README.md index 287fe92..409b23b 100644 --- a/profile/README.md +++ b/profile/README.md @@ -24,7 +24,7 @@ · Synth · - WSC + Sigil @@ -33,10 +33,10 @@ ## The Pipeline -Meld fuses. Loom optimizes. Synth compiles. Kiln fires. WSC verifies every step. +Meld fuses. Loom weaves. Synth compiles. Kiln fires. Sigil seals.
-PulseEngine Pipeline: .wasm → Meld (fuse, Rocq) → Loom (optimize, Rocq+Z3) → Synth (compile, Z3) → Kiln (fire, Kani) — with WSC attestation at every stage +PulseEngine Pipeline: .wasm → Meld (fuse, Rocq) → Loom (optimize, Rocq+Z3) → Synth (compile, Z3) → Kiln (fire, Kani) — with Sigil attestation at every stage
  @@ -87,7 +87,7 @@ WebAssembly runtime for safety-critical systems. Full Component Model and WASI P   -### [WSC](https://github.com/pulseengine/wsc) — Supply Chain Security +### [Sigil](https://github.com/pulseengine/wsc) — Supply Chain Security ![Sigstore](https://img.shields.io/badge/Sigstore-keyless_signing-654FF0?style=flat-square&labelColor=1a1b27) ![SLSA](https://img.shields.io/badge/SLSA-L4_provenance-00C853?style=flat-square&labelColor=1a1b27) @@ -99,7 +99,7 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio   > [!NOTE] -> **Correctness at every layer** — Kani bounded model checking in the runtime, Rocq mechanized proofs for fusion and optimization, Z3 SMT verification for compilation, and WSC attestation chains binding it all together. No transformation ships without a proof. +> **Correctness at every layer** — Kani bounded model checking in the runtime, Rocq mechanized proofs for fusion and optimization, Z3 SMT verification for compilation, and Sigil attestation chains binding it all together. No transformation ships without a proof.   diff --git a/profile/assets/pipeline.svg b/profile/assets/pipeline.svg index ce296d5..be53758 100644 --- a/profile/assets/pipeline.svg +++ b/profile/assets/pipeline.svg @@ -25,8 +25,8 @@ } - - wsc · attest · sign · verify + + sigil · attest · sign · verify From 5ef2226e5cb929ad1bd38afdfd6519ad7d1a4354 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 19 Feb 2026 22:03:04 +0100 Subject: [PATCH 5/7] =?UTF-8?q?docs:=20Synth=20transpiles,=20verification?= =?UTF-8?q?=20is=20cross-cutting,=20add=20Verus,=20rename=20wsc=E2=86=92si?= =?UTF-8?q?gil?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Synth "transpiles" not "compiles" (WASM→ARM is between two low-level representations) - Remove per-project verification tool assignments from SVG and cards; Rocq, Kani, Z3, and Verus are used across the entire toolchain - Add rules_verus to Build & Verification ecosystem - Add Verus to footer tech stack and verification callout - Rename GitHub repo wsc→sigil and update all links - SVG viewBox trimmed (no proof labels below boxes = shorter) Co-Authored-By: Claude Opus 4.6 --- profile/README.md | 28 +++++++++++----------------- profile/assets/pipeline.svg | 22 ++++++++-------------- 2 files changed, 19 insertions(+), 31 deletions(-) diff --git a/profile/README.md b/profile/README.md index 409b23b..7aef11c 100644 --- a/profile/README.md +++ b/profile/README.md @@ -24,7 +24,7 @@ · Synth · - Sigil + Sigil @@ -33,10 +33,10 @@ ## The Pipeline -Meld fuses. Loom weaves. Synth compiles. Kiln fires. Sigil seals. +Meld fuses. Loom weaves. Synth transpiles. Kiln fires. Sigil seals.
-PulseEngine Pipeline: .wasm → Meld (fuse, Rocq) → Loom (optimize, Rocq+Z3) → Synth (compile, Z3) → Kiln (fire, Kani) — with Sigil attestation at every stage +PulseEngine Pipeline: .wasm → Meld (fuse) → Loom (optimize) → Synth (transpile) → Kiln (fire) — with Sigil attestation at every stage
  @@ -47,18 +47,14 @@ Meld fuses. Loom weaves. Synth compiles. Kiln fires. Sigil seals. ### [Meld](https://github.com/pulseengine/meld) -![Rocq](https://img.shields.io/badge/verified_with-Rocq-00C853?style=flat-square&labelColor=1a1b27) - -Statically fuses multiple WebAssembly P2/P3 components into a single core module. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time — runtime linking eliminated entirely. Every transformation carries Rocq mechanized proofs covering parsing, resolution, merging, and adapter correctness. +Statically fuses multiple WebAssembly P2/P3 components into a single core module. Import resolution, index-space merging, and canonical ABI adapter generation happen at build time — runtime linking eliminated entirely. Every transformation carries mechanized proofs covering parsing, resolution, merging, and adapter correctness. ### [Loom](https://github.com/pulseengine/loom) -![Rocq + Z3](https://img.shields.io/badge/verified_with-Rocq_+_Z3-00C853?style=flat-square&labelColor=1a1b27) - -Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass proven correct through Z3 SMT translation validation and Rocq mechanized proofs. Includes a fused mode purpose-built for Meld output. +Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern-matching engine. Constant folding, strength reduction, CSE, inlining, dead code elimination — each pass proven correct through SMT translation validation and mechanized proofs. Includes a fused mode purpose-built for Meld output. @@ -67,19 +63,16 @@ Twelve-pass WebAssembly optimization pipeline built on Cranelift's ISLE pattern- ### [Synth](https://github.com/pulseengine/synth) -![Z3](https://img.shields.io/badge/verified_with-Z3-00C853?style=flat-square&labelColor=1a1b27) - -Compiles WebAssembly to native ARM for embedded Cortex-M targets. Not just translation — program synthesis: exploring equivalent implementations for provably optimal native code. Pattern-based instruction selection, AAPCS calling conventions, and ELF generation. Z3 translation validation ensures the compiled output faithfully preserves WebAssembly semantics. +Transpiles WebAssembly to native ARM for embedded Cortex-M targets. Not just translation — program synthesis: exploring equivalent implementations for provably optimal native code. Pattern-based instruction selection, AAPCS calling conventions, and ELF generation. Translation validation ensures the transpiled output faithfully preserves WebAssembly semantics. ### [Kiln](https://github.com/pulseengine/kiln) -![Kani](https://img.shields.io/badge/verified_with-Kani-00C853?style=flat-square&labelColor=1a1b27) ![no_std](https://img.shields.io/badge/no__std-compatible-654FF0?style=flat-square&labelColor=1a1b27) -WebAssembly runtime for safety-critical systems. Full Component Model and WASI Preview 2 support with a modular `no_std` architecture for embedded, automotive, medical, and aerospace environments. Bounded allocations, deterministic execution, and memory safety guaranteed through Kani bounded model checking. +WebAssembly runtime for safety-critical systems. Full Component Model and WASI Preview 2 support with a modular `no_std` architecture for embedded, automotive, medical, and aerospace environments. Bounded allocations, deterministic execution, and memory safety through bounded model checking and formal verification. @@ -87,7 +80,7 @@ WebAssembly runtime for safety-critical systems. Full Component Model and WASI P   -### [Sigil](https://github.com/pulseengine/wsc) — Supply Chain Security +### [Sigil](https://github.com/pulseengine/sigil) — Supply Chain Security ![Sigstore](https://img.shields.io/badge/Sigstore-keyless_signing-654FF0?style=flat-square&labelColor=1a1b27) ![SLSA](https://img.shields.io/badge/SLSA-L4_provenance-00C853?style=flat-square&labelColor=1a1b27) @@ -99,7 +92,7 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio   > [!NOTE] -> **Correctness at every layer** — Kani bounded model checking in the runtime, Rocq mechanized proofs for fusion and optimization, Z3 SMT verification for compilation, and Sigil attestation chains binding it all together. No transformation ships without a proof. +> **Correctness at every layer** — Rocq mechanized proofs, Kani bounded model checking, Z3 SMT verification, and Verus Rust verification are used across the toolchain — not confined to individual projects. Sigil attestation chains bind it all together. No transformation ships without a proof.   @@ -110,6 +103,7 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio - [**rules_wasm_component**](https://github.com/pulseengine/rules_wasm_component) — Bazel rules for WebAssembly Component Model across Rust, Go, C++, and JavaScript - [**rules_rocq_rust**](https://github.com/pulseengine/rules_rocq_rust) — Bazel rules for Rocq theorem proving and Rust formal verification with hermetic Nix toolchains +- [**rules_verus**](https://github.com/pulseengine/rules_verus) — Bazel rules for Verus Rust verification - [**rules_moonbit**](https://github.com/pulseengine/rules_moonbit) — Bazel rules for MoonBit with hermetic toolchain support @@ -143,6 +137,6 @@ Sigstore keyless signing for CI/CD. SLSA policy enforcement with per-tool versio
-Rust · WebAssembly Component Model · WASI Preview 2/3 · Bazel · Rocq · Z3 · Kani · Sigstore +Rust · WebAssembly Component Model · WASI Preview 2/3 · Bazel · Rocq · Z3 · Kani · Verus · Sigstore
diff --git a/profile/assets/pipeline.svg b/profile/assets/pipeline.svg index be53758..6ad59eb 100644 --- a/profile/assets/pipeline.svg +++ b/profile/assets/pipeline.svg @@ -1,33 +1,31 @@ - + - sigil · attest · sign · verify - + sigil · attest · sign · verify + .wasm @@ -38,7 +36,6 @@ Meld fuse - Rocq @@ -48,7 +45,6 @@ Loom optimize - Rocq + Z3 @@ -57,8 +53,7 @@ Synth - compile - Z3 + transpile @@ -68,5 +63,4 @@ Kiln fire - Kani From 51cfb256411e99b5cdb73a8d5fe1925fca70b220 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 19 Feb 2026 22:07:04 +0100 Subject: [PATCH 6/7] ci: add checks workflow with ci, lint, and test jobs - ci: validates required files exist - lint: checks relative image references in README resolve - test: validates SVG is well-formed XML Co-Authored-By: Claude Opus 4.6 --- .github/workflows/checks.yml | 47 ++++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 .github/workflows/checks.yml diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml new file mode 100644 index 0000000..64ae6d4 --- /dev/null +++ b/.github/workflows/checks.yml @@ -0,0 +1,47 @@ +name: Checks + +on: + push: + branches: [main] + pull_request: + branches: [main] + +jobs: + ci: + name: ci + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Validate files exist + run: | + test -f profile/README.md + test -f profile/assets/pipeline.svg + + lint: + name: lint + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Validate markdown + run: | + # Check for broken relative image references + grep -oP 'src="\.\/[^"]+"|srcset="\.\/[^"]+"' profile/README.md | \ + sed 's/.*"\.\//profile\//' | sed 's/".*//' | \ + while read -r file; do + if [ ! -f "$file" ]; then + echo "Missing referenced file: $file" + exit 1 + fi + done + echo "All referenced files exist" + + test: + name: test + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Validate SVG + run: | + # Check SVG is well-formed XML + xmllint --noout profile/assets/pipeline.svg + echo "SVG is valid" From 041386d997904921e5f8cdff1d150fa39bfd2977 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Fri, 20 Feb 2026 05:47:04 +0100 Subject: [PATCH 7/7] fix(ci): use python3 xml parser instead of xmllint xmllint is not available on ubuntu-latest runners by default. Python3 and xml.etree.ElementTree are always present. Co-Authored-By: Claude Opus 4.6 --- .github/workflows/checks.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/checks.yml b/.github/workflows/checks.yml index 64ae6d4..9693b00 100644 --- a/.github/workflows/checks.yml +++ b/.github/workflows/checks.yml @@ -43,5 +43,5 @@ jobs: - name: Validate SVG run: | # Check SVG is well-formed XML - xmllint --noout profile/assets/pipeline.svg + python3 -c "import xml.etree.ElementTree as ET; ET.parse('profile/assets/pipeline.svg')" echo "SVG is valid"