Welcome to Owi

Owi is an open-source framework for advanced WebAssembly analysis and manipulation, with a focus on practical symbolic execution and robust tooling. It is designed for researchers, engineers, programming language enthusiasts and practitioners requiring precise, flexible, and extensible support program reasoning.

Owi provides three primary components:

🔬 Symbolic Execution Engine for Wasm, C, C++, Rust, and Zig

Owi includes a cross-language symbolic execution engine supporting:

• Automated testing, bug finding and pentesting through symbolic testing and constraint solving;
• Solver-aided programming for problem solving and synthesis tasks;
• Test case generation aligned with advanced coverage criteria;
• Formal verification: prove properties or find counterexamples in real-world programs.

The engine is designed for precision, scalability, interoperability across languages, and extensibility toward both experimental and applied verification use-cases. It offers a practical path from fuzzing to formal proofs.

🔧 The Wasm Swiss Army Knife

Owi offers a set of practical tools for Wasm development and analysis:

• Formatter and optimizer for Wasm modules;
• Interpreter for .wasm, .wat, and even Wasm scripts (.wast) files that are used in the reference test suite;
• Specification-compliant validator;
• Bidirectional translation between binary (.wasm) and text (.wat) formats;
• Randomized fuzzer generating valid (well-typed) Wasm modules.

These tools aim to support everyday development tasks as well as research on program analysis, fuzzing, and program transformation.

🐪 Native OCaml Library for Wasm Integration

Owi is written in OCaml, thus it also provides a library for:

• Embedding Wasm modules into OCaml applications;
• Importing OCaml functions into Wasm modules with full type safety.

This allows for tightly integrating Wasm-based computation within OCaml-based systems while maintaining strong type guarantees.

⚠️ Warning

For now, the optimizer and the formatter are quite experimental. The optimizer is well tested but only performs basic optimizations in an inefficient way. The formatter is mainly used for debugging purpose and is probably incorrect on some cases. Moreover, the concolic mode is currently broken, use the symbolic one.

🧑‍🎓Want to join us?

We are looking for interns, have a look at the internship labeled issues.