diff --git a/example/weasel/grammar.ebnf b/example/weasel/grammar.ebnf
new file mode 100644
index 000000000..6e101461a
--- /dev/null
+++ b/example/weasel/grammar.ebnf
@@ -0,0 +1,150 @@
+(*
+    In the grammar below, the following notations are adopted:
+        - The nonterminal symbol `u32` denotes 32-bit unsigned integers.
+        - The nonterminal symbol `integer` denotes arbitrary-precision mathematical integers.
+*)
+
+idchar =
+    "0" | ... | "9"
+  | "A" | ... | "Z"
+  | "a" | ... | "z"
+  | "!" | "#" | "$" | "%" | "&" | "'" | "*" | "+" | "-" | "." | "/"
+  | ":" | "<" | "=" | ">" | "?" | "@" | "\" | "^" | "_" | "`" | "|" | "~" ;
+
+id =
+  idchar , { idchar } ;
+
+ind =
+    "$" , id
+  | u32 ;
+
+wasm_int_type =
+    "i32"
+  | "i64" ;
+
+wasm_float_type =
+    "f32"
+  | "f64" ;
+
+wasm_type =
+    wasm_int_type
+  | wasm_float_type ;
+
+num_type =
+    wasm_type
+  | "integer"
+
+ref_type =
+    "funcref"
+  | "externref" ;
+
+unop =
+    "clz"             (on wasm_int_type)
+  | "ctz"             (on wasm_int_type)
+  | "popcnt"          (on wasm_int_type)
+  | "abs"
+  | "neg"
+  | "sqrt"
+  | "ceil"
+  | "floor"
+  | "trunc"           (on wasm_float_type)
+  | "nearest" ;       (on wasm_float_type)
+
+binop =
+    "add" | "+"
+  | "sub" | "-"
+  | "mul" | "*"
+  | "div" | "/"
+  | "rem" | "%"       (on wasm_int_type or integer)
+  | "min"
+  | "max"
+  | "and" | "&"       (on wasm_int_type or integer)
+  | "or" | "|"        (on wasm_int_type or integer)
+  | "xor" | "^"       (on wasm_int_type or integer)
+  | "shl" | "<<"      (on wasm_int_type or integer)
+  | "shr_s" | ">>"    (on wasm_int_type or integer)
+  | "shr_x" | ">>>"   (on wasm_int_type or integer)
+  | "rotl"            (on wasm_int_type)
+  | "rotr" ;          (on wasm_int_type)
+
+memarg =
+  "(" , "base" , term , ")" ,
+  [ "(" , "offset" , term , ")" ] ,
+  [ "(" , "align" , term , ")" ] ;
+
+term =
+    "result"
+  | "i32_max"
+  | "i32_min"
+  | "i64_max"
+  | "i64_min"
+  | integer
+  | id
+  | pterm ;
+
+pterm =
+    "result" , [ u32 ]
+  | "old" , term
+  | "param" , ind
+  | "global" , ind
+  | "binder" , ind
+  | unop , term
+  | binop , term , term
+  | "ref_null" , ref_type
+  | "ref_func" , ind
+  | "table_get" , ind
+  | "table_size" , ind
+  | "i32_load" , memarg
+  | "i64_load" , memarg
+  | "f32_load" , memarg
+  | "f64_load" , memarg
+  | "memory_size" , ind
+  | "cond" , prop , term , term
+  | "let" , num_type , [ id ] , term , term
+  | "cast" , num_type , term
+  | "call" , ind , { term } ;
+
+unpred =
+    "eqz"
+  | "is_null" ;       (on ref_type)
+
+binpred =
+    "eq" | "="
+  | "ne" | "!="
+  | "lt" | "<"
+  | "gt" | ">"
+  | "le" | "<="
+  | "ge" | ">=" ;
+
+prop =
+    "true"
+  | "false"
+  | "(" , pprop , ")" ;
+
+pprop =
+    "old" , prop
+  | "!" , prop
+  | "&&" , prop , prop
+  | "||" , prop , prop
+  | "^^" , prop , prop
+  | "==>" , prop , prop
+  | "<==>" , prop , prop
+  | "cond" , prop , prop , prop
+  | "let" , num_type , [ id ] , term , prop
+  | unpred , term
+  | binpred , term , term
+  | ("forall" | "∀") , num_type , [ id ] , prop
+  | ("exists" | "∃") , num_type , [ id ] , prop
+  | "call" , ind , { term } ; (the function must return an i32)
+
+requires_clause = "(" , "requires" , prop , ")" ;
+
+assigns_clause = "(" , "assigns" , ( "nothing" | memarg ) , ")" ;
+
+ensures_clause = "(" , "ensures" , prop , ")" ;
+
+simple_behavior = { requires_clause | assigns_clause | ensures_clause } ;
+
+contract = "(@contract" , ind , [ "pure" ] , simple_behavior , ")" ;
+
+annotation = contract ;
diff --git a/example/weasel/ill_formed.wat b/example/weasel/ill_formed.wat
new file mode 100644
index 000000000..058978564
--- /dev/null
+++ b/example/weasel/ill_formed.wat
@@ -0,0 +1,7 @@
+(module
+  (@contract $f
+    owi
+    (ensures true)
+  )
+  (func $f)
+)
diff --git a/example/weasel/language design.md b/example/weasel/language design.md
new file mode 100644
index 000000000..ec46c7252
--- /dev/null
+++ b/example/weasel/language design.md	
@@ -0,0 +1,46 @@
+# Weasel: WebAssembly Specification Language
+
+## Custom Annotations
+
+Weasel specifications are written directly in WebAssembly's text format as [custom annotations](https://webassembly.github.io/annotations/core/text/lexical.html#annotations). Compared to comments, embedding specifications in custom annotations provides the benefit of syntax highlighting, while keeping the source file compatable with the WebAssembly specification.
+
+Custom annotations take the form `(@annotid content)`, where there is no space between `(@` and `annotid`. `annotid` could either be a sequence of characters or a double-quoted string, and `content` should be well-parenthesized. It is possible to have nested custom annotations.
+
+## Parser Behavior
+
+Custom annotations may appear anywhere inside WebAssembly text format files where spaces are allowed. They do not interfere with the semantics of WebAssembly, and parsers are free to discard custom annotations.
+
+For applications where certain custom annotations carry specific meanings, additional grammatical restrictions may be imposed on the content of custom annotations. Their behavior in case of an error are implementation-defined. For example, Owi's implementation of Weasel emits a syntax error when encountering an ill-formed function contract.
+
+<!-- $MDX file=ill_formed.wat -->
+```wat
+(module
+  (@contract $f
+    owi
+    (ensures true)
+  )
+  (func $f)
+)
+```
+
+```sh
+$ owi instrument ill_formed.wat
+unknown annotation clause owi
+```
+
+## Type of Annotation
+
+In Weasel, `annotid` specifies the type of annotation. Different types of annotations follow slightly different grammatical rules and must appear in specific locations of the source code. Currently, Weasel define only one type of annotation:
+
+- **function contract** should appear anywhere a module field is allowed (i.e. as a custom section). Though it is recommended to place the contract immediately before the corresponding function definition.
+
+## Grammar
+
+Weasel adopts an S-expression-like syntax for the time being, mainly because it is easy to prototype. The syntax may evolve in the future (to an infix one, possibly).
+
+The grammar of Weasel annotations is specified [here](grammar.ebnf) in [EBNF-ISO form](https://en.wikipedia.org/wiki/Extended_Backus%E2%80%93Naur_form#Table_of_symbols).
+
+## Future works
+
+- big number
+- specification of loop invariant