diff --git a/tests/web3/firefly_getCoverageData0.expected.json b/tests/web3/firefly_getCoverageData0.expected.json
new file mode 100644
index 0000000000..b58e545cbd
--- /dev/null
+++ b/tests/web3/firefly_getCoverageData0.expected.json
@@ -0,0 +1 @@
+[{"jsonrpc":"2.0","id":1,"result":true},{"jsonrpc":"2.0","id":2,"result":true},{"jsonrpc":"2.0","id":3,"result":"0x0000000000000000000000000000000000000000000000000000000000ffffff"},{"jsonrpc":"2.0","id":3,"result":{"coverages":[{"93758614234106549757282766802448384239213770766359592192750614820519184033004":{"RUNTIME":100}}],"coveredOpcodes":[{"93758614234106549757282766802448384239213770766359592192750614820519184033004":{"RUNTIME":[0,4,6,7,9,11]}}],"programs":[{"93758614234106549757282766802448384239213770766359592192750614820519184033004":{"RUNTIME":[0,4,6,7,9,11]}}]}}]
\ No newline at end of file
diff --git a/tests/web3/firefly_getCoverageData0.in.json b/tests/web3/firefly_getCoverageData0.in.json
new file mode 100644
index 0000000000..187542c6f1
--- /dev/null
+++ b/tests/web3/firefly_getCoverageData0.in.json
@@ -0,0 +1,42 @@
+[
+    {
+        "jsonrpc": "2.0",
+        "id": 1,
+        "method": "firefly_addAccount",
+        "params": [
+            {
+                "key": "0x5fffe36d0218b8b8d45d4e70788096a5e0c289cf89c907f97d1cdecdccaa8b6b",
+                "balance": "0x56BC75E2D63100000"
+            }
+        ]
+    },
+    {
+        "jsonrpc": "2.0",
+        "id": 2,
+        "method": "firefly_addAccount",
+        "params": [
+            {
+                "address": "0xdf1db454e4dc226da2b0f8d471976180555355e2",
+                "code": "0x62FFFFFF60005260206000F3"
+            }
+        ]
+    },
+    {
+        "jsonrpc": "2.0",
+        "id": 3,
+        "method": "eth_call",
+        "params": [
+            {
+                "from": "0xee70809B448816B3D2D40C1DB8B44aACf50BAD3a",
+                "to": "0xdf1db454e4dc226da2b0f8d471976180555355e2"
+            },
+            "latest"
+        ]
+    },
+    {
+        "jsonrpc": "2.0",
+        "id": 3,
+        "method": "firefly_getCoverageData",
+        "params": []
+    }
+]
\ No newline at end of file
diff --git a/web3.md b/web3.md
index af2b6bd659..51923dd356 100644
--- a/web3.md
+++ b/web3.md
@@ -315,6 +315,8 @@ WEB3 JSON RPC
          <method> "eth_call" </method>
     rule <k> #runRPCCall => #eth_estimateGas ... </k>
          <method> "eth_estimateGas" </method>
+    rule <k> #runRPCCall => #firefly_getCoverageData ... </k>
+         <method> "firefly_getCoverageData" </method>
 
     rule <k> #runRPCCall => #sendResponse( "error": {"code": -32601, "message": "Method not found"} ) ... </k> [owise]
 
@@ -1072,6 +1074,10 @@ Collecting Coverage Data
 - `<opcodeLists>` cell is a map similar to `<opcodeCoverage>` which stores instead a list containing all the `OpcodeItem`s of the executed bytecode for each contract.
 - `OpcodeItem` is a tuple which contains the Program Counter and the Opcode name.
 
