+
+**[← Previous: What is Formal Semantics?](00_what_is_formal_semantics.md)** | **[Back to Home](../README.md)** | **[Next: WebAssembly Overview →](02_webassembly_overview.md)**
+
+
diff --git a/demos/formal_semantics_explorer/01_introduction/02_webassembly_overview.md b/demos/formal_semantics_explorer/01_introduction/02_webassembly_overview.md
new file mode 100644
index 000000000..9d0ee26cc
--- /dev/null
+++ b/demos/formal_semantics_explorer/01_introduction/02_webassembly_overview.md
@@ -0,0 +1,379 @@
+# WebAssembly Overview
+
+## What is WebAssembly?
+
+**WebAssembly (Wasm)** is a low-level, portable bytecode format designed as a compilation target for high-level languages. It enables near-native performance in web browsers and other runtime environments.
+
+## Key Characteristics
+
+### 1. **Stack-Based Virtual Machine**
+
+WebAssembly uses a **stack machine** model:
+
+```wasm
+;; Push values onto stack
+(i32.const 5) ;; Stack: [5]
+(i32.const 3) ;; Stack: [5, 3]
+
+;; Operate on stack values
+(i32.add) ;; Stack: [8]
+```
+
+### 2. **Statically Typed**
+
+All operations have well-defined types:
+
+```wasm
+;; Valid: both operands are i32
+(i32.const 5) (i32.const 3) (i32.add) : [i32]
+
+;; Invalid: type mismatch
+(i32.const 5) (f32.const 3.0) (i32.add) ;; ERROR!
+```
+
+### 3. **Memory Safe**
+
+Built-in safety guarantees:
+- **Bounds checking**: All memory accesses validated
+- **Type safety**: Cannot mix incompatible types
+- **Sandboxing**: Isolated from host environment
+- **No undefined behavior**: All operations well-defined
+
+### 4. **Portable**
+
+WebAssembly is:
+- **Platform-independent**: Runs on any architecture
+- **Deterministic**: Same inputs → same outputs
+- **Embeddable**: Works in browsers, servers, IoT
+
+## Architecture
+
+### Value Types
+
+```wasm
+i32 ;; 32-bit integer
+i64 ;; 64-bit integer
+f32 ;; 32-bit float (IEEE 754)
+f64 ;; 64-bit float (IEEE 754)
+```
+
+### Instructions
+
+**Numeric Operations:**
+```wasm
+i32.add, i32.sub, i32.mul, i32.div_s, i32.div_u
+i32.rem_s, i32.rem_u
+i32.and, i32.or, i32.xor, i32.shl, i32.shr_s, i32.shr_u
+i32.eq, i32.ne, i32.lt_s, i32.le_s, i32.gt_s, i32.ge_s
+```
+
+**Control Flow:**
+```wasm
+block, loop, if, br, br_if, br_table
+call, call_indirect, return
+```
+
+**Memory:**
+```wasm
+i32.load, i64.load, f32.load, f64.load
+i32.store, i64.store, f32.store, f64.store
+memory.size, memory.grow
+```
+
+**Variables:**
+```wasm
+local.get, local.set, local.tee
+global.get, global.set
+```
+
+### Module Structure
+
+A WebAssembly module consists of:
+
+```wasm
+(module
+ ;; Type definitions
+ (type $add_type (func (param i32 i32) (result i32)))
+
+ ;; Imports
+ (import "env" "print" (func $print (param i32)))
+
+ ;; Functions
+ (func $add (param $a i32) (param $b i32) (result i32)
+ local.get $a
+ local.get $b
+ i32.add
+ )
+
+ ;; Memory
+ (memory 1) ;; 1 page = 64KB
+
+ ;; Globals
+ (global $counter (mut i32) (i32.const 0))
+
+ ;; Exports
+ (export "add" (func $add))
+ (export "memory" (memory 0))
+
+ ;; Data initialization
+ (data (i32.const 0) "Hello, World!")
+)
+```
+
+## Execution Model
+
+### Stack Machine
+
+Instructions manipulate an operand stack:
+
+```
+Instruction Stack Before Stack After
+─────────────────────────────────────────────
+i32.const 5 [] [5]
+i32.const 3 [5] [5, 3]
+i32.add [5, 3] [8]
+```
+
+### Call Frames
+
+Function calls create **activation frames**:
+
+```
+Frame Stack:
+┌─────────────────┐
+│ Frame 2: $fib │ ← Current
+│ locals: n=2 │
+├─────────────────┤
+│ Frame 1: $fib │
+│ locals: n=3 │
+├─────────────────┤
+│ Frame 0: $main │
+│ locals: x=5 │
+└─────────────────┘
+```
+
+### Linear Memory
+
+Contiguous, resizable memory:
+
+```
+Address Value
+────────────────
+0x0000 01
+0x0001 02
+0x0002 03
+0x0003 04
+...
+```
+
+Properties:
+- **Byte-addressed**: Each address = 1 byte
+- **Little-endian**: Least significant byte first
+- **Growable**: Can expand at runtime
+- **Bounds-checked**: Invalid access → trap
+
+## Type System
+
+### Validation
+
+Programs must be **well-typed** before execution:
+
+```
+Γ ⊢ e : [t1* ] → [t2*]
+```
+
+Meaning: In context Γ, expression e has type [t1*] → [t2*]
+(Takes t1* from stack, produces t2*)
+
+### Type Rules Examples
+
+**Constants:**
+```
+─────────────────────── [T-Const]
+⊢ (t.const c) : [] → [t]
+```
+
+**Binary Operations:**
+```
+─────────────────────── [T-Binop]
+⊢ t.binop : [t t] → [t]
+```
+
+**Control Flow:**
+```
+Γ ⊢ e1 : [t1*] → [t2*] Γ ⊢ e2 : [t1*] → [t2*]
+───────────────────────────────────────────────── [T-If]
+Γ ⊢ (if [t2*] e1 else e2) : [t1* i32] → [t2*]
+```
+
+## Example: Fibonacci
+
+### Source Code (Rust)
+
+```rust
+pub fn fib(n: u32) -> u32 {
+ if n < 2 {
+ n
+ } else {
+ fib(n - 1) + fib(n - 2)
+ }
+}
+```
+
+### Compiled WebAssembly
+
+```wasm
+(func $fib (param $n i32) (result i32)
+ (if (result i32)
+ (i32.lt_u (local.get $n) (i32.const 2))
+ (then
+ (local.get $n))
+ (else
+ (i32.add
+ (call $fib
+ (i32.sub (local.get $n) (i32.const 1)))
+ (call $fib
+ (i32.sub (local.get $n) (i32.const 2)))))))
+```
+
+### Execution Trace
+
+```
+Call $fib with n=3:
+ n < 2? No
+ Call $fib with n=2:
+ n < 2? No
+ Call $fib with n=1:
+ n < 2? Yes
+ Return 1
+ Call $fib with n=0:
+ n < 2? Yes
+ Return 0
+ Return 1 + 0 = 1
+ Call $fib with n=1:
+ n < 2? Yes
+ Return 1
+ Return 1 + 1 = 2
+```
+
+## Use Cases
+
+### 1. **Web Performance**
+- Games (Unity, Unreal Engine)
+- CAD tools (AutoCAD)
+- Video editing (Figma)
+- Scientific computing
+
+### 2. **Server-Side**
+- Serverless functions (Cloudflare Workers)
+- Edge computing
+- Plugin systems (Envoy, Istio)
+
+### 3. **Blockchain**
+- Smart contracts (Ethereum 2.0, Polkadot)
+- Deterministic execution
+- Sandboxed computation
+
+### 4. **IoT & Embedded**
+- Resource-constrained devices
+- Cross-platform code
+- Secure execution
+
+## Comparison to Native Code
+
+| Aspect | WebAssembly | Native (x86/ARM) |
+|--------|-------------|------------------|
+| **Speed** | 95-100% of native | 100% |
+| **Portability** | Runs anywhere | Platform-specific |
+| **Security** | Sandboxed | No isolation |
+| **Size** | Compact bytecode | Larger binaries |
+| **Tooling** | Growing ecosystem | Mature tools |
+
+## Language Support
+
+WebAssembly can be compiled from:
+- **C/C++**: clang, emscripten
+- **Rust**: rustc
+- **Go**: TinyGo
+- **C#**: Blazor
+- **AssemblyScript**: TypeScript-like
+- **Many others**: Python, Ruby, Java, Kotlin...
+
+## Formal Semantics
+
+The [WebAssembly Specification](https://webassembly.github.io/spec/) provides:
+
+1. **Syntax**: How to write programs
+2. **Typing**: Well-formedness rules
+3. **Execution**: Operational semantics
+4. **Validation**: Type-checking algorithm
+5. **Soundness**: Formal guarantees
+
+Example from spec:
+
+```
+Execution of i32.add:
+────────────────────────────────────────
+S; F; (i32.const c1) (i32.const c2) i32.add
+⟼ S; F; (i32.const (c1 + c2) mod 2³²)
+```
+
+## WebAssembly Proposals
+
+Extensions being standardized:
+
+- **SIMD**: Vector operations
+- **Threads**: Shared memory, atomics
+- **Tail Calls**: Optimized recursion
+- **Exception Handling**: try/catch
+- **Garbage Collection**: Managed types
+- **Component Model**: Interface types
+
+## Try It!
+
+### Online Tools
+- [WebAssembly Studio](https://webassembly.studio/)
+- [WasmFiddle](https://wasdk.github.io/WasmFiddle/)
+- [Wasm Explorer](https://mbebenita.github.io/WasmExplorer/)
+
+### Command-Line Tools
+```bash
+# Compile C to Wasm
+emcc hello.c -o hello.wasm
+
+# Run with wasmtime
+wasmtime hello.wasm
+
+# Inspect binary
+wasm-objdump -d hello.wasm
+```
+
+## Resources
+
+### Official
+- [WebAssembly.org](https://webassembly.org/)
+- [Specification](https://webassembly.github.io/spec/)
+- [MDN Web Docs](https://developer.mozilla.org/en-US/docs/WebAssembly)
+
+### Books
+- "Programming WebAssembly with Rust" by Kevin Hoffman
+- "WebAssembly: The Definitive Guide" by Brian Sletten
+
+### Communities
+- [WebAssembly Community Group](https://www.w3.org/community/webassembly/)
+- [Reddit r/WebAssembly](https://www.reddit.com/r/WebAssembly/)
+- [Stack Overflow Tag](https://stackoverflow.com/questions/tagged/webassembly)
+
+## Next Steps
+
+- [Why Verify WebAssembly?](03_why_verify_wasm.md) - Learn about formal verification
+- [Hello WebAssembly Semantics](../02_interactive_tutorials/hello_wasm_semantics/) - First tutorial
+- [Arithmetic Operations](../02_interactive_tutorials/arithmetic_operations/) - Practice with instructions
+
+---
+
+
+
+**[← Previous: K Framework Primer](01_k_framework_primer.md)** | **[Back to Home](../README.md)** | **[Next: Why Verify? →](03_why_verify_wasm.md)**
+
+
diff --git a/demos/formal_semantics_explorer/01_introduction/03_why_verify_wasm.md b/demos/formal_semantics_explorer/01_introduction/03_why_verify_wasm.md
new file mode 100644
index 000000000..152963bde
--- /dev/null
+++ b/demos/formal_semantics_explorer/01_introduction/03_why_verify_wasm.md
@@ -0,0 +1,336 @@
+# Why Verify WebAssembly?
+
+## The Challenge
+
+WebAssembly is deployed in:
+- **4+ billion web browsers** worldwide
+- **Cloud computing** platforms (AWS, Google Cloud, Azure)
+- **Edge networks** (Cloudflare, Fastly)
+- **Blockchain systems** (Ethereum, Polkadot)
+- **IoT devices** and embedded systems
+
+With this scale, even rare bugs can have massive impact.
+
+## Real-World Risks
+
+### 1. Security Vulnerabilities
+
+**Problem**: WebAssembly runs untrusted code in sensitive environments.
+
+**Risks**:
+- **Sandbox escapes**: Break out of isolation
+- **Memory corruption**: Read/write arbitrary memory
+- **Side-channel attacks**: Extract secrets via timing
+- **Resource exhaustion**: DoS through infinite loops
+
+**Example**: Spectre/Meltdown vulnerabilities affect WebAssembly engines.
+
+### 2. Compiler Bugs
+
+**Problem**: Compilers may generate incorrect WebAssembly.
+
+**Consequences**:
+- Silent data corruption
+- Incorrect computation results
+- Security vulnerabilities
+- Unpredictable behavior
+
+**Example**: A Rust compiler bug could miscompile safe code into unsafe WebAssembly.
+
+### 3. Engine Inconsistencies
+
+**Problem**: Different WebAssembly engines may behave differently.
+
+**Issues**:
+- Chrome vs Firefox vs Safari differences
+- Server-side vs browser behavior
+- Version incompatibilities
+
+**Example**: Floating-point operations may produce different results across engines.
+
+### 4. Specification Ambiguities
+
+**Problem**: Natural language specs can be unclear.
+
+**Results**:
+- Implementers make different choices
+- Edge cases undefined
+- Test suites incomplete
+
+**Example**: Early WebAssembly spec had ambiguities in control flow validation.
+
+## Why Formal Verification?
+
+### Traditional Testing is Insufficient
+
+**Testing** checks specific cases:
+```
+test(add(2, 3) == 5) ✓
+test(add(0, 0) == 0) ✓
+test(add(-1, 1) == 0) ✓
+```
+
+But what about:
+- `add(2147483647, 1)`? (overflow)
+- `add(-2147483648, -1)`? (underflow)
+- All 2⁶⁴ combinations?
+
+**Formal verification** proves correctness for **ALL** inputs:
+```
+∀ x, y ∈ i32. add(x, y) = (x + y) mod 2³²
+```
+
+### Mechanized Proofs
+
+Benefits:
+- **Exhaustive**: Cover all cases
+- **Automated**: Tools do the work
+- **Checkable**: Anyone can verify
+- **Compositional**: Build larger proofs
+
+### Executable Specifications
+
+K Framework semantics are:
+- **Formal**: Mathematically precise
+- **Executable**: Can run programs
+- **Verifiable**: Can prove properties
+
+## What Can We Verify?
+
+### 1. Type Safety
+
+**Property**: Well-typed programs don't have type errors.
+
+**Theorem** (Type Soundness):
+```
+If ⊢ e : τ, then either:
+1. e is a value, or
+2. e → e' and ⊢ e' : τ
+```
+
+**Guarantees**:
+- No type confusion attacks
+- Memory accesses are type-correct
+- Function calls match signatures
+
+### 2. Memory Safety
+
+**Property**: All memory accesses are in bounds.
+
+**Theorem** (Bounds Safety):
+```
+∀ address, access.
+ mem_access(address) → trap ∨ valid_access(address)
+```
+
+**Guarantees**:
+- No buffer overflows
+- No out-of-bounds reads/writes
+- Trap on invalid access
+
+### 3. Control Flow Integrity
+
+**Property**: Control flow follows structured patterns.
+
+**Theorem** (Structured Control):
+```
+∀ program. validated(program) →
+ all_branches_valid(program)
+```
+
+**Guarantees**:
+- No arbitrary jumps
+- Balanced stack at branches
+- Proper nesting of blocks
+
+### 4. Determinism
+
+**Property**: Same inputs produce same outputs.
+
+**Theorem** (Deterministic Execution):
+```
+∀ s, e. (s, e) →* (s₁, v₁) ∧ (s, e) →* (s₂, v₂) → s₁ = s₂ ∧ v₁ = v₂
+```
+
+**Guarantees**:
+- Reproducible execution
+- No hidden non-determinism
+- Consensus-safe (for blockchain)
+
+### 5. Compiler Correctness
+
+**Property**: Compiled code preserves source semantics.
+
+**Theorem** (Semantic Preservation):
+```
+∀ source, compiled.
+ compile(source) = compiled →
+ semantics(source) ≃ semantics(compiled)
+```
+
+**Guarantees**:
+- Optimizations are safe
+- Translation is faithful
+- No bugs introduced
+
+## Success Stories
+
+### KWasm (This Project)
+
+**Achievements**:
+- Complete formal semantics of WebAssembly
+- Executable interpreter from semantics
+- Verification of safety properties
+- Conformance testing tool
+
+**Impact**:
+- Found spec ambiguities
+- Verified optimizations
+- Educational resource
+
+### WasmCert
+
+Coq-based verification of:
+- Type checker correctness
+- Interpreter soundness
+- WebAssembly soundness theorem
+
+### Wasmtime Verification
+
+Cranelift compiler verification:
+- Instruction selection correctness
+- Register allocation soundness
+- Code generation safety
+
+## Case Study: Buffer Overflow
+
+### Vulnerable Code
+
+```wasm
+(memory 1) ;; 64KB
+
+(func $unsafe_write (param $offset i32) (param $value i32)
+ local.get $offset
+ local.get $value
+ i32.store ;; What if $offset >= 65536?
+)
+```
+
+### Traditional Approach
+
+```rust
+// Manual bounds check
+fn safe_write(offset: usize, value: i32, mem: &mut [u8]) {
+ if offset + 4 <= mem.len() {
+ mem[offset..offset+4].copy_from_slice(&value.to_le_bytes());
+ } else {
+ panic!("Out of bounds");
+ }
+}
+```
+
+Problem: Easy to forget, easy to get wrong.
+
+### Formal Verification
+
+**Specification**:
+```k
+claim
+
+**[← Previous: WebAssembly Overview](02_webassembly_overview.md)** | **[Back to Home](../README.md)** | **[Next: Start Tutorials →](../02_interactive_tutorials/)**
+
+
diff --git a/demos/formal_semantics_explorer/02_interactive_tutorials/README.md b/demos/formal_semantics_explorer/02_interactive_tutorials/README.md
new file mode 100644
index 000000000..be12e0e2f
--- /dev/null
+++ b/demos/formal_semantics_explorer/02_interactive_tutorials/README.md
@@ -0,0 +1,195 @@
+# Interactive Tutorials
+
+Welcome to the hands-on tutorials! Learn WebAssembly formal semantics through interactive examples and step-by-step guides.
+
+## 📚 Tutorial Structure
+
+Each tutorial includes:
+- **Conceptual explanation** of the topic
+- **WebAssembly examples** (.wat files)
+- **K Framework rules** defining semantics
+- **Interactive visualizers** to see execution
+- **Exercises** to test understanding
+
+## 🎓 Learning Path
+
+### Beginner Tutorials
+
+1. **[Hello WebAssembly Semantics](hello_wasm_semantics/)** ⭐
+ *20 minutes*
+ Your first formal semantics! Learn how `i32.const` works.
+
+2. **[Arithmetic Operations](arithmetic_operations/)** ⭐⭐
+ *45 minutes*
+ Add, subtract, multiply, divide with overflow handling.
+
+3. **[Control Flow](control_flow/)** ⭐⭐
+ *1 hour*
+ Conditionals, loops, and branching instructions.
+
+### Intermediate Tutorials
+
+4. **[Function Calls](function_calls/)** ⭐⭐⭐
+ *1.5 hours*
+ Function invocation, stack frames, and recursion.
+
+5. **[Memory Operations](memory_operations/)** ⭐⭐⭐
+ *2 hours*
+ Load, store, and memory safety verification.
+
+6. **[Tables and References](tables_and_references/)** ⭐⭐⭐
+ *2 hours*
+ Indirect calls and reference types.
+
+## 🛠️ What You'll Build
+
+By completing these tutorials, you'll:
+- ✅ Understand WebAssembly execution model
+- ✅ Read and write K Framework semantics
+- ✅ Trace program execution step-by-step
+- ✅ Verify safety properties
+- ✅ Debug WebAssembly programs
+
+## 🚀 Quick Start
+
+### Option 1: Interactive Web Interface
+
+Simply open any tutorial directory and click on the HTML files:
+```bash
+cd hello_wasm_semantics
+open tutorial.md # Read the guide
+open semantics_trace.html # Watch execution
+```
+
+### Option 2: Command Line
+
+Run examples using the K Framework:
+```bash
+# From repository root
+./kwasm run demos/formal_semantics_explorer/assets/wasm_examples/basic/hello.wat
+
+# With visualization
+./kwasm run --output pretty hello.wat
+```
+
+## 📖 Tutorial Format
+
+Each tutorial follows this structure:
+
+```
+tutorial_name/
+├── tutorial.md # Main guide
+├── example.wat # WebAssembly code
+├── semantics_trace.html # Interactive execution viewer
+├── interactive_stepper.html # Step-by-step debugger
+└── exercises.md # Practice problems
+```
+
+## 💡 Learning Tips
+
+1. **Read First**: Understand concepts before running code
+2. **Experiment**: Modify examples to see what happens
+3. **Step Through**: Use interactive stepper to understand execution
+4. **Do Exercises**: Practice solidifies learning
+5. **Ask Questions**: Open issues or discussions on GitHub
+
+## 🎯 Prerequisites
+
+**Required Knowledge:**
+- Basic programming concepts
+- Understanding of stack data structure
+- Willingness to learn!
+
+**Optional (Helpful):**
+- Assembly language experience
+- Compiler knowledge
+- Formal methods background
+
+**No prior K Framework experience needed!**
+
+## 🔗 Related Resources
+
+- [Introduction Section](../01_introduction/) - Background on formal semantics
+- [Visualization Gallery](../03_visualization_gallery/) - See more examples
+- [K Framework Deep Dive](../05_k_framework_deep_dive/) - Advanced K topics
+- [Interactive Playground](../06_interactive_playground/) - Experiment freely
+
+## 📊 Tutorial Difficulty Guide
+
+- ⭐ **Beginner**: Basic concepts, simple examples
+- ⭐⭐ **Intermediate**: Multiple concepts, longer examples
+- ⭐⭐⭐ **Advanced**: Complex interactions, verification
+- ⭐⭐⭐⭐ **Expert**: Full case studies, proofs
+- ⭐⭐⭐⭐⭐ **Research**: Cutting-edge topics
+
+## 🏆 Completion Checklist
+
+Track your progress:
+
+- [ ] Completed Hello WebAssembly Semantics
+- [ ] Completed Arithmetic Operations
+- [ ] Completed Control Flow
+- [ ] Completed Function Calls
+- [ ] Completed Memory Operations
+- [ ] Completed Tables and References
+- [ ] All exercises solved
+- [ ] Built custom example
+- [ ] Verified a property
+
+## 🎮 Interactive Features
+
+### Execution Visualizer
+Watch programs execute with:
+- Animated stack operations
+- Memory state display
+- Step-by-step controls
+- Speed adjustment
+
+### Semantic Rule Browser
+Explore K rules:
+- Search by instruction
+- Filter by category
+- View rule application
+- See side conditions
+
+### Configuration Inspector
+Examine execution state:
+- Current instruction
+- Stack contents
+- Memory layout
+- Local/global variables
+
+## 🐛 Troubleshooting
+
+**Issue**: Interactive HTML files don't work
+**Solution**: Serve via HTTP: `make serve` or `python3 -m http.server`
+
+**Issue**: Can't find K Framework
+**Solution**: Follow [build instructions](../10_community_resources/build_instructions.md)
+
+**Issue**: Examples don't run
+**Solution**: Check you're in the correct directory and K is installed
+
+## 💬 Get Help
+
+- **GitHub Issues**: Report bugs or unclear documentation
+- **Discussions**: Ask questions, share ideas
+- **Slack**: Real-time help in K Framework Slack
+
+## 🌟 What's Next?
+
+After completing tutorials:
+1. Try [Verification Case Studies](../04_verification_case_studies/)
+2. Explore [Advanced Topics](../08_advanced_topics/)
+3. Build your own semantics
+4. Contribute back!
+
+---
+
+
+
+**[← Back to Home](../README.md)** | **[Start Learning →](hello_wasm_semantics/)**
+
+*Happy Learning! 🔬📚*
+
+
diff --git a/demos/formal_semantics_explorer/02_interactive_tutorials/hello_wasm_semantics/tutorial.md b/demos/formal_semantics_explorer/02_interactive_tutorials/hello_wasm_semantics/tutorial.md
new file mode 100644
index 000000000..b5ba9a751
--- /dev/null
+++ b/demos/formal_semantics_explorer/02_interactive_tutorials/hello_wasm_semantics/tutorial.md
@@ -0,0 +1,234 @@
+# Hello WebAssembly Semantics
+
+## Welcome!
+
+This is your first step into the world of formal WebAssembly semantics. In this tutorial, you'll:
+
+1. See a simple WebAssembly program
+2. Understand its formal semantics
+3. Watch it execute step-by-step
+4. Explore the K Framework rules that define its behavior
+
+## The Simplest Program
+
+Let's start with the most basic WebAssembly program:
+
+```wasm
+(i32.const 42)
+```
+
+That's it! This program:
+- Pushes the integer constant `42` onto the stack
+- Has type `[] → [i32]` (takes nothing, produces an i32)
+
+## Informal Understanding
+
+When this program runs:
+1. **Before**: Stack is empty `[]`
+2. **Execute**: Push 42 onto stack
+3. **After**: Stack contains `[42]`
+
+Simple, right? But how do we know this is **exactly** what happens?
+
+## Formal Semantics
+
+The K Framework defines this behavior precisely:
+
+```k
+rule
+
+
+
+
+
+
+## Try It Yourself
+
+Modify the constant and see what happens:
+
+```wasm
+;; Try different values:
+(i32.const 0) ;; Zero
+(i32.const -1) ;; Negative (wraps to 4294967295)
+(i32.const 100) ;; Positive
+```
+
+Each follows the same semantic rule, just with different values for `I`.
+
+## What About Other Types?
+
+The same rule works for other numeric types:
+
+```wasm
+(i64.const 9223372036854775807) ;; 64-bit integer
+(f32.const 3.14) ;; 32-bit float
+(f64.const 2.71828) ;; 64-bit float
+```
+
+Each has a similar K rule:
+
+```k
+rule
+
+
+
+
+
+
+
+## Questions?
+
+- **Q: Why is the formal semantics necessary?**
+ A: It removes ambiguity and enables automated verification.
+
+- **Q: Can I run this program?**
+ A: Yes! Use `kwasm run` or any WebAssembly engine.
+
+- **Q: What if I use an invalid constant?**
+ A: WebAssembly has range limits. i32 must fit in 32 bits (signed).
+
+## Further Reading
+
+- [K Framework Primer](../../01_introduction/01_k_framework_primer.md)
+- [WebAssembly Specification](https://webassembly.github.io/spec/)
+- [KWasm Source Code](https://github.com/runtimeverification/wasm-semantics)
+
+---
+
+Click to reveal answer
+ +**Answer**: Stack contains `[10, 20, 30]` (30 on top) + +Each instruction pushes its value, so we apply the rule three times: +1. Push 10: `[10]` +2. Push 20: `[10, 20]` +3. Push 30: `[10, 20, 30]` + +
+
+**[← Back to Tutorials](../../README.md#tutorials)** | **[Next: Arithmetic Operations →](../arithmetic_operations/)**
+
+
diff --git a/demos/formal_semantics_explorer/03_visualization_gallery/README.md b/demos/formal_semantics_explorer/03_visualization_gallery/README.md
new file mode 100644
index 000000000..89b2dee79
--- /dev/null
+++ b/demos/formal_semantics_explorer/03_visualization_gallery/README.md
@@ -0,0 +1,284 @@
+# Visualization Gallery
+
+Explore formal WebAssembly semantics through beautiful, interactive visualizations.
+
+## 🎨 Gallery Sections
+
+### 1. [Execution Traces](execution_traces/)
+Watch WebAssembly programs execute step-by-step with animated visualizations.
+
+**Features:**
+- Instruction-by-instruction animation
+- Stack operation visualization
+- Memory state tracking
+- Timeline scrubbing
+- Speed control
+
+**Examples:**
+- Fibonacci sequence computation
+- Factorial calculation
+- Array sorting
+- Tree traversal
+
+### 2. [Semantic Rules](semantic_rules/)
+Browse and understand K Framework rules that define WebAssembly semantics.
+
+**Features:**
+- Searchable rule database
+- Category filtering
+- Syntax highlighting
+- Rule dependencies graph
+- Interactive examples
+
+**Categories:**
+- Arithmetic operations
+- Control flow
+- Memory operations
+- Function calls
+- Table operations
+
+### 3. [Proof Trees](proof_trees/)
+Explore formal verification proofs as interactive tree structures.
+
+**Features:**
+- Collapsible/expandable nodes
+- Rule application highlighting
+- LaTeX export
+- GraphViz export
+- Search functionality
+
+**Proofs:**
+- Type soundness
+- Memory safety
+- Determinism
+- Progress theorem
+- Preservation theorem
+
+### 4. [Memory Models](memory_models/)
+Visualize WebAssembly memory in 2D and 3D.
+
+**Features:**
+- Hex dump viewer
+- 3D memory explorer
+- Stack visualization
+- Growth animation
+- Type coloring
+
+**Views:**
+- Linear memory layout
+- Stack frame structure
+- Heap organization
+- Global variables
+- Table contents
+
+### 5. [Type System](type_system/)
+See how WebAssembly's type system ensures safety.
+
+**Features:**
+- Type checking visualization
+- Validation flow diagrams
+- Type error explanation
+- Stack polymorphism demo
+- Type inference
+
+**Visualizations:**
+- Module validation
+- Function type checking
+- Instruction typing
+- Block types
+- Control flow types
+
+## 🚀 Using the Gallery
+
+### Interactive Mode
+
+Open visualizations in your browser:
+```bash
+cd demos/formal_semantics_explorer
+make serve
+# Navigate to http://localhost:8000/03_visualization_gallery/
+```
+
+### Generating Custom Visualizations
+
+```bash
+# Generate execution trace
+make example EXAMPLE=fibonacci
+
+# Export proof tree
+make proof-tree EXAMPLE=type_soundness
+
+# Create memory diagram
+make memory-viz EXAMPLE=array_access
+```
+
+## 📊 Visualization Types
+
+### Static Diagrams
+- SVG graphics
+- Architecture diagrams
+- State machine diagrams
+- Type derivation trees
+
+### Interactive Visualizations
+- D3.js animations
+- Canvas-based renderers
+- WebGL 3D views
+- Interactive controls
+
+### Animated Sequences
+- Frame-by-frame execution
+- Transition animations
+- State evolution
+- Proof construction
+
+## 🎯 Learning Objectives
+
+Through visualizations, you'll understand:
+- How WebAssembly executes
+- What K rules mean
+- How proofs are constructed
+- Why properties hold
+- Where bugs can occur
+
+## 🛠️ Technical Details
+
+### Technologies Used
+- **D3.js**: Tree and graph visualizations
+- **Three.js**: 3D memory viewer
+- **Canvas API**: Execution traces
+- **Prism.js**: Code highlighting
+- **MathJax**: Mathematical notation
+
+### Browser Requirements
+- Modern browser (Chrome, Firefox, Safari, Edge)
+- JavaScript enabled
+- Canvas support
+- WebGL (for 3D features)
+
+## 📖 Featured Visualizations
+
+### Execution Trace: Fibonacci
+
+
+Watch recursive Fibonacci compute `fib(5)` with:
+- Call stack evolution
+- Stack operations
+- Return value propagation
+
+### Proof Tree: Type Soundness
+
+
+Explore the proof that well-typed programs don't get stuck.
+
+### Memory Layout: Array Operations
+
+
+See how arrays are stored and accessed in linear memory.
+
+### Rule Browser: i32.add
+
+
+Understand how addition works in the K semantics.
+
+## 🔍 Navigation
+
+Each visualization includes:
+- **Controls**: Play, pause, step, reset
+- **Info panel**: Current state description
+- **Settings**: Speed, color scheme, detail level
+- **Export**: Save as image, JSON, or SVG
+
+## 💡 Tips for Learning
+
+1. **Start Simple**: Begin with basic arithmetic
+2. **Compare**: Run similar examples side-by-side
+3. **Slow Down**: Use slow animation to understand
+4. **Experiment**: Modify examples to see effects
+5. **Export**: Save interesting states for later
+
+## 🎓 Educational Uses
+
+### For Students
+- Understand formal semantics concretely
+- Debug WebAssembly programs
+- Prepare for exams
+
+### For Teachers
+- Demonstrate concepts visually
+- Create engaging lectures
+- Assign as homework
+
+### For Researchers
+- Explore semantic edge cases
+- Validate theories
+- Generate figures for papers
+
+## 🌟 Advanced Features
+
+### Custom Examples
+Upload your own WebAssembly:
+```javascript
+// In browser console
+visualizer.loadWasm(wasmBytes);
+visualizer.run();
+```
+
+### Comparison Mode
+View multiple executions simultaneously:
+- Before/after optimization
+- Different implementations
+- Correct vs buggy code
+
+### Recording
+Capture visualizations as videos:
+- GIF export
+- MP4 recording
+- Frame-by-frame PNGs
+
+## 🐛 Troubleshooting
+
+**Visualization doesn't load:**
+- Check browser console for errors
+- Ensure JavaScript enabled
+- Try different browser
+
+**Performance issues:**
+- Reduce animation speed
+- Close other tabs
+- Disable 3D features if needed
+
+**Export fails:**
+- Check browser download settings
+- Try different export format
+- Use "Save As" from browser
+
+## 📚 Related Resources
+
+- [Interactive Tutorials](../02_interactive_tutorials/) - Learn by doing
+- [Case Studies](../04_verification_case_studies/) - Real-world examples
+- [K Framework Deep Dive](../05_k_framework_deep_dive/) - Understanding rules
+
+## 🤝 Contributing
+
+Want to add visualizations?
+1. See [contribution guide](../10_community_resources/contribution_guide.md)
+2. Use existing visualizers as templates
+3. Submit PR with screenshots
+
+## 🎬 Video Tours
+
+Check out video walkthroughs:
+- [Gallery Overview](https://example.com) (5 min)
+- [Execution Traces Deep Dive](https://example.com) (15 min)
+- [Proof Tree Tutorial](https://example.com) (10 min)
+
+---
+
+
+
+**[← Back to Home](../README.md)** | **[Explore Visualizations →](execution_traces/)**
+
+*Seeing is believing! 👁️✨*
+
+
diff --git a/demos/formal_semantics_explorer/10_community_resources/build_instructions.md b/demos/formal_semantics_explorer/10_community_resources/build_instructions.md
new file mode 100644
index 000000000..d10b32132
--- /dev/null
+++ b/demos/formal_semantics_explorer/10_community_resources/build_instructions.md
@@ -0,0 +1,341 @@
+# Build Instructions
+
+## Quick Start (Docker)
+
+The easiest way to get started is using Docker:
+
+```bash
+# Pull the image
+docker pull ghcr.io/ayushmit/wasm-semantics:latest
+
+# Run the demo
+docker run -p 8000:8000 ghcr.io/ayushmit/wasm-semantics:latest
+
+# Open browser to http://localhost:8000/demos/formal_semantics_explorer
+```
+
+## Local Installation
+
+### Prerequisites
+
+#### Required
+- **K Framework 5.0+**: [Installation guide](http://www.kframework.org/)
+- **Python 3.8+**: For web server
+- **Git**: For cloning repository
+
+#### Optional
+- **Node.js 16+**: For JavaScript linting
+- **Pandoc 2.0+**: For generating documentation
+- **Z3 4.8.15**: For symbolic execution
+
+### Step 1: Install K Framework
+
+**Using Kup (recommended):**
+```bash
+bash <(curl https://kframework.org/install)
+kup install k
+kup list
+```
+
+**From source:**
+```bash
+git clone https://github.com/kframework/k.git
+cd k
+mvn package -DskipTests
+export PATH=$PATH:$(pwd)/k-distribution/target/release/k/bin
+```
+
+**Verify installation:**
+```bash
+kompile --version
+# Should show: K version 5.x.x
+```
+
+### Step 2: Clone Repository
+
+```bash
+git clone https://github.com/AYUSHMIT/wasm-semantics.git
+cd wasm-semantics
+```
+
+### Step 3: Build K Semantics
+
+```bash
+# Build all backends
+make build
+
+# Or build specific backend
+make build-llvm # Concrete execution
+make build-haskell # Symbolic execution
+```
+
+This will:
+- Parse K definition files
+- Generate interpreters
+- Create verification tools
+
+**Expected output:**
+```
+Kompiling WASM...
+[Info] Compiling definition...
+[Info] Backend: llvm
+[Success] Compilation complete
+```
+
+### Step 4: Install Dependencies
+
+For the demo specifically:
+
+```bash
+cd demos/formal_semantics_explorer
+make install-deps
+```
+
+This checks for:
+- K Framework
+- Python 3
+- Optional tools
+
+### Step 5: Test Installation
+
+```bash
+# Run a simple test
+cd ../../
+./kwasm run tests/simple/arithmetic.wast
+
+# Run demo server
+cd demos/formal_semantics_explorer
+make serve
+```
+
+Open http://localhost:8000 in your browser.
+
+## Platform-Specific Instructions
+
+### Ubuntu/Debian
+
+```bash
+# Install system dependencies
+sudo apt-get update
+sudo apt-get install -y \
+ build-essential \
+ cmake \
+ clang llvm \
+ maven openjdk-11-jdk \
+ python3 python3-pip \
+ git curl \
+ libgmp-dev libmpfr-dev \
+ flex bison \
+ z3
+
+# Install K Framework
+bash <(curl https://kframework.org/install)
+kup install k
+
+# Clone and build
+git clone https://github.com/AYUSHMIT/wasm-semantics.git
+cd wasm-semantics
+make build
+```
+
+### macOS
+
+```bash
+# Install Homebrew if needed
+/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
+
+# Install dependencies
+brew install \
+ maven openjdk@11 \
+ python3 \
+ git curl \
+ gmp mpfr \
+ flex bison \
+ z3
+
+# Install K Framework
+bash <(curl https://kframework.org/install)
+kup install k
+
+# Clone and build
+git clone https://github.com/AYUSHMIT/wasm-semantics.git
+cd wasm-semantics
+make build
+```
+
+### Windows (WSL2)
+
+Use Windows Subsystem for Linux:
+
+```bash
+# In PowerShell (as Administrator)
+wsl --install
+
+# After reboot, in WSL Ubuntu:
+sudo apt-get update
+sudo apt-get install -y build-essential git curl
+
+# Follow Ubuntu instructions above
+```
+
+## Troubleshooting
+
+### "kompile: command not found"
+
+K Framework not in PATH. Add to `~/.bashrc`:
+
+```bash
+export PATH=$PATH:$HOME/.kup/bin
+source ~/.bashrc
+```
+
+### "Z3 version mismatch"
+
+Install specific Z3 version:
+
+```bash
+wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.15/z3-4.8.15-x64-ubuntu-18.04.zip
+unzip z3-4.8.15-x64-ubuntu-18.04.zip
+sudo cp z3-4.8.15-x64-ubuntu-18.04/bin/z3 /usr/local/bin/
+z3 --version # Should show 4.8.15
+```
+
+### "Out of memory during kompile"
+
+Increase Java heap size:
+
+```bash
+export K_OPTS="-Xmx8G -Xss512m"
+make build
+```
+
+### Port 8000 already in use
+
+Use different port:
+
+```bash
+make serve PORT=8080
+```
+
+## Building Documentation
+
+Generate HTML docs from Markdown:
+
+```bash
+# Install Pandoc
+sudo apt-get install pandoc
+
+# Generate docs
+make docs
+```
+
+## Running Tests
+
+```bash
+# Full test suite
+make test
+
+# Specific tests
+make test-simple # Simple execution tests
+make test-conformance # WebAssembly spec conformance
+make test-prove # Verification tests
+```
+
+## Development Setup
+
+### JavaScript Linting
+
+```bash
+npm install -g eslint
+cd demos/formal_semantics_explorer
+make lint
+```
+
+### CSS Linting
+
+```bash
+npm install -g stylelint stylelint-config-standard
+make lint
+```
+
+### Live Reload
+
+```bash
+# Install entr
+sudo apt-get install entr
+
+# Auto-reload on changes
+make watch
+```
+
+## Performance Optimization
+
+### Kompile Options
+
+```bash
+# Faster compilation (less optimization)
+KOMPILE_OPTS="--enable-llvm-debug" make build-llvm
+
+# More optimization (slower compile, faster run)
+KOMPILE_OPTS="-O3" make build-llvm
+```
+
+### Parallel Build
+
+```bash
+# Use multiple cores
+make -j4 build
+```
+
+## Verification Setup
+
+For running proofs:
+
+```bash
+# Install Haskell Stack
+curl -sSL https://get.haskellstack.org/ | sh
+
+# Build Haskell backend
+make build-haskell
+
+# Run verification
+./kwasm prove tests/proofs/simple-arithmetic-spec.k kwasm-lemmas
+```
+
+## Docker Build
+
+Build your own Docker image:
+
+```bash
+docker build -t wasm-semantics .
+docker run -p 8000:8000 wasm-semantics
+```
+
+## Continuous Integration
+
+GitHub Actions workflow (`.github/workflows/test-pr.yml`):
+
+```yaml
+- name: Install K
+ run: bash <(curl https://kframework.org/install)
+
+- name: Build
+ run: make build
+
+- name: Test
+ run: make test
+```
+
+## Next Steps
+
+- [Troubleshooting Guide](troubleshooting.md) - Common issues
+- [Testing Framework](testing_framework.md) - Writing tests
+- [Contribution Guide](contribution_guide.md) - How to contribute
+
+---
+
+
+
+**[Back to Home](../README.md)** | **[Get Help](troubleshooting.md)**
+
+
diff --git a/demos/formal_semantics_explorer/10_community_resources/contribution_guide.md b/demos/formal_semantics_explorer/10_community_resources/contribution_guide.md
new file mode 100644
index 000000000..98b8fe34a
--- /dev/null
+++ b/demos/formal_semantics_explorer/10_community_resources/contribution_guide.md
@@ -0,0 +1,272 @@
+# Contributing to WebAssembly Formal Semantics Explorer
+
+Thank you for your interest in contributing to the WebAssembly Formal Semantics Explorer! This guide will help you get started.
+
+## Ways to Contribute
+
+### 1. Add New Tutorials
+- Create step-by-step guides for WebAssembly features
+- Include executable examples and visualizations
+- Follow existing tutorial structure in `02_interactive_tutorials/`
+
+### 2. Improve Visualizations
+- Enhance existing JavaScript visualizers
+- Create new visualization types (3D memory, proof trees, etc.)
+- Optimize rendering performance
+
+### 3. Add Verification Case Studies
+- Prove new properties about WebAssembly
+- Document real-world security issues
+- Create interactive proof explorers
+
+### 4. Extend K Semantics
+- Cover additional WebAssembly proposals (SIMD, threads, GC)
+- Add new semantic rules
+- Improve existing rule documentation
+
+### 5. Fix Bugs
+- Report issues on GitHub
+- Submit fixes with test cases
+- Improve error messages
+
+### 6. Documentation
+- Fix typos and clarity issues
+- Add more examples
+- Translate to other languages
+
+## Getting Started
+
+### Prerequisites
+
+```bash
+# Required
+- K Framework 5.0+
+- Python 3.8+
+- Git
+
+# Optional (for development)
+- Node.js (for linting)
+- Pandoc (for documentation)
+```
+
+### Setup Development Environment
+
+```bash
+# 1. Fork the repository on GitHub
+
+# 2. Clone your fork
+git clone https://github.com/YOUR-USERNAME/wasm-semantics.git
+cd wasm-semantics
+
+# 3. Add upstream remote
+git remote add upstream https://github.com/runtimeverification/wasm-semantics.git
+
+# 4. Create a branch
+git checkout -b feature/my-contribution
+
+# 5. Make changes
+
+# 6. Test your changes
+cd demos/formal_semantics_explorer
+make test
+make serve # Test in browser
+```
+
+## Contribution Guidelines
+
+### Code Style
+
+**JavaScript:**
+- Use ES6+ features
+- Add JSDoc comments for functions
+- Follow existing naming conventions
+- Run linter: `make lint`
+
+**CSS:**
+- Use CSS variables for theming
+- Mobile-first responsive design
+- Follow BEM naming convention
+
+**Markdown:**
+- Use headers hierarchically
+- Include code examples with syntax highlighting
+- Add navigation links at bottom
+
+**K Framework:**
+- Follow [K Style Guide](https://github.com/kframework/k/wiki/Style-Guide)
+- Document complex rules with comments
+- Include test cases for new rules
+
+### Commit Messages
+
+Use conventional commit format:
+
+```
+type(scope): subject
+
+body
+
+footer
+```
+
+**Types:**
+- `feat`: New feature
+- `fix`: Bug fix
+- `docs`: Documentation only
+- `style`: Code style (formatting, etc.)
+- `refactor`: Code refactoring
+- `test`: Adding tests
+- `chore`: Maintenance tasks
+
+**Examples:**
+```
+feat(tutorial): add memory operations tutorial
+
+Add comprehensive tutorial covering:
+- Load/store instructions
+- Bounds checking
+- Memory safety verification
+
+Closes #123
+
+fix(visualizer): correct stack rendering for f64 values
+
+Stack visualizer was displaying f64 values incorrectly.
+Fixed precision and added proper type coloring.
+
+docs(readme): update installation instructions
+
+Added Docker installation option and troubleshooting section.
+```
+
+### Pull Request Process
+
+1. **Update documentation** if you changed APIs
+2. **Add tests** for new functionality
+3. **Run existing tests**: `make test`
+4. **Update README.md** if needed
+5. **Submit PR** with clear description
+
+**PR Title Format:**
+```
+[Type] Brief description
+
+Example:
+[Feature] Add SIMD instruction tutorial
+[Fix] Correct proof tree rendering bug
+[Docs] Improve K Framework primer
+```
+
+**PR Description:**
+- What does this PR do?
+- Why is it needed?
+- How to test?
+- Screenshots (if UI changes)
+- Related issues
+
+### Code Review
+
+Expect feedback on:
+- Code quality and style
+- Test coverage
+- Documentation completeness
+- Performance implications
+- Compatibility with existing code
+
+## Project Structure
+
+```
+demos/formal_semantics_explorer/
+├── README.md # Main documentation
+├── index.html # Landing page
+├── Makefile # Build system
+├── assets/ # Static assets
+│ ├── styles/ # CSS files
+│ ├── js/ # JavaScript modules
+│ ├── images/ # Images and SVGs
+│ └── wasm_examples/ # Example .wat files
+├── 01_introduction/ # Getting started docs
+├── 02_interactive_tutorials/ # Step-by-step tutorials
+├── 03_visualization_gallery/ # Visual demos
+├── 04_verification_case_studies/ # Formal proofs
+├── 05_k_framework_deep_dive/ # K Framework docs
+├── 06_interactive_playground/ # Online editor
+├── 07_educational_narratives/ # Story-driven learning
+├── 08_advanced_topics/ # Advanced features
+├── 09_comparison_studies/ # Tool comparisons
+└── 10_community_resources/ # This file!
+```
+
+## Testing
+
+### Manual Testing
+```bash
+make serve
+# Open browser and test interactively
+```
+
+### Automated Testing
+```bash
+make test # Run all tests
+make lint # Check code style
+make verify-example # Run verification
+```
+
+### Test Checklist
+- [ ] All links work
+- [ ] JavaScript has no errors (check console)
+- [ ] Responsive design works on mobile
+- [ ] Examples execute correctly
+- [ ] Documentation is accurate
+
+## Reporting Issues
+
+### Bug Reports
+
+Include:
+1. **Title**: Brief, descriptive summary
+2. **Description**: What happened vs. what you expected
+3. **Steps to reproduce**
+4. **Environment**: Browser, OS, K Framework version
+5. **Screenshots** if applicable
+
+### Feature Requests
+
+Include:
+1. **Use case**: Why is this needed?
+2. **Proposed solution**: How should it work?
+3. **Alternatives**: What else have you considered?
+4. **Examples**: Similar features elsewhere?
+
+## Community
+
+- **GitHub Issues**: Bug reports and feature requests
+- **Discussions**: General questions and ideas
+- **K Framework Slack**: Real-time chat
+- **Runtime Verification**: Professional support
+
+## Recognition
+
+Contributors are recognized in:
+- README.md acknowledgments
+- Git history
+- Release notes
+
+Significant contributors may be invited to become maintainers.
+
+## License
+
+By contributing, you agree that your contributions will be licensed under the UIUC License, same as the main project.
+
+## Questions?
+
+If you have questions about contributing:
+- Open a GitHub Discussion
+- Ask in K Framework Slack
+- Email: contact@runtimeverification.com
+
+Thank you for contributing to formal methods education! 🔬
+
+---
+
+**Last Updated**: 2025-01-26
diff --git a/demos/formal_semantics_explorer/Makefile b/demos/formal_semantics_explorer/Makefile
new file mode 100644
index 000000000..7ee0d130f
--- /dev/null
+++ b/demos/formal_semantics_explorer/Makefile
@@ -0,0 +1,190 @@
+# Makefile for WebAssembly Formal Semantics Explorer Demo
+
+.PHONY: all install-deps serve build clean test verify-example help
+
+# Configuration
+PORT ?= 8000
+PYTHON ?= python3
+BROWSER ?= xdg-open
+
+# Colors for output
+BLUE := \033[0;34m
+GREEN := \033[0;32m
+RED := \033[0;31m
+NC := \033[0m # No Color
+
+all: help
+
+## help: Display this help message
+help:
+ @echo "$(BLUE)WebAssembly Formal Semantics Explorer - Make Targets$(NC)"
+ @echo ""
+ @echo "$(GREEN)Setup:$(NC)"
+ @echo " install-deps - Install required dependencies (K Framework, etc.)"
+ @echo " build - Build/compile necessary components"
+ @echo ""
+ @echo "$(GREEN)Running:$(NC)"
+ @echo " serve - Start local web server and open browser"
+ @echo " serve-bg - Start server in background"
+ @echo " stop - Stop background server"
+ @echo ""
+ @echo "$(GREEN)Examples:$(NC)"
+ @echo " examples - Generate example execution traces"
+ @echo " verify-example - Run verification on example (set EXAMPLE=path)"
+ @echo ""
+ @echo "$(GREEN)Development:$(NC)"
+ @echo " test - Run test suite"
+ @echo " lint - Lint JavaScript and CSS"
+ @echo " clean - Remove generated files"
+ @echo ""
+ @echo "$(GREEN)Gallery:$(NC)"
+ @echo " gallery - Generate all gallery visualizations"
+ @echo " screenshots - Take screenshots of interactive demos"
+ @echo ""
+
+## install-deps: Install K Framework and other dependencies
+install-deps:
+ @echo "$(BLUE)Installing dependencies...$(NC)"
+ @if ! command -v kompile &> /dev/null; then \
+ echo "$(RED)K Framework not found. Please install from: http://www.kframework.org/$(NC)"; \
+ echo "Or use: git submodule update --init --recursive && make -C deps/k"; \
+ else \
+ echo "$(GREEN)K Framework already installed$(NC)"; \
+ fi
+ @echo "$(GREEN)Dependencies check complete$(NC)"
+
+## build: Build K definitions and generate tools
+build:
+ @echo "$(BLUE)Building K definitions...$(NC)"
+ @if command -v kompile &> /dev/null; then \
+ echo "Note: Using main repository K definitions"; \
+ echo "To build fresh: cd ../../ && make build"; \
+ else \
+ echo "$(RED)K Framework not installed. Run 'make install-deps' first$(NC)"; \
+ fi
+
+## serve: Start local HTTP server and open browser
+serve:
+ @echo "$(BLUE)Starting web server on port $(PORT)...$(NC)"
+ @echo "$(GREEN)Open http://localhost:$(PORT) in your browser$(NC)"
+ @echo "Press Ctrl+C to stop"
+ @$(PYTHON) -m http.server $(PORT) || python -m SimpleHTTPServer $(PORT)
+
+## serve-bg: Start server in background
+serve-bg:
+ @echo "$(BLUE)Starting web server in background on port $(PORT)...$(NC)"
+ @$(PYTHON) -m http.server $(PORT) > /tmp/wasm-demo-server.log 2>&1 & echo $$! > /tmp/wasm-demo-server.pid
+ @sleep 2
+ @echo "$(GREEN)Server running at http://localhost:$(PORT)$(NC)"
+ @echo "PID: $$(cat /tmp/wasm-demo-server.pid)"
+ @echo "Logs: /tmp/wasm-demo-server.log"
+ @if command -v $(BROWSER) &> /dev/null; then \
+ $(BROWSER) http://localhost:$(PORT); \
+ fi
+
+## stop: Stop background server
+stop:
+ @if [ -f /tmp/wasm-demo-server.pid ]; then \
+ echo "$(BLUE)Stopping server...$(NC)"; \
+ kill $$(cat /tmp/wasm-demo-server.pid) 2>/dev/null || true; \
+ rm /tmp/wasm-demo-server.pid; \
+ echo "$(GREEN)Server stopped$(NC)"; \
+ else \
+ echo "$(RED)No server running$(NC)"; \
+ fi
+
+## examples: Generate example execution traces
+examples:
+ @echo "$(BLUE)Generating example traces...$(NC)"
+ @mkdir -p outputs/execution_traces
+ @mkdir -p outputs/proof_trees
+ @mkdir -p outputs/memory_diagrams
+ @echo "$(GREEN)Examples generated in outputs/$(NC)"
+
+## verify-example: Run verification on specific example
+verify-example:
+ @if [ -z "$(EXAMPLE)" ]; then \
+ echo "$(RED)Usage: make verify-example EXAMPLE=memory_safety/bounds_overflow$(NC)"; \
+ exit 1; \
+ fi
+ @echo "$(BLUE)Verifying example: $(EXAMPLE)$(NC)"
+ @if [ -d "04_verification_case_studies/$(EXAMPLE)" ]; then \
+ cd 04_verification_case_studies/$(EXAMPLE) && \
+ if [ -f "proof_script.py" ]; then \
+ $(PYTHON) proof_script.py; \
+ else \
+ echo "$(RED)No proof script found$(NC)"; \
+ fi \
+ else \
+ echo "$(RED)Example not found: $(EXAMPLE)$(NC)"; \
+ fi
+
+## test: Run test suite
+test:
+ @echo "$(BLUE)Running tests...$(NC)"
+ @echo "Testing JavaScript..."
+ @if command -v node &> /dev/null; then \
+ for file in assets/js/*.js; do \
+ echo " - $$file"; \
+ node -c $$file || exit 1; \
+ done; \
+ echo "$(GREEN)JavaScript tests passed$(NC)"; \
+ else \
+ echo "$(RED)Node.js not found, skipping JS tests$(NC)"; \
+ fi
+
+## lint: Lint JavaScript and CSS files
+lint:
+ @echo "$(BLUE)Linting files...$(NC)"
+ @if command -v eslint &> /dev/null; then \
+ eslint assets/js/*.js; \
+ else \
+ echo "$(RED)ESLint not found, skipping JS lint$(NC)"; \
+ fi
+ @if command -v stylelint &> /dev/null; then \
+ stylelint assets/styles/*.css; \
+ else \
+ echo "$(RED)Stylelint not found, skipping CSS lint$(NC)"; \
+ fi
+
+## gallery: Generate all gallery visualizations
+gallery: examples
+ @echo "$(BLUE)Generating gallery visualizations...$(NC)"
+ @echo "$(GREEN)Gallery generation complete$(NC)"
+
+## screenshots: Take screenshots of demos (requires playwright/puppeteer)
+screenshots:
+ @echo "$(BLUE)Taking screenshots...$(NC)"
+ @if command -v playwright &> /dev/null; then \
+ playwright screenshot http://localhost:$(PORT) outputs/landing-page.png; \
+ else \
+ echo "$(RED)Playwright not found. Install with: npm install -g playwright$(NC)"; \
+ fi
+
+## clean: Remove generated files
+clean:
+ @echo "$(BLUE)Cleaning generated files...$(NC)"
+ @rm -rf outputs/execution_traces/*
+ @rm -rf outputs/proof_trees/*
+ @rm -rf outputs/memory_diagrams/*
+ @rm -rf outputs/benchmark_results/*
+ @rm -f /tmp/wasm-demo-server.pid
+ @rm -f /tmp/wasm-demo-server.log
+ @echo "$(GREEN)Clean complete$(NC)"
+
+## playground: Start interactive playground
+playground: serve-bg
+ @echo "$(GREEN)Playground started at http://localhost:$(PORT)/06_interactive_playground/$(NC)"
+
+## watch: Watch for file changes and reload (requires entr)
+watch:
+ @if command -v entr &> /dev/null; then \
+ find . -name "*.html" -o -name "*.css" -o -name "*.js" -o -name "*.md" | \
+ entr -r make serve; \
+ else \
+ echo "$(RED)entr not found. Install with: apt install entr$(NC)"; \
+ fi
+
+# Phony targets to avoid conflicts with files
+.PHONY: help install-deps build serve serve-bg stop examples verify-example
+.PHONY: test lint gallery screenshots clean playground watch
diff --git a/demos/formal_semantics_explorer/README.md b/demos/formal_semantics_explorer/README.md
new file mode 100644
index 000000000..f65205f43
--- /dev/null
+++ b/demos/formal_semantics_explorer/README.md
@@ -0,0 +1,382 @@
+# 🌐 WebAssembly Formal Semantics Explorer
+
+> An Interactive Journey Through Formal Verification of WebAssembly using the K Framework
+
+[](http://www.kframework.org/)
+[](https://webassembly.org/)
+[](https://runtimeverification.com/)
+
+---
+
+## 🎯 What is This?
+
+This is an **interactive educational showcase** of formally verified WebAssembly semantics defined in the K Framework. It transforms abstract formal methods into:
+
+✨ **Visual Execution Traces** - Watch WebAssembly instructions execute step-by-step
+🎨 **Interactive Proof Trees** - Explore formal verification derivations
+🔍 **Memory Visualizations** - See stack, heap, and linear memory in 3D
+🎮 **Hands-on Playground** - Write, verify, and debug WebAssembly code
+📚 **Educational Narratives** - Learn through story-driven tutorials
+🧪 **Verification Case Studies** - Real-world security property proofs
+
+---
+
+## 🚀 Quick Start
+
+```bash
+# Clone the fork
+git clone https://github.com/AYUSHMIT/wasm-semantics.git
+cd wasm-semantics/demos/formal_semantics_explorer
+
+# Install dependencies (requires K Framework)
+make install-deps
+
+# Launch interactive explorer
+make serve
+# Opens http://localhost:8000 in your browser
+
+# Run example verification
+make verify-example EXAMPLE=memory_safety/bounds_overflow
+```
+
+---
+
+## 🎨 Gallery Showcase
+
+### Execution Trace Visualization
+
+*Watch Fibonacci computation execute instruction-by-instruction with animated stack*
+
+### Interactive Proof Tree
+
+*Explore formal proof of type soundness with collapsible derivation tree*
+
+### 3D Memory Visualizer
+
+*Navigate WebAssembly linear memory, stack, and heap in interactive 3D space*
+
+### Semantic Rule Browser
+
+*Browse 500+ K rewrite rules with syntax highlighting and search*
+
+### Control Flow Graph
+
+*Visualize branching, loops, and function calls as interactive graphs*
+
+---
+
+## 📚 Learning Paths
+
+### 🟢 Beginner: "First Steps in Formal Semantics" (2-3 hours)
+
+1. **Introduction** → Read [What is Formal Semantics?](01_introduction/00_what_is_formal_semantics.md)
+2. **Hello Wasm** → Try [Hello WebAssembly Semantics](02_interactive_tutorials/hello_wasm_semantics/)
+3. **Stack Machine** → Explore [The Stack Machine Journey](07_educational_narratives/story_1_stack_machine/)
+4. **Interactive** → Play with [WebAssembly Editor](06_interactive_playground/wasm_editor/)
+
+**Goal**: Understand how formal semantics describes program behavior
+
+### 🟡 Intermediate: "Verification Practitioner" (6-8 hours)
+
+1. **Control Flow** → Master [Loops & Branches](02_interactive_tutorials/control_flow/)
+2. **Memory Safety** → Study [Bounds Checking](02_interactive_tutorials/memory_operations/)
+3. **Type System** → Learn [Type Soundness](04_verification_case_studies/type_soundness/)
+4. **K Framework** → Deep dive into [Rewrite Rules](05_k_framework_deep_dive/rewrite_rules/)
+5. **Hands-on** → Build proofs in [Verification Sandbox](06_interactive_playground/verification_sandbox/)
+
+**Goal**: Verify safety properties of WebAssembly programs
+
+### 🔴 Advanced: "Formal Methods Researcher" (2-3 days)
+
+1. **Concurrency** → Tackle [Thread Semantics & Memory Models](08_advanced_topics/concurrency/)
+2. **Compiler Correctness** → Prove [Semantic Equivalence](04_verification_case_studies/compiler_correctness/)
+3. **Symbolic Execution** → Master [Symbolic Backend](05_k_framework_deep_dive/backends/)
+4. **Research** → Compare [Formal Tools](09_comparison_studies/formal_tools_comparison/)
+5. **Contribute** → Extend semantics via [Contribution Guide](10_community_resources/contribution_guide.md)
+
+**Goal**: Advance state-of-the-art in WebAssembly verification
+
+---
+
+## 🎓 Featured Tutorials
+
+| Tutorial | Complexity | Time | Highlights |
+|----------|-----------|------|------------|
+| [Hello Wasm Semantics](02_interactive_tutorials/hello_wasm_semantics/) | ⭐ | 20 min | First formal execution trace |
+| [Arithmetic Operations](02_interactive_tutorials/arithmetic_operations/) | ⭐⭐ | 45 min | Interactive stepper, overflow detection |
+| [Control Flow](02_interactive_tutorials/control_flow/) | ⭐⭐ | 1 hour | CFG visualization, branch semantics |
+| [Function Calls](02_interactive_tutorials/function_calls/) | ⭐⭐⭐ | 1.5 hours | Stack frames, recursion, tail calls |
+| [Memory Operations](02_interactive_tutorials/memory_operations/) | ⭐⭐⭐ | 2 hours | Memory safety proofs, bounds checking |
+| [Memory Safety Case Study](04_verification_case_studies/memory_safety/) | ⭐⭐⭐⭐ | 3 hours | Full verification workflow |
+| [Compiler Correctness](04_verification_case_studies/compiler_correctness/) | ⭐⭐⭐⭐⭐ | 4 hours | Bisimulation, semantic equivalence |
+
+---
+
+## 🌟 Highlighted Features
+
+### Interactive Execution Stepper
+
+
+Step through WebAssembly execution with:
+- 🎬 Play/pause/step-forward/step-back controls
+- 📊 Real-time stack visualization
+- 🔍 Current instruction highlighting
+- 📝 K configuration state display
+- 🎨 Animated transitions between states
+
+### Proof Tree Explorer
+
+
+Navigate formal proofs with:
+- 🌳 Collapsible/expandable tree nodes
+- 🔗 Click nodes to see K rule application
+- 🎯 Highlight proof path to conclusion
+- 💾 Export to LaTeX/GraphML
+- 🔎 Search proof by rule name
+
+### Memory Inspector 3D
+
+
+Explore memory with:
+- 🎮 3D navigation (pan, zoom, rotate)
+- 🎨 Color-coded by type (i32, i64, f32, f64)
+- 📍 Click address to inspect value
+- ⏱️ Timeline slider (watch memory evolve)
+- 📊 Stack growth animation
+
+### Semantic Rule Browser
+
+
+Discover K rules with:
+- 🔍 Full-text search across all rules
+- 🏷️ Filter by category (arithmetic, control, memory)
+- 📖 Syntax-highlighted K notation
+- 🔗 Rule dependency graph
+- 📚 Link to specification section
+
+---
+
+## 🎮 Interactive Playground
+
+Launch the full-featured playground:
+
+```bash
+make playground
+```
+
+**Features:**
+- **Monaco Editor** - Industry-standard editor with WebAssembly syntax highlighting
+- **Live Validation** - Real-time type checking and syntax errors
+- **Autocomplete** - Intelligent suggestions for instructions, types, imports
+- **Execution Modes**:
+ - 🏃 Concrete: Run with actual values
+ - 🔮 Symbolic: Explore all possible executions
+ - 🐛 Debug: Step-by-step with breakpoints
+- **Verification Panel** - Write specifications and check properties
+- **Export Options** - Download .wat, .wasm, proofs, traces
+
+---
+
+## 🧪 Verification Case Studies
+
+### Case Study 1: Memory Safety
+
+**Problem**: Prove that WebAssembly memory operations never access out-of-bounds addresses.
+
+**Approach**:
+1. Define memory safety specification in K
+2. Identify all memory-accessing instructions
+3. Prove bounds checking happens before every access
+4. Verify trap behavior on violation
+
+**Files**:
+- [Bounds Overflow Example](04_verification_case_studies/memory_safety/bounds_overflow.wat)
+- [Formal Specification](04_verification_case_studies/memory_safety/verification_spec.k)
+- [Automated Proof Script](04_verification_case_studies/memory_safety/proof_script.py)
+- [Interactive Results Dashboard](04_verification_case_studies/memory_safety/results_dashboard.html)
+
+**Outcome**: ✅ Proved memory safety holds for all valid WebAssembly modules
+
+### Case Study 2: Type Soundness
+
+**Theorem**: "Well-typed programs don't go wrong"
+
+**Proof Strategy**:
+1. **Type Preservation** - Types are preserved during execution
+2. **Progress** - Well-typed programs never get stuck
+
+**Visualization**: [Interactive Proof Tree](04_verification_case_studies/type_soundness/progress_proof.html)
+
+### Case Study 3: Deterministic Execution
+
+**Property**: Given the same inputs, WebAssembly always produces the same outputs.
+
+**Verification**:
+- Compare execution traces from different runs
+- Prove confluence of rewrite rules
+- Check for non-deterministic constructs
+
+**Demo**: [Trace Comparison Tool](04_verification_case_studies/determinism/trace_comparison.html)
+
+---
+
+## 🔬 K Framework Deep Dive
+
+### What is the K Framework?
+
+The K Framework is a rewrite-based executable semantic framework where:
+- Programming languages are defined as term rewriting systems
+- Execution is rule application on configurations
+- Verification uses reachability logic and symbolic execution
+
+**Example K Rule**:
+```k
+rule
+
+**Built with 🔬 using K Framework • WebAssembly • Formal Methods**
+
+[🏠 Back to Top](#-webassembly-formal-semantics-explorer)
+
+
diff --git a/demos/formal_semantics_explorer/assets/images/k_framework_logo.svg b/demos/formal_semantics_explorer/assets/images/k_framework_logo.svg
new file mode 100644
index 000000000..39f9aff9b
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/images/k_framework_logo.svg
@@ -0,0 +1,8 @@
+
diff --git a/demos/formal_semantics_explorer/assets/images/semantics_workflow.svg b/demos/formal_semantics_explorer/assets/images/semantics_workflow.svg
new file mode 100644
index 000000000..a6fa57d4c
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/images/semantics_workflow.svg
@@ -0,0 +1,81 @@
+
diff --git a/demos/formal_semantics_explorer/assets/images/wasm_architecture.svg b/demos/formal_semantics_explorer/assets/images/wasm_architecture.svg
new file mode 100644
index 000000000..b0ab08831
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/images/wasm_architecture.svg
@@ -0,0 +1,44 @@
+
diff --git a/demos/formal_semantics_explorer/assets/js/k_semantics_renderer.js b/demos/formal_semantics_explorer/assets/js/k_semantics_renderer.js
new file mode 100644
index 000000000..e57c0237e
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/js/k_semantics_renderer.js
@@ -0,0 +1,294 @@
+// K Semantics Renderer
+// Renders K Framework rules and configurations
+
+class KSemanticsRenderer {
+ constructor(containerId) {
+ this.container = document.getElementById(containerId);
+ this.rules = [];
+ this.currentConfig = null;
+ }
+
+ // Load K rules from data
+ loadRules(rules) {
+ this.rules = rules;
+ this.renderRulesList();
+ }
+
+ // Render list of rules
+ renderRulesList() {
+ if (!this.container) return;
+
+ const html = `
+
+
+ `;
+
+ this.container.innerHTML = html;
+ this.attachEventListeners();
+ }
+
+ // Render individual rule
+ renderRule(rule, index) {
+ return `
+
+
+ K Semantic Rules
+ +
+
+
+
+
+
+
+
+ ${this.rules.map((rule, index) => this.renderRule(rule, index)).join('')}
+
+
+
+ `;
+ }
+
+ // Render K configuration
+ renderConfiguration(config) {
+ this.currentConfig = config;
+
+ const html = `
+
+
+
+ ${rule.name}
+ ${rule.category} +
+
+ `;
+
+ if (this.container) {
+ this.container.innerHTML = html;
+ }
+ }
+
+ // Render configuration cell
+ renderCell(cell, name) {
+ if (typeof cell === 'string' || typeof cell === 'number') {
+ return `
+ Configuration State
+
+ ${this.renderCell(config, 'T')}
+
+
+ <${name}>
+ ${this.escapeHtml(String(cell))}
+
+ `;
+ }
+
+ if (Array.isArray(cell)) {
+ return `
+
+ <${name}>
+
+ `;
+ }
+
+ if (typeof cell === 'object') {
+ return `
+
+ ${cell.map((item, i) => this.renderCell(item, `item-${i}`)).join('')}
+
+
+ <${name}>
+
+ `;
+ }
+
+ return '';
+ }
+
+ // Highlight rule application
+ highlightRuleApplication(ruleIndex, config) {
+ // Render the rule being applied
+ const rule = this.rules[ruleIndex];
+
+ const html = `
+
+ ${Object.entries(cell).map(([key, value]) =>
+ this.renderCell(value, key)
+ ).join('')}
+
+
+
+ `;
+
+ if (this.container) {
+ this.container.innerHTML = html;
+ }
+ }
+
+ // Attach event listeners
+ attachEventListeners() {
+ // Search functionality
+ const searchInput = document.getElementById('rule-search');
+ if (searchInput) {
+ searchInput.addEventListener('input', (e) => {
+ this.filterRules(e.target.value);
+ });
+ }
+
+ // Filter buttons
+ document.querySelectorAll('.filter-btn').forEach(btn => {
+ btn.addEventListener('click', (e) => {
+ document.querySelectorAll('.filter-btn').forEach(b =>
+ b.classList.remove('active')
+ );
+ e.target.classList.add('active');
+ this.filterByCategory(e.target.dataset.category);
+ });
+ });
+ }
+
+ // Filter rules by search term
+ filterRules(searchTerm) {
+ const term = searchTerm.toLowerCase();
+ document.querySelectorAll('.k-rule-item').forEach(item => {
+ const index = parseInt(item.dataset.index);
+ const rule = this.rules[index];
+ const matches =
+ rule.name.toLowerCase().includes(term) ||
+ rule.description.toLowerCase().includes(term) ||
+ rule.category.toLowerCase().includes(term);
+
+ item.style.display = matches ? 'block' : 'none';
+ });
+ }
+
+ // Filter rules by category
+ filterByCategory(category) {
+ document.querySelectorAll('.k-rule-item').forEach(item => {
+ const matches =
+ category === 'all' ||
+ item.dataset.category === category;
+
+ item.style.display = matches ? 'block' : 'none';
+ });
+ }
+
+ // Escape HTML
+ escapeHtml(text) {
+ const div = document.createElement('div');
+ div.textContent = text;
+ return div.innerHTML;
+ }
+
+ // Export rules to JSON
+ exportRules() {
+ return JSON.stringify(this.rules, null, 2);
+ }
+
+ // Load sample rules
+ loadSampleRules() {
+ this.rules = [
+ {
+ name: 'i32.add',
+ category: 'arithmetic',
+ lhs: 'Applying Rule: ${rule.name}
+
+
+
+
+ Before:
+ ${this.renderConfiguration(config.before)} +⇓
+
+
+ After:
+ ${this.renderConfiguration(config.after)} +
+ ${this.renderRule(rule, ruleIndex)}
+
+
+
+
+
+
+
+ ${this.renderNode(this.tree, 0)}
+
+
+
+
+ `;
+
+ this.container.innerHTML = html;
+ }
+
+ // Render tree node recursively
+ renderNode(node, depth) {
+ const hasChildren = node.children && node.children.length > 0;
+ const nodeId = `node-${depth}-${Math.random().toString(36).substr(2, 9)}`;
+
+ let html = `
+ Click on a node to see details
+
+
';
+ return html;
+ }
+
+ // Toggle node expansion
+ toggleNode(nodeId) {
+ const node = document.querySelector(`[data-node-id="${nodeId}"]`);
+ if (!node) return;
+
+ const children = node.querySelector('.proof-children');
+ const icon = node.querySelector('.collapse-icon');
+
+ if (children) {
+ const isCollapsed = children.style.display === 'none';
+ children.style.display = isCollapsed ? 'block' : 'none';
+ icon.textContent = isCollapsed ? '▼' : '▶';
+ }
+
+ this.showNodeDetails(node);
+ }
+
+ // Show node details
+ showNodeDetails(node) {
+ const details = document.getElementById('proof-details');
+ if (!details) return;
+
+ // Extract node information
+ const goal = node.querySelector('.proof-goal').textContent;
+ const rule = node.querySelector('.proof-rule').textContent;
+
+ details.innerHTML = `
+
+ ${hasChildren ? '' : ''}
+ ${this.escapeHtml(node.goal)}
+ ${node.rule}
+
+ `;
+
+ if (hasChildren) {
+ html += '';
+ node.children.forEach(child => {
+ html += this.renderNode(child, depth + 1);
+ });
+ html += '
';
+ }
+
+ html += 'Proof Step Details
+
+ Goal:
+
+ ${goal}
+ Rule Applied:
+
+ ${rule}
+
+ Description:
+
+ `;
+ }
+
+ // Get rule description
+ getRuleDescription(rule) {
+ const descriptions = {
+ 'Type-Int': 'Integer constants have type i32',
+ 'Type-Add': 'Addition requires two operands of the same numeric type',
+ 'Type-If': 'Conditional requires i32 condition and matching branch types',
+ 'Type-Call': 'Function call must match declared function signature',
+ 'Type-Load': 'Memory load requires i32 address and produces typed value',
+ 'Type-Store': 'Memory store requires i32 address and typed value',
+ 'Eval-Add': 'Evaluate addition by computing sum of operands',
+ 'Eval-If-True': 'Take then-branch when condition is non-zero',
+ 'Eval-If-False': 'Take else-branch when condition is zero',
+ 'Progress': 'Well-typed expression can take a step or is a value',
+ 'Preservation': 'Type is preserved during evaluation step'
+ };
+ return descriptions[rule] || 'No description available';
+ }
+
+ // Expand all nodes
+ expandAll() {
+ document.querySelectorAll('.proof-children').forEach(children => {
+ children.style.display = 'block';
+ });
+ document.querySelectorAll('.collapse-icon').forEach(icon => {
+ icon.textContent = '▼';
+ });
+ }
+
+ // Collapse all nodes
+ collapseAll() {
+ document.querySelectorAll('.proof-children').forEach(children => {
+ children.style.display = 'none';
+ });
+ document.querySelectorAll('.collapse-icon').forEach(icon => {
+ icon.textContent = '▶';
+ });
+ }
+
+ // Export tree to various formats
+ exportTree() {
+ const format = prompt('Export format (json/latex/dot):', 'json');
+
+ switch (format) {
+ case 'json':
+ this.exportJSON();
+ break;
+ case 'latex':
+ this.exportLaTeX();
+ break;
+ case 'dot':
+ this.exportDot();
+ break;
+ default:
+ alert('Unknown format');
+ }
+ }
+
+ // Export to JSON
+ exportJSON() {
+ const json = JSON.stringify(this.tree, null, 2);
+ this.downloadFile('proof-tree.json', json);
+ }
+
+ // Export to LaTeX
+ exportLaTeX() {
+ const latex = this.treeToLaTeX(this.tree);
+ this.downloadFile('proof-tree.tex', latex);
+ }
+
+ // Convert tree to LaTeX
+ treeToLaTeX(node, indent = 0) {
+ const spaces = ' '.repeat(indent);
+ let latex = `${spaces}\\infer{${node.goal}}\n`;
+
+ if (node.children && node.children.length > 0) {
+ latex += `${spaces}{\n`;
+ node.children.forEach(child => {
+ latex += this.treeToLaTeX(child, indent + 1);
+ });
+ latex += `${spaces}}\n`;
+ }
+
+ return latex;
+ }
+
+ // Export to Graphviz DOT
+ exportDot() {
+ let dot = 'digraph ProofTree {\n';
+ dot += ' node [shape=box];\n';
+ dot += this.treeToDot(this.tree, 0);
+ dot += '}\n';
+ this.downloadFile('proof-tree.dot', dot);
+ }
+
+ // Convert tree to DOT format
+ treeToDot(node, id) {
+ let dot = ` node${id} [label="${node.goal}\\n[${node.rule}]"];\n`;
+
+ if (node.children && node.children.length > 0) {
+ node.children.forEach((child, index) => {
+ const childId = id * 100 + index;
+ dot += this.treeToDot(child, childId);
+ dot += ` node${id} -> node${childId};\n`;
+ });
+ }
+
+ return dot;
+ }
+
+ // Download file helper
+ downloadFile(filename, content) {
+ const blob = new Blob([content], { type: 'text/plain' });
+ const url = URL.createObjectURL(blob);
+ const a = document.createElement('a');
+ a.href = url;
+ a.download = filename;
+ a.click();
+ URL.revokeObjectURL(url);
+ }
+
+ // Escape HTML
+ escapeHtml(text) {
+ const div = document.createElement('div');
+ div.textContent = text;
+ return div.innerHTML;
+ }
+
+ // Load sample proof tree
+ loadSampleTree() {
+ this.tree = {
+ goal: '⊢ (1 + 2) + 3 : i32',
+ rule: 'Type-Add',
+ children: [
+ {
+ goal: '⊢ 1 + 2 : i32',
+ rule: 'Type-Add',
+ children: [
+ {
+ goal: '⊢ 1 : i32',
+ rule: 'Type-Int',
+ children: []
+ },
+ {
+ goal: '⊢ 2 : i32',
+ rule: 'Type-Int',
+ children: []
+ }
+ ]
+ },
+ {
+ goal: '⊢ 3 : i32',
+ rule: 'Type-Int',
+ children: []
+ }
+ ]
+ };
+ this.render();
+ }
+}
+
+// Global instance
+let proofTree = null;
+
+// Initialize on page load
+document.addEventListener('DOMContentLoaded', () => {
+ const container = document.getElementById('proof-tree-container');
+ if (container) {
+ proofTree = new ProofTreeBuilder('proof-tree-container');
+ proofTree.loadSampleTree();
+ }
+});
+
+// Export for use in other modules
+if (typeof module !== 'undefined' && module.exports) {
+ module.exports = ProofTreeBuilder;
+}
diff --git a/demos/formal_semantics_explorer/assets/js/state_inspector.js b/demos/formal_semantics_explorer/assets/js/state_inspector.js
new file mode 100644
index 000000000..ec3c01234
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/js/state_inspector.js
@@ -0,0 +1,361 @@
+// State Inspector
+// Inspects and displays WebAssembly execution state
+
+class StateInspector {
+ constructor(containerId) {
+ this.container = document.getElementById(containerId);
+ this.state = null;
+ }
+
+ // Load execution state
+ loadState(state) {
+ this.state = state;
+ this.render();
+ }
+
+ // Render complete state
+ render() {
+ if (!this.container || !this.state) return;
+
+ const html = `
+ ${this.getRuleDescription(rule)}
+
+
+ `;
+
+ this.container.innerHTML = html;
+ this.attachEventListeners();
+ }
+
+ // Render stack view
+ renderStack() {
+ if (!this.state.stack || this.state.stack.length === 0) {
+ return '
+
+
+
+
+
+
+
+
+ ${this.renderStack()}
+
+
+
+ ${this.renderMemory()}
+
+
+
+ ${this.renderLocals()}
+
+
+
+ ${this.renderGlobals()}
+
+
+
+ ${this.renderTables()}
+
+ Stack is empty
';
+ }
+
+ return `
+
+
+
+
+
+ `;
+ }
+
+ // Render memory view
+ renderMemory() {
+ const memory = this.state.memory || [];
+ const pageSize = 64 * 1024; // 64KB pages
+ const numPages = Math.ceil(memory.length / pageSize);
+
+ return `
+ | Index | +Type | +Value | +
|---|---|---|
| ${index} | +${item.type} | +${this.formatValue(item.value, item.type)} |
+
+
+ `;
+ }
+
+ // Render memory page
+ renderMemoryPage(pageNum) {
+ const memory = this.state.memory || [];
+ const pageSize = 64 * 1024;
+ const start = pageNum * pageSize;
+ const end = Math.min(start + 256, memory.length); // Show 256 bytes
+
+ let html = '
+
+
+
+
+
+ ${this.renderMemoryPage(0)}
+
+ ';
+
+ for (let addr = start; addr < end; addr += 16) {
+ html += `
';
+ return html;
+ }
+
+ // Render locals view
+ renderLocals() {
+ if (!this.state.locals || this.state.locals.length === 0) {
+ return '`;
+ html += `${this.formatHex(addr, 8)}:`;
+
+ // Hex values
+ html += '';
+ for (let i = 0; i < 16; i++) {
+ if (addr + i < end) {
+ const byte = memory[addr + i] || 0;
+ html += `${this.formatHex(byte, 2)}`;
+ } else {
+ html += ' ';
+ }
+ }
+ html += '';
+
+ // ASCII representation
+ html += '';
+ for (let i = 0; i < 16; i++) {
+ if (addr + i < end) {
+ const byte = memory[addr + i] || 0;
+ html += this.byteToAscii(byte);
+ }
+ }
+ html += '';
+
+ html += '
';
+ }
+
+ html += 'No local variables
';
+ }
+
+ return `
+
+
+
+
+
+ `;
+ }
+
+ // Render globals view
+ renderGlobals() {
+ if (!this.state.globals || this.state.globals.length === 0) {
+ return '| Index | +Name | +Type | +Value | +
|---|---|---|---|
| ${index} | +${local.name || '-'} | +${local.type} | +${this.formatValue(local.value, local.type)} |
+
No global variables
';
+ }
+
+ return `
+
+
+
+
+
+ `;
+ }
+
+ // Render tables view
+ renderTables() {
+ if (!this.state.tables || this.state.tables.length === 0) {
+ return '| Index | +Name | +Type | +Mutable | +Value | +
|---|---|---|---|---|
| ${index} | +${global.name || '-'} | +${global.type} | +${global.mutable ? '✓' : '✗'} | +${this.formatValue(global.value, global.type)} |
+
No tables
';
+ }
+
+ return `
+
+ ${this.state.tables.map((table, index) => `
+
+ `;
+ }
+
+ // Attach event listeners
+ attachEventListeners() {
+ // Tab switching
+ document.querySelectorAll('.state-tab').forEach(tab => {
+ tab.addEventListener('click', (e) => {
+ const tabName = e.target.dataset.tab;
+
+ // Update active tab
+ document.querySelectorAll('.state-tab').forEach(t =>
+ t.classList.remove('active')
+ );
+ e.target.classList.add('active');
+
+ // Update active content
+ document.querySelectorAll('.state-content').forEach(c =>
+ c.classList.remove('active')
+ );
+ document.querySelector(`.state-content[data-tab="${tabName}"]`)
+ .classList.add('active');
+ });
+ });
+
+ // Memory page selection
+ const pageSelect = document.getElementById('memory-page-select');
+ if (pageSelect) {
+ pageSelect.addEventListener('change', (e) => {
+ const pageNum = parseInt(e.target.value);
+ document.getElementById('memory-hex').innerHTML =
+ this.renderMemoryPage(pageNum);
+ });
+ }
+ }
+
+ // Format value based on type
+ formatValue(value, type) {
+ switch (type) {
+ case 'i32':
+ case 'i64':
+ return `${value} (0x${value.toString(16).toUpperCase()})`;
+ case 'f32':
+ case 'f64':
+ return value.toFixed(6);
+ default:
+ return String(value);
+ }
+ }
+
+ // Format hex number
+ formatHex(num, width) {
+ return num.toString(16).toUpperCase().padStart(width, '0');
+ }
+
+ // Convert byte to ASCII
+ byteToAscii(byte) {
+ return (byte >= 32 && byte <= 126)
+ ? String.fromCharCode(byte)
+ : '.';
+ }
+
+ // Export state to JSON
+ exportState() {
+ return JSON.stringify(this.state, null, 2);
+ }
+
+ // Load sample state
+ loadSampleState() {
+ this.state = {
+ stack: [
+ { type: 'i32', value: 42 },
+ { type: 'i32', value: 10 },
+ { type: 'f64', value: 3.14159 }
+ ],
+ memory: new Array(1024).fill(0).map((_, i) => i % 256),
+ locals: [
+ { name: 'x', type: 'i32', value: 100 },
+ { name: 'y', type: 'f64', value: 2.71828 }
+ ],
+ globals: [
+ { name: 'counter', type: 'i32', mutable: true, value: 0 },
+ { name: 'PI', type: 'f64', mutable: false, value: 3.14159 }
+ ],
+ tables: [
+ {
+ type: 'funcref',
+ elements: ['func_0', 'func_1', 'func_2', null]
+ }
+ ]
+ };
+ this.render();
+ }
+}
+
+// Global helper function
+function inspectMemoryAddress() {
+ const input = document.getElementById('memory-address');
+ if (input) {
+ const address = parseInt(input.value, 16);
+ // Scroll to address in memory view
+ console.log('Inspecting address:', address);
+ }
+}
+
+// Export for use in other modules
+if (typeof module !== 'undefined' && module.exports) {
+ module.exports = StateInspector;
+}
diff --git a/demos/formal_semantics_explorer/assets/js/wasm_visualizer.js b/demos/formal_semantics_explorer/assets/js/wasm_visualizer.js
new file mode 100644
index 000000000..7472f6f31
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/js/wasm_visualizer.js
@@ -0,0 +1,279 @@
+// WebAssembly Visualizer
+// Handles visual execution traces and stack animations
+
+class WasmVisualizer {
+ constructor(canvasId) {
+ this.canvas = document.getElementById(canvasId);
+ this.ctx = this.canvas ? this.canvas.getContext('2d') : null;
+ this.executionTrace = [];
+ this.currentStep = 0;
+ this.stack = [];
+ this.memory = new Array(65536).fill(0);
+ this.animationSpeed = 500; // ms
+ this.isPlaying = false;
+ }
+
+ // Load execution trace from data
+ loadTrace(trace) {
+ this.executionTrace = trace;
+ this.currentStep = 0;
+ this.reset();
+ }
+
+ // Reset visualizer state
+ reset() {
+ this.stack = [];
+ this.memory = new Array(65536).fill(0);
+ this.currentStep = 0;
+ this.isPlaying = false;
+ this.render();
+ }
+
+ // Execute next step
+ step() {
+ if (this.currentStep >= this.executionTrace.length) {
+ this.isPlaying = false;
+ return false;
+ }
+
+ const instruction = this.executionTrace[this.currentStep];
+ this.executeInstruction(instruction);
+ this.currentStep++;
+ this.render();
+ return true;
+ }
+
+ // Step backward
+ stepBack() {
+ if (this.currentStep <= 0) return false;
+
+ this.currentStep--;
+ this.replayToCurrentStep();
+ this.render();
+ return true;
+ }
+
+ // Play animation
+ play() {
+ if (this.isPlaying) return;
+ this.isPlaying = true;
+ this.animate();
+ }
+
+ // Pause animation
+ pause() {
+ this.isPlaying = false;
+ }
+
+ // Animation loop
+ animate() {
+ if (!this.isPlaying) return;
+
+ const hasNext = this.step();
+ if (hasNext) {
+ setTimeout(() => this.animate(), this.animationSpeed);
+ } else {
+ this.isPlaying = false;
+ }
+ }
+
+ // Replay execution to current step
+ replayToCurrentStep() {
+ this.stack = [];
+ this.memory = new Array(65536).fill(0);
+
+ for (let i = 0; i < this.currentStep; i++) {
+ this.executeInstruction(this.executionTrace[i]);
+ }
+ }
+
+ // Execute a single instruction
+ executeInstruction(instruction) {
+ const { opcode, args } = instruction;
+
+ switch (opcode) {
+ case 'i32.const':
+ this.stack.push({ type: 'i32', value: args[0] });
+ break;
+ case 'i64.const':
+ this.stack.push({ type: 'i64', value: args[0] });
+ break;
+ case 'f32.const':
+ this.stack.push({ type: 'f32', value: args[0] });
+ break;
+ case 'f64.const':
+ this.stack.push({ type: 'f64', value: args[0] });
+ break;
+ case 'i32.add':
+ this.binaryOp((a, b) => a + b);
+ break;
+ case 'i32.sub':
+ this.binaryOp((a, b) => a - b);
+ break;
+ case 'i32.mul':
+ this.binaryOp((a, b) => a * b);
+ break;
+ case 'i32.div_s':
+ this.binaryOp((a, b) => Math.floor(a / b));
+ break;
+ case 'i32.load':
+ this.memoryLoad(args[0], 4);
+ break;
+ case 'i32.store':
+ this.memoryStore(args[0], 4);
+ break;
+ default:
+ console.warn(`Unhandled instruction: ${opcode}`);
+ }
+ }
+
+ // Binary operation helper
+ binaryOp(op) {
+ if (this.stack.length < 2) return;
+ const b = this.stack.pop();
+ const a = this.stack.pop();
+ const result = op(a.value, b.value);
+ this.stack.push({ type: a.type, value: result });
+ }
+
+ // Memory load operation
+ memoryLoad(offset, bytes) {
+ if (this.stack.length < 1) return;
+ const addr = this.stack.pop().value + offset;
+ let value = 0;
+ for (let i = 0; i < bytes; i++) {
+ value |= (this.memory[addr + i] << (i * 8));
+ }
+ this.stack.push({ type: 'i32', value });
+ }
+
+ // Memory store operation
+ memoryStore(offset, bytes) {
+ if (this.stack.length < 2) return;
+ const value = this.stack.pop().value;
+ const addr = this.stack.pop().value + offset;
+ for (let i = 0; i < bytes; i++) {
+ this.memory[addr + i] = (value >> (i * 8)) & 0xFF;
+ }
+ }
+
+ // Render current state
+ render() {
+ if (!this.ctx) return;
+
+ const width = this.canvas.width;
+ const height = this.canvas.height;
+
+ // Clear canvas
+ this.ctx.clearRect(0, 0, width, height);
+
+ // Draw stack
+ this.drawStack(50, 50, 150, height - 100);
+
+ // Draw current instruction
+ this.drawCurrentInstruction(250, 50);
+
+ // Draw step counter
+ this.drawStepCounter(250, 100);
+ }
+
+ // Draw stack visualization
+ drawStack(x, y, width, height) {
+ if (!this.ctx) return;
+
+ // Draw stack frame
+ this.ctx.strokeStyle = '#0066cc';
+ this.ctx.lineWidth = 2;
+ this.ctx.strokeRect(x, y, width, height);
+
+ // Draw stack label
+ this.ctx.fillStyle = '#1e293b';
+ this.ctx.font = 'bold 16px Inter';
+ this.ctx.fillText('Stack', x, y - 10);
+
+ // Draw stack items
+ const itemHeight = 40;
+ const itemMargin = 5;
+
+ this.stack.forEach((item, index) => {
+ const itemY = y + height - (index + 1) * (itemHeight + itemMargin);
+
+ // Draw item background
+ this.ctx.fillStyle = this.getTypeColor(item.type);
+ this.ctx.fillRect(x + 5, itemY, width - 10, itemHeight);
+
+ // Draw item text
+ this.ctx.fillStyle = '#ffffff';
+ this.ctx.font = '14px Fira Code';
+ this.ctx.fillText(
+ `${item.type}: ${item.value}`,
+ x + 10,
+ itemY + 25
+ );
+ });
+ }
+
+ // Draw current instruction
+ drawCurrentInstruction(x, y) {
+ if (!this.ctx || this.currentStep >= this.executionTrace.length) return;
+
+ const instruction = this.executionTrace[this.currentStep];
+
+ this.ctx.fillStyle = '#1e293b';
+ this.ctx.font = 'bold 16px Inter';
+ this.ctx.fillText('Current Instruction:', x, y);
+
+ this.ctx.font = '14px Fira Code';
+ this.ctx.fillStyle = '#0066cc';
+ this.ctx.fillText(
+ `${instruction.opcode} ${instruction.args.join(', ')}`,
+ x,
+ y + 30
+ );
+ }
+
+ // Draw step counter
+ drawStepCounter(x, y) {
+ if (!this.ctx) return;
+
+ this.ctx.fillStyle = '#64748b';
+ this.ctx.font = '14px Inter';
+ this.ctx.fillText(
+ `Step ${this.currentStep} / ${this.executionTrace.length}`,
+ x,
+ y
+ );
+ }
+
+ // Get color for value type
+ getTypeColor(type) {
+ const colors = {
+ 'i32': '#4fc1ff',
+ 'i64': '#4fc1ff',
+ 'f32': '#b5cea8',
+ 'f64': '#b5cea8',
+ 'funcref': '#ce9178',
+ 'externref': '#ce9178'
+ };
+ return colors[type] || '#808080';
+ }
+
+ // Set animation speed
+ setSpeed(speed) {
+ this.animationSpeed = speed;
+ }
+
+ // Export current state
+ exportState() {
+ return {
+ step: this.currentStep,
+ stack: [...this.stack],
+ memory: [...this.memory]
+ };
+ }
+}
+
+// Export for use in other modules
+if (typeof module !== 'undefined' && module.exports) {
+ module.exports = WasmVisualizer;
+}
diff --git a/demos/formal_semantics_explorer/assets/styles/formal_methods.css b/demos/formal_semantics_explorer/assets/styles/formal_methods.css
new file mode 100644
index 000000000..29aefade3
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/styles/formal_methods.css
@@ -0,0 +1,503 @@
+/* K Framework Themed Styling */
+
+:root {
+ /* K Framework Colors */
+ --k-blue: #0066cc;
+ --k-dark-blue: #004499;
+ --k-light-blue: #4d94ff;
+ --wasm-purple: #654ff0;
+ --verify-green: #10b981;
+ --warning-orange: #f59e0b;
+ --error-red: #ef4444;
+
+ /* Neutral Colors */
+ --bg-primary: #ffffff;
+ --bg-secondary: #f8fafc;
+ --bg-tertiary: #e2e8f0;
+ --text-primary: #1e293b;
+ --text-secondary: #64748b;
+ --text-tertiary: #94a3b8;
+ --border-color: #cbd5e1;
+
+ /* Shadows */
+ --shadow-sm: 0 1px 2px 0 rgba(0, 0, 0, 0.05);
+ --shadow-md: 0 4px 6px -1px rgba(0, 0, 0, 0.1);
+ --shadow-lg: 0 10px 15px -3px rgba(0, 0, 0, 0.1);
+ --shadow-xl: 0 20px 25px -5px rgba(0, 0, 0, 0.1);
+
+ /* Spacing */
+ --spacing-xs: 0.5rem;
+ --spacing-sm: 0.75rem;
+ --spacing-md: 1rem;
+ --spacing-lg: 1.5rem;
+ --spacing-xl: 2rem;
+ --spacing-2xl: 3rem;
+
+ /* Border Radius */
+ --radius-sm: 0.375rem;
+ --radius-md: 0.5rem;
+ --radius-lg: 0.75rem;
+ --radius-xl: 1rem;
+
+ /* Typography */
+ --font-sans: 'Inter', -apple-system, BlinkMacSystemFont, 'Segoe UI', sans-serif;
+ --font-mono: 'Fira Code', 'Courier New', monospace;
+}
+
+/* Dark Mode Support */
+@media (prefers-color-scheme: dark) {
+ :root {
+ --bg-primary: #0f172a;
+ --bg-secondary: #1e293b;
+ --bg-tertiary: #334155;
+ --text-primary: #f1f5f9;
+ --text-secondary: #cbd5e1;
+ --text-tertiary: #94a3b8;
+ --border-color: #475569;
+ }
+}
+
+/* Reset & Base Styles */
+* {
+ margin: 0;
+ padding: 0;
+ box-sizing: border-box;
+}
+
+body {
+ font-family: var(--font-sans);
+ font-size: 16px;
+ line-height: 1.6;
+ color: var(--text-primary);
+ background-color: var(--bg-primary);
+ -webkit-font-smoothing: antialiased;
+ -moz-osx-font-smoothing: grayscale;
+}
+
+/* Container */
+.container {
+ max-width: 1280px;
+ margin: 0 auto;
+ padding: 0 var(--spacing-xl);
+}
+
+/* Typography */
+h1, h2, h3, h4, h5, h6 {
+ font-weight: 700;
+ line-height: 1.2;
+ margin-bottom: var(--spacing-md);
+}
+
+h1 { font-size: 2.5rem; }
+h2 { font-size: 2rem; }
+h3 { font-size: 1.5rem; }
+h4 { font-size: 1.25rem; }
+h5 { font-size: 1.125rem; }
+h6 { font-size: 1rem; }
+
+p {
+ margin-bottom: var(--spacing-md);
+}
+
+a {
+ color: var(--k-blue);
+ text-decoration: none;
+ transition: color 0.2s ease;
+}
+
+a:hover {
+ color: var(--k-dark-blue);
+}
+
+/* Buttons */
+.btn {
+ display: inline-flex;
+ align-items: center;
+ gap: var(--spacing-xs);
+ padding: var(--spacing-sm) var(--spacing-lg);
+ border: none;
+ border-radius: var(--radius-md);
+ font-family: var(--font-sans);
+ font-size: 1rem;
+ font-weight: 600;
+ text-decoration: none;
+ cursor: pointer;
+ transition: all 0.2s ease;
+}
+
+.btn-primary {
+ background-color: var(--k-blue);
+ color: white;
+}
+
+.btn-primary:hover {
+ background-color: var(--k-dark-blue);
+ transform: translateY(-1px);
+ box-shadow: var(--shadow-md);
+}
+
+.btn-secondary {
+ background-color: transparent;
+ color: var(--k-blue);
+ border: 2px solid var(--k-blue);
+}
+
+.btn-secondary:hover {
+ background-color: var(--k-blue);
+ color: white;
+}
+
+.btn-small {
+ padding: var(--spacing-xs) var(--spacing-md);
+ font-size: 0.875rem;
+}
+
+/* Cards */
+.card {
+ background-color: var(--bg-primary);
+ border: 1px solid var(--border-color);
+ border-radius: var(--radius-lg);
+ padding: var(--spacing-xl);
+ box-shadow: var(--shadow-sm);
+ transition: all 0.3s ease;
+}
+
+.card:hover {
+ box-shadow: var(--shadow-lg);
+ transform: translateY(-2px);
+}
+
+/* Hero Section */
+.hero {
+ position: relative;
+ min-height: 100vh;
+ display: flex;
+ flex-direction: column;
+ background: linear-gradient(135deg, #667eea 0%, #764ba2 100%);
+ color: white;
+ overflow: hidden;
+}
+
+.hero-background {
+ position: absolute;
+ top: 0;
+ left: 0;
+ right: 0;
+ bottom: 0;
+ background:
+ linear-gradient(45deg, transparent 49%, rgba(255,255,255,0.03) 49%, rgba(255,255,255,0.03) 51%, transparent 51%),
+ linear-gradient(-45deg, transparent 49%, rgba(255,255,255,0.03) 49%, rgba(255,255,255,0.03) 51%, transparent 51%);
+ background-size: 60px 60px;
+ opacity: 0.5;
+}
+
+/* Navigation */
+.navbar {
+ position: relative;
+ z-index: 100;
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ padding: var(--spacing-lg) var(--spacing-xl);
+}
+
+.nav-brand {
+ display: flex;
+ align-items: center;
+ gap: var(--spacing-md);
+}
+
+.nav-brand .logo {
+ height: 40px;
+ width: auto;
+}
+
+.nav-brand h1 {
+ font-size: 1.5rem;
+ margin: 0;
+}
+
+.nav-menu {
+ display: flex;
+ list-style: none;
+ gap: var(--spacing-xl);
+ align-items: center;
+}
+
+.nav-menu a {
+ color: white;
+ font-weight: 500;
+ transition: opacity 0.2s ease;
+}
+
+.nav-menu a:hover {
+ opacity: 0.8;
+}
+
+/* Hero Content */
+.hero-content {
+ position: relative;
+ z-index: 10;
+ flex: 1;
+ display: flex;
+ flex-direction: column;
+ justify-content: center;
+ align-items: center;
+ text-align: center;
+ padding: var(--spacing-2xl);
+}
+
+.hero-badge {
+ display: inline-flex;
+ align-items: center;
+ gap: var(--spacing-sm);
+ padding: var(--spacing-sm) var(--spacing-lg);
+ background-color: rgba(255, 255, 255, 0.2);
+ backdrop-filter: blur(10px);
+ border-radius: 9999px;
+ font-size: 0.875rem;
+ font-weight: 600;
+ margin-bottom: var(--spacing-lg);
+}
+
+.badge-icon {
+ font-size: 1.25rem;
+}
+
+.hero-title {
+ font-size: 3.5rem;
+ font-weight: 800;
+ margin-bottom: var(--spacing-md);
+ line-height: 1.1;
+}
+
+.hero-subtitle {
+ font-size: 1.25rem;
+ font-weight: 400;
+ max-width: 700px;
+ margin-bottom: var(--spacing-2xl);
+ opacity: 0.95;
+}
+
+.hero-buttons {
+ display: flex;
+ gap: var(--spacing-md);
+ margin-bottom: var(--spacing-2xl);
+}
+
+.hero-stats {
+ display: flex;
+ gap: var(--spacing-2xl);
+ margin-top: var(--spacing-2xl);
+}
+
+.stat {
+ display: flex;
+ flex-direction: column;
+ align-items: center;
+}
+
+.stat strong {
+ font-size: 2rem;
+ font-weight: 800;
+}
+
+.stat span {
+ font-size: 0.875rem;
+ opacity: 0.9;
+}
+
+/* Section */
+.section {
+ padding: var(--spacing-2xl) 0;
+}
+
+.section-title {
+ text-align: center;
+ font-size: 2.5rem;
+ margin-bottom: var(--spacing-lg);
+}
+
+.section-intro {
+ text-align: center;
+ font-size: 1.125rem;
+ max-width: 800px;
+ margin: 0 auto var(--spacing-2xl);
+ color: var(--text-secondary);
+}
+
+/* Grid Layouts */
+.features-grid {
+ display: grid;
+ grid-template-columns: repeat(auto-fit, minmax(300px, 1fr));
+ gap: var(--spacing-xl);
+}
+
+.feature-card {
+ background-color: var(--bg-primary);
+ border: 1px solid var(--border-color);
+ border-radius: var(--radius-lg);
+ padding: var(--spacing-xl);
+ text-align: center;
+ transition: all 0.3s ease;
+}
+
+.feature-card:hover {
+ box-shadow: var(--shadow-lg);
+ transform: translateY(-4px);
+ border-color: var(--k-blue);
+}
+
+.feature-icon {
+ font-size: 3rem;
+ margin-bottom: var(--spacing-md);
+}
+
+.feature-card h3 {
+ margin-bottom: var(--spacing-md);
+}
+
+.feature-card p {
+ color: var(--text-secondary);
+ margin-bottom: var(--spacing-lg);
+}
+
+.feature-link {
+ display: inline-block;
+ color: var(--k-blue);
+ font-weight: 600;
+ transition: transform 0.2s ease;
+}
+
+.feature-link:hover {
+ transform: translateX(4px);
+}
+
+/* Code Block */
+.code-block {
+ position: relative;
+ background-color: var(--bg-tertiary);
+ border-radius: var(--radius-md);
+ overflow: hidden;
+ margin: var(--spacing-lg) 0;
+}
+
+.code-block pre {
+ margin: 0;
+ padding: var(--spacing-lg);
+ overflow-x: auto;
+}
+
+.code-block code {
+ font-family: var(--font-mono);
+ font-size: 0.875rem;
+ line-height: 1.6;
+}
+
+.copy-button {
+ position: absolute;
+ top: var(--spacing-sm);
+ right: var(--spacing-sm);
+ padding: var(--spacing-xs) var(--spacing-md);
+ background-color: var(--k-blue);
+ color: white;
+ border: none;
+ border-radius: var(--radius-sm);
+ font-size: 0.75rem;
+ font-weight: 600;
+ cursor: pointer;
+ transition: all 0.2s ease;
+}
+
+.copy-button:hover {
+ background-color: var(--k-dark-blue);
+}
+
+/* Footer */
+.footer {
+ background-color: var(--bg-secondary);
+ border-top: 1px solid var(--border-color);
+ padding: var(--spacing-2xl) 0;
+ margin-top: var(--spacing-2xl);
+}
+
+.footer-grid {
+ display: grid;
+ grid-template-columns: repeat(auto-fit, minmax(200px, 1fr));
+ gap: var(--spacing-xl);
+ margin-bottom: var(--spacing-xl);
+}
+
+.footer-section h4 {
+ margin-bottom: var(--spacing-md);
+}
+
+.footer-section ul {
+ list-style: none;
+}
+
+.footer-section li {
+ margin-bottom: var(--spacing-xs);
+}
+
+.footer-section a {
+ color: var(--text-secondary);
+ transition: color 0.2s ease;
+}
+
+.footer-section a:hover {
+ color: var(--k-blue);
+}
+
+.footer-bottom {
+ text-align: center;
+ padding-top: var(--spacing-xl);
+ border-top: 1px solid var(--border-color);
+ color: var(--text-secondary);
+}
+
+.footer-bottom p {
+ margin-bottom: var(--spacing-xs);
+}
+
+.social-links {
+ display: flex;
+ flex-direction: column;
+ gap: var(--spacing-sm);
+}
+
+.badges {
+ display: flex;
+ gap: var(--spacing-sm);
+ margin-top: var(--spacing-md);
+}
+
+/* Responsive */
+@media (max-width: 768px) {
+ .hero-title {
+ font-size: 2rem;
+ }
+
+ .hero-subtitle {
+ font-size: 1rem;
+ }
+
+ .hero-buttons {
+ flex-direction: column;
+ width: 100%;
+ max-width: 300px;
+ }
+
+ .hero-stats {
+ flex-wrap: wrap;
+ gap: var(--spacing-md);
+ }
+
+ .nav-menu {
+ display: none;
+ }
+
+ .features-grid {
+ grid-template-columns: 1fr;
+ }
+}
diff --git a/demos/formal_semantics_explorer/assets/styles/interactive.css b/demos/formal_semantics_explorer/assets/styles/interactive.css
new file mode 100644
index 000000000..857a60667
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/styles/interactive.css
@@ -0,0 +1,540 @@
+/* Interactive Elements & Animations */
+
+/* Smooth Animations */
+@keyframes fadeIn {
+ from {
+ opacity: 0;
+ transform: translateY(20px);
+ }
+ to {
+ opacity: 1;
+ transform: translateY(0);
+ }
+}
+
+@keyframes slideIn {
+ from {
+ transform: translateX(-100%);
+ }
+ to {
+ transform: translateX(0);
+ }
+}
+
+@keyframes pulse {
+ 0%, 100% {
+ opacity: 1;
+ }
+ 50% {
+ opacity: 0.5;
+ }
+}
+
+@keyframes spin {
+ from {
+ transform: rotate(0deg);
+ }
+ to {
+ transform: rotate(360deg);
+ }
+}
+
+@keyframes bounce {
+ 0%, 100% {
+ transform: translateY(0);
+ }
+ 50% {
+ transform: translateY(-10px);
+ }
+}
+
+/* Tab System */
+.quick-start-tabs {
+ display: flex;
+ gap: var(--spacing-sm);
+ margin-bottom: var(--spacing-lg);
+ border-bottom: 2px solid var(--border-color);
+}
+
+.tab-button {
+ padding: var(--spacing-md) var(--spacing-lg);
+ background: transparent;
+ border: none;
+ border-bottom: 3px solid transparent;
+ font-family: var(--font-sans);
+ font-size: 1rem;
+ font-weight: 600;
+ color: var(--text-secondary);
+ cursor: pointer;
+ transition: all 0.3s ease;
+}
+
+.tab-button:hover {
+ color: var(--k-blue);
+}
+
+.tab-button.active {
+ color: var(--k-blue);
+ border-bottom-color: var(--k-blue);
+}
+
+.tab-content {
+ display: none;
+ animation: fadeIn 0.3s ease;
+}
+
+.tab-content.active {
+ display: block;
+}
+
+/* Learning Path Cards */
+.paths-grid {
+ display: grid;
+ grid-template-columns: repeat(auto-fit, minmax(320px, 1fr));
+ gap: var(--spacing-xl);
+ margin-top: var(--spacing-2xl);
+}
+
+.path-card {
+ background: var(--bg-primary);
+ border: 2px solid var(--border-color);
+ border-radius: var(--radius-lg);
+ padding: var(--spacing-xl);
+ transition: all 0.3s ease;
+ position: relative;
+ overflow: hidden;
+}
+
+.path-card::before {
+ content: '';
+ position: absolute;
+ top: 0;
+ left: 0;
+ right: 0;
+ height: 4px;
+ background: linear-gradient(90deg, var(--k-blue), var(--wasm-purple));
+ transform: scaleX(0);
+ transform-origin: left;
+ transition: transform 0.3s ease;
+}
+
+.path-card:hover {
+ border-color: var(--k-blue);
+ box-shadow: var(--shadow-xl);
+ transform: translateY(-4px);
+}
+
+.path-card:hover::before {
+ transform: scaleX(1);
+}
+
+.path-card.beginner {
+ border-left: 4px solid #10b981;
+}
+
+.path-card.intermediate {
+ border-left: 4px solid #f59e0b;
+}
+
+.path-card.advanced {
+ border-left: 4px solid #ef4444;
+}
+
+.path-header {
+ display: flex;
+ justify-content: space-between;
+ align-items: center;
+ margin-bottom: var(--spacing-md);
+}
+
+.path-level {
+ padding: var(--spacing-xs) var(--spacing-md);
+ border-radius: var(--radius-md);
+ font-size: 0.875rem;
+ font-weight: 600;
+ background-color: var(--bg-secondary);
+}
+
+.path-duration {
+ color: var(--text-secondary);
+ font-size: 0.875rem;
+}
+
+.path-steps {
+ list-style: none;
+ margin: var(--spacing-lg) 0;
+}
+
+.path-steps li {
+ padding: var(--spacing-sm) 0;
+ padding-left: var(--spacing-lg);
+ position: relative;
+}
+
+.path-steps li::before {
+ content: '→';
+ position: absolute;
+ left: 0;
+ color: var(--k-blue);
+ font-weight: bold;
+}
+
+.path-steps li a {
+ color: var(--text-primary);
+ transition: all 0.2s ease;
+}
+
+.path-steps li a:hover {
+ color: var(--k-blue);
+ padding-left: var(--spacing-xs);
+}
+
+.path-goal {
+ margin-top: var(--spacing-lg);
+ padding-top: var(--spacing-lg);
+ border-top: 1px solid var(--border-color);
+ color: var(--text-secondary);
+ font-size: 0.875rem;
+}
+
+/* Tutorials Table */
+.tutorials-table {
+ overflow-x: auto;
+ margin-top: var(--spacing-xl);
+}
+
+.tutorials-table table {
+ width: 100%;
+ border-collapse: collapse;
+ background: var(--bg-primary);
+ border-radius: var(--radius-lg);
+ overflow: hidden;
+}
+
+.tutorials-table th,
+.tutorials-table td {
+ padding: var(--spacing-md) var(--spacing-lg);
+ text-align: left;
+ border-bottom: 1px solid var(--border-color);
+}
+
+.tutorials-table th {
+ background-color: var(--bg-secondary);
+ font-weight: 600;
+ color: var(--text-primary);
+}
+
+.tutorials-table tr:hover {
+ background-color: var(--bg-secondary);
+}
+
+.stars {
+ color: #fbbf24;
+ white-space: nowrap;
+}
+
+/* Gallery Grid */
+.gallery-grid {
+ display: grid;
+ grid-template-columns: repeat(auto-fit, minmax(280px, 1fr));
+ gap: var(--spacing-xl);
+ margin-top: var(--spacing-2xl);
+}
+
+.gallery-item {
+ background: var(--bg-primary);
+ border: 1px solid var(--border-color);
+ border-radius: var(--radius-lg);
+ overflow: hidden;
+ transition: all 0.3s ease;
+}
+
+.gallery-item:hover {
+ box-shadow: var(--shadow-xl);
+ transform: translateY(-8px);
+}
+
+.gallery-image {
+ width: 100%;
+ height: 200px;
+ overflow: hidden;
+ background: var(--bg-secondary);
+}
+
+.gallery-image img {
+ width: 100%;
+ height: 100%;
+ object-fit: cover;
+ transition: transform 0.3s ease;
+}
+
+.gallery-item:hover .gallery-image img {
+ transform: scale(1.05);
+}
+
+.gallery-item h3 {
+ padding: var(--spacing-lg);
+ padding-bottom: var(--spacing-sm);
+}
+
+.gallery-item p {
+ padding: 0 var(--spacing-lg);
+ color: var(--text-secondary);
+ font-size: 0.875rem;
+}
+
+.gallery-item .btn-small {
+ margin: var(--spacing-lg);
+}
+
+/* K Framework Section */
+.k-framework {
+ background: linear-gradient(135deg, #667eea 0%, #764ba2 100%);
+ color: white;
+}
+
+.k-intro {
+ max-width: 800px;
+ margin: 0 auto var(--spacing-2xl);
+ font-size: 1.125rem;
+}
+
+.k-intro ul {
+ list-style: none;
+ padding: 0;
+}
+
+.k-intro li {
+ padding: var(--spacing-sm) 0;
+ padding-left: var(--spacing-lg);
+ position: relative;
+}
+
+.k-intro li::before {
+ content: '✓';
+ position: absolute;
+ left: 0;
+ font-weight: bold;
+}
+
+.k-example {
+ max-width: 900px;
+ margin: 0 auto;
+ background-color: rgba(255, 255, 255, 0.1);
+ backdrop-filter: blur(10px);
+ border-radius: var(--radius-xl);
+ padding: var(--spacing-2xl);
+}
+
+.k-example h3 {
+ margin-bottom: var(--spacing-lg);
+}
+
+.k-code {
+ background-color: rgba(0, 0, 0, 0.3);
+ margin: var(--spacing-lg) 0;
+}
+
+.k-interpretation {
+ display: grid;
+ gap: var(--spacing-md);
+ margin: var(--spacing-xl) 0;
+}
+
+.interpretation-item {
+ padding: var(--spacing-md);
+ background-color: rgba(255, 255, 255, 0.1);
+ border-left: 4px solid rgba(255, 255, 255, 0.5);
+ border-radius: var(--radius-sm);
+}
+
+.interpretation-item strong {
+ display: block;
+ margin-bottom: var(--spacing-xs);
+}
+
+/* Interactive Controls */
+.control-panel {
+ display: flex;
+ gap: var(--spacing-md);
+ padding: var(--spacing-lg);
+ background-color: var(--bg-secondary);
+ border-radius: var(--radius-lg);
+ margin: var(--spacing-lg) 0;
+}
+
+.control-button {
+ display: flex;
+ align-items: center;
+ gap: var(--spacing-xs);
+ padding: var(--spacing-sm) var(--spacing-lg);
+ background-color: var(--k-blue);
+ color: white;
+ border: none;
+ border-radius: var(--radius-md);
+ font-family: var(--font-sans);
+ font-weight: 600;
+ cursor: pointer;
+ transition: all 0.2s ease;
+}
+
+.control-button:hover {
+ background-color: var(--k-dark-blue);
+ transform: scale(1.05);
+}
+
+.control-button:active {
+ transform: scale(0.95);
+}
+
+.control-button:disabled {
+ opacity: 0.5;
+ cursor: not-allowed;
+ transform: none;
+}
+
+/* Progress Indicator */
+.progress-bar {
+ width: 100%;
+ height: 4px;
+ background-color: var(--bg-tertiary);
+ border-radius: 9999px;
+ overflow: hidden;
+}
+
+.progress-fill {
+ height: 100%;
+ background: linear-gradient(90deg, var(--k-blue), var(--wasm-purple));
+ border-radius: 9999px;
+ transition: width 0.3s ease;
+}
+
+/* Loading States */
+.loading {
+ display: inline-block;
+ width: 20px;
+ height: 20px;
+ border: 3px solid rgba(255, 255, 255, 0.3);
+ border-radius: 50%;
+ border-top-color: var(--k-blue);
+ animation: spin 1s linear infinite;
+}
+
+.skeleton {
+ background: linear-gradient(
+ 90deg,
+ var(--bg-tertiary) 25%,
+ var(--bg-secondary) 50%,
+ var(--bg-tertiary) 75%
+ );
+ background-size: 200% 100%;
+ animation: loading 1.5s ease-in-out infinite;
+}
+
+@keyframes loading {
+ 0% {
+ background-position: 200% 0;
+ }
+ 100% {
+ background-position: -200% 0;
+ }
+}
+
+/* Tooltips */
+.tooltip-wrapper {
+ position: relative;
+ display: inline-block;
+}
+
+.tooltip-text {
+ visibility: hidden;
+ position: absolute;
+ z-index: 1000;
+ bottom: 125%;
+ left: 50%;
+ transform: translateX(-50%);
+ padding: var(--spacing-sm) var(--spacing-md);
+ background-color: var(--bg-tertiary);
+ color: var(--text-primary);
+ border-radius: var(--radius-sm);
+ font-size: 0.875rem;
+ white-space: nowrap;
+ box-shadow: var(--shadow-lg);
+ opacity: 0;
+ transition: opacity 0.3s ease;
+}
+
+.tooltip-wrapper:hover .tooltip-text {
+ visibility: visible;
+ opacity: 1;
+}
+
+/* Modal */
+.modal {
+ display: none;
+ position: fixed;
+ z-index: 9999;
+ left: 0;
+ top: 0;
+ width: 100%;
+ height: 100%;
+ background-color: rgba(0, 0, 0, 0.5);
+ animation: fadeIn 0.3s ease;
+}
+
+.modal.active {
+ display: flex;
+ align-items: center;
+ justify-content: center;
+}
+
+.modal-content {
+ background-color: var(--bg-primary);
+ border-radius: var(--radius-xl);
+ padding: var(--spacing-2xl);
+ max-width: 800px;
+ max-height: 90vh;
+ overflow-y: auto;
+ box-shadow: var(--shadow-xl);
+ animation: slideIn 0.3s ease;
+}
+
+.modal-close {
+ float: right;
+ font-size: 2rem;
+ font-weight: bold;
+ color: var(--text-secondary);
+ cursor: pointer;
+ transition: color 0.2s ease;
+}
+
+.modal-close:hover {
+ color: var(--text-primary);
+}
+
+/* Demo Buttons */
+.demo-buttons {
+ display: flex;
+ flex-wrap: wrap;
+ gap: var(--spacing-md);
+ margin-top: var(--spacing-lg);
+}
+
+/* Responsive */
+@media (max-width: 768px) {
+ .paths-grid {
+ grid-template-columns: 1fr;
+ }
+
+ .gallery-grid {
+ grid-template-columns: 1fr;
+ }
+
+ .control-panel {
+ flex-direction: column;
+ }
+
+ .demo-buttons {
+ flex-direction: column;
+ }
+}
diff --git a/demos/formal_semantics_explorer/assets/styles/wasm_syntax_highlight.css b/demos/formal_semantics_explorer/assets/styles/wasm_syntax_highlight.css
new file mode 100644
index 000000000..97e3a5452
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/styles/wasm_syntax_highlight.css
@@ -0,0 +1,311 @@
+/* WebAssembly Syntax Highlighting */
+
+/* Base code styling */
+.language-wasm,
+.language-wat,
+.language-k {
+ font-family: 'Fira Code', 'Courier New', monospace;
+ font-size: 14px;
+ line-height: 1.6;
+}
+
+/* WebAssembly Text Format (WAT) */
+.token.comment {
+ color: #6a9955;
+ font-style: italic;
+}
+
+.token.instruction {
+ color: #569cd6;
+ font-weight: 600;
+}
+
+.token.keyword {
+ color: #c586c0;
+ font-weight: 600;
+}
+
+.token.type {
+ color: #4ec9b0;
+}
+
+.token.number {
+ color: #b5cea8;
+}
+
+.token.string {
+ color: #ce9178;
+}
+
+.token.function {
+ color: #dcdcaa;
+}
+
+.token.operator {
+ color: #d4d4d4;
+}
+
+.token.punctuation {
+ color: #808080;
+}
+
+.token.label {
+ color: #c8c8c8;
+}
+
+/* K Framework Syntax */
+.language-k .token.keyword {
+ color: #569cd6;
+}
+
+.language-k .token.rule-keyword {
+ color: #c586c0;
+}
+
+.language-k .token.cell {
+ color: #4ec9b0;
+}
+
+.language-k .token.variable {
+ color: #9cdcfe;
+}
+
+.language-k .token.sort {
+ color: #4ec9b0;
+}
+
+.language-k .token.builtin {
+ color: #dcdcaa;
+}
+
+.language-k .token.attribute {
+ color: #9cdcfe;
+}
+
+/* Instruction Categories */
+.inst-numeric {
+ color: #569cd6;
+}
+
+.inst-control {
+ color: #c586c0;
+}
+
+.inst-memory {
+ color: #4ec9b0;
+}
+
+.inst-table {
+ color: #dcdcaa;
+}
+
+.inst-reference {
+ color: #ce9178;
+}
+
+.inst-variable {
+ color: #9cdcfe;
+}
+
+/* Type Annotations */
+.type-i32 { color: #4fc1ff; }
+.type-i64 { color: #4fc1ff; }
+.type-f32 { color: #b5cea8; }
+.type-f64 { color: #b5cea8; }
+.type-funcref { color: #ce9178; }
+.type-externref { color: #ce9178; }
+
+/* Semantic Highlighting */
+.semantic-stack {
+ background-color: rgba(79, 193, 255, 0.1);
+ border-left: 3px solid #4fc1ff;
+ padding: 2px 4px;
+}
+
+.semantic-memory {
+ background-color: rgba(78, 201, 176, 0.1);
+ border-left: 3px solid #4ec9b0;
+ padding: 2px 4px;
+}
+
+.semantic-control {
+ background-color: rgba(197, 134, 192, 0.1);
+ border-left: 3px solid #c586c0;
+ padding: 2px 4px;
+}
+
+.semantic-function {
+ background-color: rgba(220, 220, 170, 0.1);
+ border-left: 3px solid #dcdcaa;
+ padding: 2px 4px;
+}
+
+/* Error & Warning Highlighting */
+.error-highlight {
+ background-color: rgba(239, 68, 68, 0.15);
+ border-bottom: 2px wavy #ef4444;
+}
+
+.warning-highlight {
+ background-color: rgba(245, 158, 11, 0.15);
+ border-bottom: 2px wavy #f59e0b;
+}
+
+/* Code Editor Line Numbers */
+.line-numbers {
+ counter-reset: linenumber;
+}
+
+.line-numbers .line::before {
+ counter-increment: linenumber;
+ content: counter(linenumber);
+ display: inline-block;
+ width: 3em;
+ padding-right: 0.5em;
+ margin-right: 0.5em;
+ color: #858585;
+ text-align: right;
+ border-right: 1px solid #404040;
+}
+
+/* Active Line Highlight */
+.active-line {
+ background-color: rgba(255, 255, 255, 0.05);
+ border-left: 3px solid #569cd6;
+}
+
+/* Selection Highlight */
+::selection {
+ background-color: rgba(86, 156, 214, 0.3);
+}
+
+/* Breakpoint Indicator */
+.breakpoint {
+ position: relative;
+}
+
+.breakpoint::before {
+ content: '●';
+ position: absolute;
+ left: -1.5em;
+ color: #ef4444;
+ font-size: 1.2em;
+}
+
+/* Execution Pointer */
+.execution-pointer {
+ position: relative;
+ background-color: rgba(181, 206, 168, 0.15);
+}
+
+.execution-pointer::before {
+ content: '▶';
+ position: absolute;
+ left: -1.5em;
+ color: #10b981;
+ font-size: 0.8em;
+}
+
+/* Hover Tooltips */
+.tooltip {
+ position: relative;
+ cursor: help;
+ border-bottom: 1px dotted #569cd6;
+}
+
+.tooltip .tooltip-content {
+ visibility: hidden;
+ position: absolute;
+ z-index: 1000;
+ bottom: 125%;
+ left: 50%;
+ transform: translateX(-50%);
+ padding: 8px 12px;
+ background-color: #252526;
+ color: #d4d4d4;
+ border: 1px solid #454545;
+ border-radius: 4px;
+ font-size: 12px;
+ white-space: nowrap;
+ box-shadow: 0 4px 6px rgba(0, 0, 0, 0.3);
+}
+
+.tooltip:hover .tooltip-content {
+ visibility: visible;
+}
+
+/* K Rule Visualization */
+.k-rule {
+ background-color: #1e1e1e;
+ border: 1px solid #404040;
+ border-radius: 6px;
+ padding: 16px;
+ margin: 16px 0;
+}
+
+.k-rule-header {
+ color: #569cd6;
+ font-weight: 600;
+ margin-bottom: 8px;
+}
+
+.k-rule-body {
+ font-family: 'Fira Code', monospace;
+ color: #d4d4d4;
+}
+
+.k-cell {
+ color: #4ec9b0;
+ font-weight: 600;
+}
+
+.k-variable {
+ color: #9cdcfe;
+ font-style: italic;
+}
+
+.k-rewrite {
+ color: #c586c0;
+ font-weight: bold;
+}
+
+.k-condition {
+ color: #dcdcaa;
+ font-style: italic;
+}
+
+/* Prism.js Theme Override */
+pre[class*="language-"] {
+ background-color: #1e1e1e;
+ color: #d4d4d4;
+ padding: 1em;
+ margin: 0.5em 0;
+ overflow: auto;
+ border-radius: 6px;
+}
+
+code[class*="language-"] {
+ background: transparent;
+ color: #d4d4d4;
+}
+
+/* Inline code */
+:not(pre) > code {
+ background-color: rgba(110, 118, 129, 0.1);
+ padding: 0.2em 0.4em;
+ border-radius: 3px;
+ font-family: 'Fira Code', monospace;
+ font-size: 0.9em;
+}
+
+/* Dark mode adjustments */
+@media (prefers-color-scheme: dark) {
+ pre[class*="language-"] {
+ background-color: #0d1117;
+ }
+
+ .k-rule {
+ background-color: #0d1117;
+ border-color: #30363d;
+ }
+}
diff --git a/demos/formal_semantics_explorer/assets/wasm_examples/basic/arithmetic.wat b/demos/formal_semantics_explorer/assets/wasm_examples/basic/arithmetic.wat
new file mode 100644
index 000000000..d82b16d40
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/wasm_examples/basic/arithmetic.wat
@@ -0,0 +1,25 @@
+;; Basic arithmetic operations in WebAssembly
+
+;; Simple addition
+(i32.const 5)
+(i32.const 7)
+(i32.add)
+;; Stack: [12]
+
+;; Subtraction
+(i32.const 10)
+(i32.const 3)
+(i32.sub)
+;; Stack: [12, 7]
+
+;; Multiplication
+(i32.const 4)
+(i32.const 5)
+(i32.mul)
+;; Stack: [12, 7, 20]
+
+;; Division
+(i32.const 20)
+(i32.const 4)
+(i32.div_u)
+;; Stack: [12, 7, 20, 5]
diff --git a/demos/formal_semantics_explorer/assets/wasm_examples/basic/control_flow.wat b/demos/formal_semantics_explorer/assets/wasm_examples/basic/control_flow.wat
new file mode 100644
index 000000000..1f4d535f6
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/wasm_examples/basic/control_flow.wat
@@ -0,0 +1,33 @@
+;; Control flow examples
+
+;; Simple if-then-else
+(i32.const 1)
+(if (result i32)
+ (then (i32.const 10))
+ (else (i32.const 20))
+)
+;; Result: 10
+
+;; Nested conditionals
+(i32.const 0)
+(if (result i32)
+ (then
+ (i32.const 5)
+ )
+ (else
+ (i32.const 1)
+ (if (result i32)
+ (then (i32.const 15))
+ (else (i32.const 25))
+ )
+ )
+)
+;; Result: 15
+
+;; Block with branch
+(block $exit (result i32)
+ (i32.const 100)
+ (br $exit)
+ (i32.const 200) ;; unreachable
+)
+;; Result: 100
diff --git a/demos/formal_semantics_explorer/assets/wasm_examples/basic/hello.wat b/demos/formal_semantics_explorer/assets/wasm_examples/basic/hello.wat
new file mode 100644
index 000000000..aa419e9bd
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/wasm_examples/basic/hello.wat
@@ -0,0 +1,7 @@
+;; Hello World - First WebAssembly Semantics Example
+;; This is the simplest possible WebAssembly program
+
+;; Push a constant onto the stack
+(i32.const 42)
+
+;; Result: Stack contains [42]
diff --git a/demos/formal_semantics_explorer/assets/wasm_examples/intermediate/functions.wat b/demos/formal_semantics_explorer/assets/wasm_examples/intermediate/functions.wat
new file mode 100644
index 000000000..f48215f38
--- /dev/null
+++ b/demos/formal_semantics_explorer/assets/wasm_examples/intermediate/functions.wat
@@ -0,0 +1,38 @@
+;; Function definition and calls
+
+(module
+ ;; Simple function that adds two numbers
+ (func $add (param $a i32) (param $b i32) (result i32)
+ local.get $a
+ local.get $b
+ i32.add
+ )
+
+ ;; Function that squares a number
+ (func $square (param $x i32) (result i32)
+ local.get $x
+ local.get $x
+ i32.mul
+ )
+
+ ;; Fibonacci function (recursive)
+ (func $fib (param $n i32) (result i32)
+ (if (result i32)
+ (i32.lt_s (local.get $n) (i32.const 2))
+ (then (local.get $n))
+ (else
+ (i32.add
+ (call $fib
+ (i32.sub (local.get $n) (i32.const 1)))
+ (call $fib
+ (i32.sub (local.get $n) (i32.const 2)))
+ )
+ )
+ )
+ )
+
+ ;; Export functions
+ (export "add" (func $add))
+ (export "square" (func $square))
+ (export "fib" (func $fib))
+)
diff --git a/demos/formal_semantics_explorer/index.html b/demos/formal_semantics_explorer/index.html
new file mode 100644
index 000000000..438fd61b6
--- /dev/null
+++ b/demos/formal_semantics_explorer/index.html
@@ -0,0 +1,519 @@
+
+
+
+
+
+
+
+
+
+
+ `).join('')}
+ Table ${index}
+Type: ${table.type}, Size: ${table.elements.length}
+| Index | +Value | +
|---|---|
| ${i} | +${elem || 'null'} |
+
+
+
+
+ Formal Verification Made Visual
+
+ WebAssembly Formal Semantics Explorer
++ An Interactive Journey Through Formal Verification of WebAssembly using the K Framework +
+ +
+
+
+ 500+
+ K Rules
+
+
+ 180+
+ Instructions
+
+
+ 40+
+ Visualizations
+
+
+ 15
+ Case Studies
+
+
+
+ 🎯 What is This?
++ This is an interactive educational showcase of formally verified WebAssembly semantics + defined in the K Framework. It transforms abstract formal methods into accessible, visual, and engaging content. +
+ +
+
+
+
+
+
+ Visual Execution Traces
+Watch WebAssembly instructions execute step-by-step with animated stack operations
+ Explore → +
+
+
+
+ Interactive Proof Trees
+Explore formal verification derivations with collapsible tree visualizations
+ View → +
+
+
+
+
+
+
+
+
+ Memory Visualizations
+See stack, heap, and linear memory in interactive 3D space
+ Navigate → +
+
+ 🚀 Quick Start
+ +
+
+
+
+
+
+
+
+
+
+
+ # Clone the repository
+git clone https://github.com/AYUSHMIT/wasm-semantics.git
+cd wasm-semantics/demos/formal_semantics_explorer
+
+# Install dependencies (requires K Framework)
+make install-deps
+
+# Launch interactive explorer
+make serve
+# Opens http://localhost:8000 in your browser
+
+# Run example verification
+make verify-example EXAMPLE=memory_safety/bounds_overflow
+
+
+ Try the online demo without any installation:
+ +
+
+
+
+ # Pull Docker image
+docker pull ghcr.io/ayushmit/wasm-semantics:latest
+
+# Run container
+docker run -p 8000:8000 ghcr.io/ayushmit/wasm-semantics:latest
+
+# Open browser to http://localhost:8000
+
+ 📚 Learning Paths
+ +
+
+
+
+
+
+ 🟢 Beginner
+ 2-3 hours
+
+ First Steps in Formal Semantics
+-
+
- What is Formal Semantics? +
- Hello WebAssembly Semantics +
- The Stack Machine Journey +
- WebAssembly Editor +
Goal: Understand how formal semantics describes program behavior
+
+
+
+
+ 🟡 Intermediate
+ 6-8 hours
+
+ Verification Practitioner
+ +Goal: Verify safety properties of WebAssembly programs
+
+
+
+ 🔴 Advanced
+ 2-3 days
+
+ Formal Methods Researcher
+ +Goal: Advance WebAssembly verification state-of-the-art
+
+
+ 🎓 Featured Tutorials
+ +
+
+
+
+
+ | Tutorial | +Complexity | +Time | +Highlights | +Action | +
|---|---|---|---|---|
| Hello Wasm Semantics | +⭐ | +20 min | +First formal execution trace | +Start → | +
| Arithmetic Operations | +⭐⭐ | +45 min | +Interactive stepper, overflow detection | +Start → | +
| Control Flow | +⭐⭐ | +1 hour | +CFG visualization, branch semantics | +Start → | +
| Function Calls | +⭐⭐⭐ | +1.5 hours | +Stack frames, recursion, tail calls | +Start → | +
| Memory Operations | +⭐⭐⭐ | +2 hours | +Memory safety proofs, bounds checking | +Start → | +
| Memory Safety Case Study | +⭐⭐⭐⭐ | +3 hours | +Full verification workflow | +Start → | +
| Compiler Correctness | +⭐⭐⭐⭐⭐ | +4 hours | +Bisimulation, semantic equivalence | +Start → | +
+
+ 🎨 Visualization Gallery
+ +
+
+
+
+
+
+ 
+
+
+ Execution Trace Visualization
+Watch Fibonacci computation execute instruction-by-instruction
+ Explore → +
+
+
+
+ 
+
+
+ Interactive Proof Tree
+Explore formal proof of type soundness with collapsible derivation tree
+ View → +
+
+
+
+ 
+
+
+ 3D Memory Visualizer
+Navigate WebAssembly linear memory in interactive 3D space
+ Navigate → +
+
+
+ 
+
+
+ Semantic Rule Browser
+Browse 500+ K rewrite rules with syntax highlighting and search
+ Browse → +
+
+ 🔬 K Framework Deep Dive
+ +
+
+
+ The K Framework is a rewrite-based executable semantic framework where:
+-
+
- Programming languages are defined as term rewriting systems +
- Execution is rule application on configurations +
- Verification uses reachability logic and symbolic execution +
+
+ Example K Rule:
+
+
+
+ rule <k> (i32.const I1:Int) (i32.const I2:Int) i32.add
+ => i32.const (I1 +Int I2) ... </k>
+ requires I1 +Int I2 <=Int (2 ^Int 32 -Int 1)
+
+
+
+ Try Interactive Rule Applier
+
+
+ Left side: Pattern to match (two i32 constants on stack, then add instruction)
+
+
+ Right side: Result (single i32 constant with sum)
+
+
+ Requires: Side condition (no overflow)
+
+