feat: enable Idris2/Zig tooling and add proven integration docs

Changes:
- Enable idris2 0.7.0 in .tool-versions (for ABI with formal proofs)
- Enable zig 0.13.0 in .tool-versions (for FFI implementation)
- Add PROVEN.md documenting integration with proven library
- Sets up formal verification infrastructure

proven provides mathematically proven safe operations via Idris2.

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

Author: Test

.tool-versions

@@ -7,8 +7,8 @@ rust 1.84.0
 # Deno (NO Node.js/npm per language policy)
 deno 2.1.4
 
-# Optional: Idris2 for ABI work
-# idris2 0.7.0
+# Idris2 for ABI with formal proofs
+idris2 0.7.0
 
-# Optional: Zig for FFI work
-# zig 0.13.0
+# Zig for FFI implementation
+zig 0.13.0

PROVEN.md

@@ -0,0 +1,87 @@
+# Proven Integration
+
+WokeLang uses [proven](https://github.com/hyperpolymath/proven) for formally verified operations where safety is critical.
+
+## What is proven?
+
+proven is an Idris2 library providing mathematically proven safe operations:
+- **Cannot crash** - Dependent types prove correctness
+- **Totality checking** - All code paths guaranteed to terminate
+- **90+ modules** - Comprehensive formally verified functionality
+- **89 language bindings** - FFI via Zig C ABI
+
+## Architecture
+
+```
+WokeLang (Rust)
+      ↓
+Rust Bindings
+      ↓
+Zig FFI Bridge
+      ↓
+Idris2 proven Library ← MATHEMATICAL PROOFS
+```
+
+## Integration Points
+
+### Current
+
+WokeLang currently uses proven for:
+- (To be determined based on safety-critical needs)
+
+### Planned
+
+Potential proven integration for:
+- **File I/O** - Proven-safe file operations with capability checks
+- **String operations** - Bounds-checked string manipulation
+- **Collection operations** - Verified data structure operations
+- **Parser combinators** - Provably correct parsing
+
+## Using proven in WokeLang
+
+### Setup
+
+1. Ensure Idris2 is installed (see `.tool-versions`)
+2. Clone proven:
+   ```bash
+   git clone https://github.com/hyperpolymath/proven
+   cd proven
+   make install
+   ```
+
+3. Link WokeLang to proven bindings:
+   ```bash
+   cd wokelang
+   # Add proven-rust bindings to Cargo.toml
+   ```
+
+### Example
+
+```rust
+// Use proven-safe string operations
+use proven_rust::string::SafeString;
+
+let s = SafeString::new("Hello").unwrap();
+let sub = s.substring(0, 5); // Mathematically proven not to panic
+```
+
+## Badge
+
+When WokeLang uses proven modules, add the "Idris Inside" badge to README:
+
+```adoc
+image:https://img.shields.io/badge/Idris-Inside-blueviolet?style=flat[Idris Inside]
+```
+
+## Performance Note
+
+proven adds FFI overhead for maximum safety. Use for:
+- ✓ Safety-critical operations (file I/O, parsing user input)
+- ✓ Security boundaries (capability checks, permission validation)
+- ✗ Hot loops or performance-critical paths
+
+## References
+
+- proven repo: https://github.com/hyperpolymath/proven
+- Idris2 docs: https://idris2.readthedocs.io
+- Zig FFI: /var/mnt/eclipse/repos/proven/ffi/zig/