File contents WebAssembly Verifier
Verifies WebAssembly modules for safety, security, and correctness properties.
When to Use
Validating untrusted WASM modules
Building WASM security tools
Implementing sandboxes
Verifying memory safety
Proving absence of runtime errors
What This Skill Does
Type checks modules - Validates type correctnessVerifies stack - Balanced push/pop operationsChecks bounds - Memory access safetyValidates control flow - Structured execution
Key Concepts
Concept
Description
Type use Function type references
Block type Control flow return type
Stack polymorphism Dynamic stack height
Validation context Current type environment
Validation Rules
Category
Checks
Type use Index in bounds
Function Locals, return type
Stack Balanced pushes/pops
Control Proper label nesting
Memory Bounds, alignment
Tips
Implement incrementally by instruction class
Track stack height precisely
Handle unreachable code properly
Verify at load time, not runtime
Consider symbolic verification
Related Skills
webassembly-runtime - WASM executionmodel-checker - Model checkingtype-checker-generator - Type checkingwebassembly-runtime - Safe execution
Canonical References
Reference
Why It Matters
WebAssembly Specification - Validation Official validation spec
Haas et al., "Bringing the Web up to Speed with WebAssembly" (PLDI 2017) WASM design
WebAssembly Binary Toolkit Validator tools
Tradeoffs and Limitations
Approaches
Approach
Pros
Cons
Syntactic validation Fast, complete
No semantic proofs
Symbolic verification Deep properties
Slow, complex
Runtime checks Dynamic safety
Performance cost
Limitations
Cannot verify all runtime properties statically
Cannot prove termination
Limited introspection of data
Validation is sound but not complete
Research Tools & Artifacts
Real-world Wasm verification tools:
Tool
Why It Matters
wasm-validate Official validator
WABT Tool suite
wasm-micro-runtime Runtime
V8 JS engine with Wasm
Key Systems
W3C spec : StandardFirefox Wasm : Production
Research Frontiers
Current Wasm verification research:
Direction
Key Papers
Challenge
Security "Wasm Security"
Isolation
Verification "Verified Wasm"
Properties
Hot Topics
Wasm GC : Garbage collectionWasm WASI : System interface
Implementation Pitfalls
Common Wasm verification bugs:
Pitfall
Real Example
Prevention
Stack Stack underflow
Check
Converted and distributed by TomeVault — claim your Tome and manage your conversions.
1 --- 2 name: rainoftime-pl-skills-webassembly-verifier 3 description: WebAssembly Verifier 4 --- 5 6 # WebAssembly Verifier 7 8 Verifies WebAssembly modules for safety, security, and correctness properties. 9 10 ## When to Use 11 12 - Validating untrusted WASM modules 13 - Building WASM security tools 14 - Implementing sandboxes 15 - Verifying memory safety 16 - Proving absence of runtime errors 17 18 ## What This Skill Does 19 20 1. **Type checks modules** - Validates type correctness 21 2. **Verifies stack** - Balanced push/pop operations 22 3. **Checks bounds** - Memory access safety 23 4. **Validates control flow** - Structured execution 24 25 ## Key Concepts 26 27 | Concept | Description | 28 |---------|-------------| 29 | **Type use** | Function type references | 30 | **Block type** | Control flow return type | 31 | **Stack polymorphism** | Dynamic stack height | 32 | **Validation context** | Current type environment | 33 34 ## Validation Rules 35 36 | Category | Checks | 37 |----------|--------| 38 | **Type use** | Index in bounds | 39 | **Function** | Locals, return type | 40 | **Stack** | Balanced pushes/pops | 41 | **Control** | Proper label nesting | 42 | **Memory** | Bounds, alignment | 43 44 ## Tips 45 46 - Implement incrementally by instruction class 47 - Track stack height precisely 48 - Handle unreachable code properly 49 - Verify at load time, not runtime 50 - Consider symbolic verification 51 52 ## Related Skills 53 54 - `webassembly-runtime` - WASM execution 55 - `model-checker` - Model checking 56 - `type-checker-generator` - Type checking 57 - `webassembly-runtime` - Safe execution 58 59 ## Canonical References 60 61 | Reference | Why It Matters | 62 |-----------|----------------| 63 | **WebAssembly Specification - Validation** | Official validation spec | 64 | **Haas et al., "Bringing the Web up to Speed with WebAssembly" (PLDI 2017)** | WASM design | 65 | **WebAssembly Binary Toolkit** | Validator tools | 66 67 ## Tradeoffs and Limitations 68 69 ### Approaches 70 71 | Approach | Pros | Cons | 72 |----------|------|------| 73 | **Syntactic validation** | Fast, complete | No semantic proofs | 74 | **Symbolic verification** | Deep properties | Slow, complex | 75 | **Runtime checks** | Dynamic safety | Performance cost | 76 77 ### Limitations 78 79 - Cannot verify all runtime properties statically 80 - Cannot prove termination 81 - Limited introspection of data 82 - Validation is sound but not complete 83 84 ## Research Tools & Artifacts 85 86 Real-world Wasm verification tools: 87 88 | Tool | Why It Matters | 89 |------|----------------| 90 | **wasm-validate** | Official validator | 91 | **WABT** | Tool suite | 92 | **wasm-micro-runtime** | Runtime | 93 | **V8** | JS engine with Wasm | 94 95 ### Key Systems 96 97 - **W3C spec**: Standard 98 - **Firefox Wasm**: Production 99 100 ## Research Frontiers 101 102 Current Wasm verification research: 103 104 | Direction | Key Papers | Challenge | 105 |-----------|------------|-----------| 106 | **Security** | "Wasm Security" | Isolation | 107 | **Verification** | "Verified Wasm" | Properties | 108 109 ### Hot Topics 110 111 1. **Wasm GC**: Garbage collection 112 2. **Wasm WASI**: System interface 113 114 ## Implementation Pitfalls 115 116 Common Wasm verification bugs: 117 118 | Pitfall | Real Example | Prevention | 119 |---------|--------------|------------| 120 | **Stack** | Stack underflow | Check | 121 122 --- 123 > Converted and distributed by [TomeVault](https://tomevault.io/claim/rainoftime) — claim your Tome and manage your conversions. 124 <!-- tomevault:4.0:skill_md:2026-04-11 -->
commit b046efa385
Frequently asked questions How do I install the Rainoftime Pl Skills Webassembly Verifier skill? Run npx skillmds@latest add tomevault-io/rainoftime-pl-skills-webassembly-verifier in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.
What does the Rainoftime Pl Skills Webassembly Verifier skill do? WebAssembly Verifier It is listed under Coding & Dev Tools on SkillMD.
Is Rainoftime Pl Skills Webassembly Verifier safe to use? This skill has not completed SkillMD's automated safety review yet. Independent scanners report: SkillSpector: PASS, Skill Scanner: PASS. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.
Which AI agents work with Rainoftime Pl Skills Webassembly Verifier? This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.
Is Rainoftime Pl Skills Webassembly Verifier free to use? Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.
Who published Rainoftime Pl Skills Webassembly Verifier? tomevault-io (@tomevault-io) published this skill. Their other Agent Skills are listed on their SkillMD profile.
tomevault-io