+**TODO**: instead of having both `#serializeCoverage` and `#serializePrograms` we could keep only the first rule as `#serializeCoverageMap` if `<opcodeLists>` would store `Sets` instead of `Lists`.
+**TODO**: compute coverage percentages in `Float` instead of `Int`
+**TODO**: `Set2List` won't return `ListItems` in order, causing tests to fail.
+
 ```k
     syntax Phase ::= ".Phase"
                    | "CONSTRUCTOR"
@@ -1126,5 +1132,69 @@ Collecting Coverage Data
       requires notBool PCOUNT in PCS
       [priority(25)]
 
+    syntax KItem ::= "#firefly_getCoverageData"
+ // -------------------------------------------
+    rule <k> #firefly_getCoverageData => #sendResponse ("result": #makeCoverageReport(COVERAGE, PGMS)) ... </k>
+         <opcodeCoverage> COVERAGE </opcodeCoverage>
+         <opcodeLists>    PGMS     </opcodeLists>
+
+    syntax JSON ::= #makeCoverageReport ( Map, Map ) [function]
+ // -----------------------------------------------------------
+    rule #makeCoverageReport (COVERAGE, PGMS) => {
+                                                  "coverages": [#coveragePercentages(keys_list(PGMS),COVERAGE,PGMS)],
+                                                  "coveredOpcodes": [#serializeCoverage(keys_list(COVERAGE),COVERAGE)],
+                                                  "programs": [#serializePrograms(keys_list(PGMS),PGMS)] 
+                                                 }
+
+    syntax JSONList ::= #serializeCoverage ( List, Map ) [function]
+ // ---------------------------------------------------------------
+    rule #serializeCoverage (.List, _ ) => .JSONList
+    rule #serializeCoverage ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:Set COVERAGE:Map ) => { Int2String(CODEHASH):{ Phase2String(EPHASE): [IntList2JSONList(qsort(Set2List(X)))] }}, #serializeCoverage(KEYS, COVERAGE)
+
+    syntax JSONList ::= #serializePrograms ( List, Map ) [function]
+ // ---------------------------------------------------------------
+    rule #serializePrograms (.List, _ ) => .JSONList
+    rule #serializePrograms ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:List PGMS:Map ) => { Int2String(CODEHASH):{ Phase2String(EPHASE): [CoverageIDList2JSONList(X)] }}, #serializePrograms(KEYS, PGMS)
+
+    syntax String ::= Phase2String ( Phase ) [function]
+ // ----------------------------------------------------
+    rule Phase2String (CONSTRUCTOR) => "CONSTRUCTOR"
+    rule Phase2String (RUNTIME)     => "RUNTIME"
+
+    syntax JSONList ::= CoverageIDList2JSONList ( List ) [function]
+ // ---------------------------------------------------------------
+    rule CoverageIDList2JSONList (.List)                           => .JSONList
+    rule CoverageIDList2JSONList (ListItem({I:Int | _:OpCode }) L) => I, CoverageIDList2JSONList(L)
+
+    syntax JSONList ::= IntList2JSONList ( List ) [function]
+ // --------------------------------------------------------
+    rule IntList2JSONList (.List)             => .JSONList
+    rule IntList2JSONList (ListItem(I:Int) L) => I, IntList2JSONList(L)
+
+    syntax List ::= getIntElementsSmallerThan ( Int, List, List ) [function]
+ // ------------------------------------------------------------------------
+    rule getIntElementsSmallerThan (_, .List,               RESULTS) => RESULTS
+    rule getIntElementsSmallerThan (X, (ListItem(I:Int) L), RESULTS) => getIntElementsSmallerThan (X, L, ListItem(I) RESULTS) requires I  <Int X
+    rule getIntElementsSmallerThan (X, (ListItem(I:Int) L), RESULTS) => getIntElementsSmallerThan (X, L, RESULTS)             requires I >=Int X
+
+    syntax List ::= getIntElementsGreaterThan ( Int, List, List ) [function]
+ // ------------------------------------------------------------------------
+    rule getIntElementsGreaterThan (_, .List ,              RESULTS) => RESULTS
+    rule getIntElementsGreaterThan (X, (ListItem(I:Int) L), RESULTS) => getIntElementsGreaterThan (X, L, ListItem(I) RESULTS) requires I  >Int X
+    rule getIntElementsGreaterThan (X, (ListItem(I:Int) L), RESULTS) => getIntElementsGreaterThan (X, L, RESULTS)             requires I <=Int X
+
+    syntax List ::= qsort ( List ) [function]
+ // -----------------------------------------
+    rule qsort ( .List )           => .List
+    rule qsort (ListItem(I:Int) L) => qsort(getIntElementsSmallerThan(I, L, .List)) ListItem(I) qsort(getIntElementsGreaterThan(I, L, .List))
+
+    syntax JSONList ::= #coveragePercentages ( List, Map, Map) [function]
+ // ---------------------------------------------------------------------
+    rule #coveragePercentages (.List, _, _) => .JSONList
+    rule #coveragePercentages ((ListItem({ CODEHASH | EPHASE } #as KEY) KEYS), KEY |-> X:Set COVERAGE:Map, KEY |-> Y:List PGMS:Map) => { Int2String(CODEHASH):{ Phase2String(EPHASE): #computePercentage(size(X),size(Y)) }}, #coveragePercentages(KEYS,COVERAGE,PGMS)
+
+    syntax Int ::= #computePercentage ( Int, Int ) [function]
+ // ---------------------------------------------------------
+    rule #computePercentage (EXECUTED, TOTAL) => (100 *Int EXECUTED) /Int TOTAL
 endmodule
-```
\ No newline at end of file
+```