Formal verification is a powerful way to ensure software correctness, but traditional methods can be manual, niche, and costly. Deductive proofs using systems like Rocq or Lean are mathematically rigorous but slow and labor-intensive. Static analysis tools, like Astrée or MOPSA, automate checks but often produce many false positives.
Symbolic execution offers a middle ground: it automatically finds bugs by exploring program behavior, while giving concrete counterexamples, though it may miss some paths. The challenge was to make symbolic execution accessible and practical for modern development workflows.
Titagone developed Owi as part of our mission to make formal methods accessible and practical for real-world development. Leveraging our expertise in symbolic execution, WebAssembly, and program verification, we saw an opportunity to create a modern alternative to aging tools like KLEE. Our research background in formal methods and our experience with cross-language verification positioned us uniquely to build a symbolic execution engine that would be actively maintained, standards-based, and easy to use, bridging the gap between academic research tools and practical software development.
Developed by Titagone, Owi is a symbolic execution engine designed to work seamlessly with WebAssembly (Wasm), a standardized, low-level, deterministic language that is easy to verify and widely supported. Owi can handle code compiled from C, C++, or Rust, bridging multiple languages with a single, unified interface.
Owi works by building a complete model of program behavior in Wasm, then executing it symbolically through an ergonomic web interface. When a potential bug is detected, Owi produces a detailed failure report, leveraging SMT solvers like Z3 or Alt-Ergo.
Unlike KLEE (the main competitor which relies on LLVM and suffers from maintenance and compatibility issues), Owi is actively maintained, supports Wasm, and offers comparable performance, making it more adaptable to modern development workflows.
Beyond raw performance, Owi makes symbolic execution accessible and practical. It provides a smooth interface for generating tests, visualizing program behavior, and exploring edge cases, all in a web-based, interactive environment. By combining modern standards (Wasm), symbolic execution, and usability, Owi empowers developers and verification engineers to find bugs faster, understand program behavior, and increase software reliability. In short, Owi is not just a symbolic engine: it's a bridge between languages, a tool for exploration, and a platform for learning, making formal methods more approachable while maintaining industrial-grade rigor.
Let's discuss how symbolic execution can improve your software reliability and development workflow.
Get in Touch