---
title: "Mechanising and Verifying the WebAssembly Specification (2018)"
description: "WebAssembly is a low-level bytecode language supported by all major browsers and intended as a… 31 references, cited by 8 papers here."
authors: ["Conrad Watt"]
year: 2018
venue: "CPP 2018"
source: "https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf"
licence: "author's copy — read only"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/watt-2018-mechanising-verifying-webassembly-specification/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/watt-2018-mechanising-verifying-webassembly-specification/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2018](https://md.research.elamur.ai/free/en/papers/2018/page/5/) / Mechanising and Verifying the WebAssembly Specification

# Mechanising and Verifying the WebAssembly Specification

**Authors:** Conrad Watt · **Year:** 2018 · **Venue:** [CPP 2018](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/) ([CPP 2018](https://md.research.elamur.ai/free/en/venues/acm-sigplan-international-conference-on-certified-programs-and-proofs-cpp/2018/)) · **Licence:** author's copy — read only

**Links:** [Publisher's page](https://doi.org/10.1145/3167082) · [PDF](https://www.cl.cam.ac.uk/~caw77/papers/mechanising-and-verifying-the-webassembly-specification.pdf) · [OpenAlex](https://openalex.org/W2778960843)

**Citations:** 66 citations (OpenAlex, 2026-10-14) · 8 in our library, of the 149,439 papers whose bibliographies we read

## Summary
WebAssembly is a low-level bytecode language supported by all major browsers and intended as a universal compilation target for the web. Its designers wrote a formal semantics on paper, but that semantics had never been mechanised, and its claimed type-soundness properties had never been proven. Watt formalises WebAssembly's central type system and the rules governing how its programs execute in the Isabelle proof assistant. Building on this model, he machine-checks the soundness of the type system and develops a separately verified executable interpreter and type checker. The official OCaml reference interpreter supplies parsing and linking. Constructing the proof exposed several flaws in the official specification. Some made the type system unsound, including a problem in how modules interact with the host environment. The specification authors corrected these flaws. The interpreter was then validated against the official conformance tests and through differential fuzzing against commercial engines. According to the paper, this is the first mechanised formalisation of the full core language and the first complete soundness proof. It demonstrates that deep mechanised verification can directly improve an industrial language standard.

## Key points
- The development contains about 11,000 lines of Isabelle code, of which about 700 lines specify the language itself. It is publicly released under a BSD-style license.
- The specification defines 171 concrete opcodes, which map onto the 28 abstract operations used in Haas et al. (2017).
- Soundness bugs found during the proof, including one in the host-environment interface, were fixed in the official WebAssembly specification.
- The verified interpreter passes all core conformance tests in the WebAssembly repository.
- Differential fuzzing used CSmith and the Binaryen toolchain. It found no bugs in commercial engines, but it uncovered a crash in Binaryen, which was then fixed. The project structure follows the approach of JSCert.

*Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.*

## Institutions

- [University of Cambridge](https://md.research.elamur.ai/free/en/universities/university-of-cambridge/) — University, Cambridge, United Kingdom · 287 works · 125,174 citations

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

## Cite

Cite as: Conrad Watt. 2018. Mechanising and Verifying the WebAssembly Specification. CPP 2018.

The paper itself, not this page. BibTeX from the library's record of the work.

```bibtex
@inproceedings{watt2018mechanising,
  title = {{Mechanising and Verifying the WebAssembly Specification}},
  author = {Conrad Watt},
  booktitle = {CPP 2018},
  year = {2018},
  doi = {10.1145/3167082},
  url = {https://doi.org/10.1145/3167082}
}
```

- [← previous Stance Detection in Fake News A Combined Feature Representation](https://md.research.elamur.ai/free/en/papers/ghanem-2018-stance-detection-fake-news-combined/)
- [next → NTUA-SLP at SemEval-2018 Task 3: Tracking Ironic Tweets using Ensembles of Word and Character Level Attentive RNNs](https://md.research.elamur.ai/free/en/papers/baziotis-2018-ntua-slp-semeval-2018-task-s18-1100/)
- [↑ back to papers of 2018](https://md.research.elamur.ai/free/en/papers/2018/page/5/)

## References

31 references, 1 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

1. Mark Batty, Kayvan Memarian, Kyndylan Nienhuis, Jean Pichon-Pharabod, and Peter Sewell. 2015. The Problem of Programming Language Concurrency Semantics. Springer Berlin Heidelberg, Berlin, Heidelberg, 283–307. https://doi.org/10.1007/978-3-662-46669-8_12 — [doi:10.1007/978-3-662-46669-8_12](https://doi.org/10.1007/978-3-662-46669-8_12) [↗](https://doi.org/10.1007/978-3-662-46669-8_12)
2. Martin Bodin, Arthur Chargueraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt, and Gareth Smith. 2014. A Trusted Mechanised JavaScript Specification. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). A… — [doi:10.1145/2535838.2535876](https://doi.org/10.1145/2535838.2535876) [find](https://scholar.google.com/scholar?q=Martin+Bodin%2C+Arthur+Chargueraud%2C+Daniele+Filaretti%2C+Philippa+Gardner%2C+Sergio+Maffeis%2C+Daiva+Naudziuniene%2C+Alan+Schmitt%2C+and+Gareth+Smith%2E+2014%2E+A+Trusted+Mechanised+JavaScript+Specification%2E+In+Proce)
3. CakeML Projects. (2017). Retrieved October 7, 2017 from [https://cakeml.org/projects](https://cakeml.org/projects) [↗](https://cakeml.org/projects)
4. Ethereum Group. 2017. eWASM. (2017). Retrieved October 7, 2017 from [https://github.com/ewasm](https://github.com/ewasm) [↗](https://github.com/ewasm)
5. Google. 2017. Welcome to Native Client. (2017). Retrieved October 7, 2017 from [https://developer.chrome.com/native-client](https://developer.chrome.com/native-client) Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017a. Bringing the Web Up to Speed with Web… [↗](https://developer.chrome.com/native-client)
6. Andreas Haas, Andreas Rossberg, Derek L. Schuff, Ben L. Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai, and JF Bastien. 2017b. Bringing the Web Up to Speed with WebAssembly. (March 2017). Retrieved October 7, 2017 from [https://github.com/WebAssembly/spec/blob/bbb26c42b62096baff860897675…](https://github.com/WebAssembly/spec/blob/bbb26c42b62096baff860897675…) [↗](https://github.com/WebAssembly/spec/blob/bbb26c42b62096baff860897675…)
7. David Herman, Luke Wagner, and Alon Zakai. 2014. asm.js. (August 2014). Retrieved October 7, 2017 from [http://asmjs.org/spec/latest](http://asmjs.org/spec/latest) Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In 1st Workshop on Trusted Smart Contracts. [↗](http://asmjs.org/spec/latest)
8. Gerwin Klein and Tobias Nipkow. 2006. A Machine-checked Model for a Java-like Language, Virtual Machine, and Compiler. ACM Trans. Program. Lang. Syst. 28, 4 (July 2006), 619–695. https://doi.org/10.1145/1146809.1146811 — [doi:10.1145/1146809.1146811](https://doi.org/10.1145/1146809.1146811) [↗](https://doi.org/10.1145/1146809.1146811)
9. Peter J Knaggs. 1993. Towards a Formal Forth. (September 1993). Retrieved October 7, 2017 from [http://www.rigwit.co.uk/papers/formal2.pdf](http://www.rigwit.co.uk/papers/formal2.pdf) Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML. In Proceedings of the 41st ACM SIGPLAN-SIGACT Sy… — [doi:10.1145/2535838.2535841](https://doi.org/10.1145/2535838.2535841) [↗](http://www.rigwit.co.uk/papers/formal2.pdf)
10. Andreas Lochbihler and Lukas Bulwahn. 2011. Animating the Formalised Semantics of a Java-like Language. In Proceedings of the Second International Conference on Interactive Theorem Proving (ITP’11). Springer-Verlag, Berlin, Heidelberg, 216–232. [http://dl.acm.org/citation.cfm?id=2033939.2033958](http://dl.acm.org/citation.cfm?id=2033939.2033958) [↗](http://dl.acm.org/citation.cfm?id=2033939.2033958)
11. Jaanus Poial. 1990. Algebraic Specification of Stack Effects for Forth Programs. In Forml Conference Proceedings (Forml 1990). The Forth Interest Group, San Jose, CA, USA, 282– 290. [find](https://scholar.google.com/scholar?q=Jaanus+Poial%2E+1990%2E+Algebraic+Specification+of+Stack+Effects+for+Forth+Programs%2E+In+Forml+Conference+Proceedings+%28Forml+1990%29%2E+The+Forth+Interest+Group%2C+San+Jose%2C+CA%2C+USA%2C+282%E2%80%93+290%2E)
12. Jaanus Poial. 2002. Stack effect calculus with typed wildcards, polymorphism and inheritance. In Proc. 18-th EuroForth Conference. [find](https://scholar.google.com/scholar?q=Jaanus+Poial%2E+2002%2E+Stack+effect+calculus+with+typed+wildcards%2C+polymorphism+and+inheritance%2E+In+Proc%2E+18%2Dth+EuroForth+Conference%2E)
13. James F. Power and David Sinclair. 2004. A Formal Model of Forth Control Words in the Pi-Calculus. J. UCS 10, 9 (2004), 1272–1293. https://doi.org/10.3217/jucs-010-09-1272 — [doi:10.3217/jucs-010-09-1272](https://doi.org/10.3217/jucs-010-09-1272) [↗](https://doi.org/10.3217/jucs-010-09-1272)
14. Andreas Rossberg. 2017a. [spec] Fix and clean up invariants for host functions. (September 2017). Retrieved October 7, 2017 from [https://github.com/WebAssembly/spec/pull/563](https://github.com/WebAssembly/spec/pull/563) [↗](https://github.com/WebAssembly/spec/pull/563)
15. Andreas Rossberg. 2017b. [spec] Fix and clean up invariants for host functions. (September 2017). Retrieved October 7, 2017 from [https://github.com/WebAssembly/spec/commit/772d87705ea4786c0d44d41902097e91cf31f82b](https://github.com/WebAssembly/spec/commit/772d87705ea4786c0d44d41902097e91cf31f82b) [↗](https://github.com/WebAssembly/spec/commit/772d87705ea4786c0d44d41902097e91cf31f82b)
16. Andreas Rossberg. 2017c. [spec] Fix and clean up invariants for host functions. (September 2017). Retrieved October 7, 2017 from [https://github.com/WebAssembly/spec/pull/563](https://github.com/WebAssembly/spec/pull/563) [↗](https://github.com/WebAssembly/spec/pull/563)
17. TC39. 2017a. Memory Model. (September 2017). Retrieved October 7, 2017 from [https://tc39.github.io/ecma262/\#sec-memory-model](https://tc39.github.io/ecma262/\#sec-memory-model) [↗](https://tc39.github.io/ecma262/\#sec-memory-model)
18. TC39. 2017b. SIMD.js specification v0.9. (April 2017). Retrieved October 7, 2017 from [http://tc39.github.io/ecmascript_simd/](http://tc39.github.io/ecmascript_simd/) [↗](http://tc39.github.io/ecmascript_simd/)
19. Conrad Watt. 2017a. Conrad Watt. (October 2017). Retrieved November 27, 2017 from [http://www.cl.cam.ac.uk/~caw77/](http://www.cl.cam.ac.uk/~caw77/) [↗](http://www.cl.cam.ac.uk/~caw77/)
20. Conrad Watt. 2017b. Crash in wasm-opt on certain optimisation levels. (August 2017). Retrieved October 7, 2017 from [https://github.com/WebAssembly/binaryen/issues/1149](https://github.com/WebAssembly/binaryen/issues/1149) [↗](https://github.com/WebAssembly/binaryen/issues/1149)
21. WebAssembly Community Group. 2017a. [find](https://scholar.google.com/scholar?q=WebAssembly+Community+Group%2E+2017a%2E)
22. Binaryen. (October 2017). Retrieved October 7, 2017 from [https://github.com/](https://github.com/) [↗](https://github.com/)
23. WebAssembly/binaryen WebAssembly Community Group. 2017b. [find](https://scholar.google.com/scholar?q=WebAssembly%2Fbinaryen+WebAssembly+Community+Group%2E+2017b%2E)
24. Instructions. (September 2017). Retrieved October 7, 2017 from [https://webassembly.github.io/spec/binary/instructions.html](https://webassembly.github.io/spec/binary/instructions.html) WebAssembly Community Group. 2017c. [↗](https://webassembly.github.io/spec/binary/instructions.html)
25. WebAssembly. (2017). Retrieved October 7, 2017 from [http://webassembly.org](http://webassembly.org) WebAssembly Community Group. 2017d. [↗](http://webassembly.org)
26. WebAssembly. (October 2017). Retrieved October 7, 2017 from [https://github.com/WebAssembly/spec/tree/master/interpreter](https://github.com/WebAssembly/spec/tree/master/interpreter) [↗](https://github.com/WebAssembly/spec/tree/master/interpreter)
27. WebAssembly Community Group. 2017e. [find](https://scholar.google.com/scholar?q=WebAssembly+Community+Group%2E+2017e%2E)
28. WebAssembly. (October 2017). Retrieved October 7, 2017 from [https://github.com/WebAssembly](https://github.com/WebAssembly) WebAssembly Community Group. 2017f. [↗](https://github.com/WebAssembly)
29. WebAssembly Specification. (September 2017). Retrieved October 7, 2017 from [https://webassembly.github.io/spec/](https://webassembly.github.io/spec/) [↗](https://webassembly.github.io/spec/)
30. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. [Finding and Understanding Bugs in C Compilers](https://md.research.elamur.ai/free/en/papers/yang-2011-finding-understanding-bugs-c-compilers/). In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’11). ACM, New York, NY, USA, 283–294. https://doi.org/10.1145/1993498.1993532 [↗](https://doi.org/10.1145/1993498.1993532)
31. Alon Zakai and Robert Nyman. 2013. Gap between asm.js and native performance gets even narrower with float32 optimizations. (December 2013). Retrieved October 7, 2017 from [https://hacks.mozilla.org/2013/12/20/](https://hacks.mozilla.org/2013/12/20/) [↗](https://hacks.mozilla.org/2013/12/20/)

*Updated 3 November 2026*