diff --git a/solarkraft/src/instrument.ts b/solarkraft/src/instrument.ts
index e73ea22..55f3632 100644
--- a/solarkraft/src/instrument.ts
+++ b/solarkraft/src/instrument.ts
@@ -130,8 +130,30 @@ export function instrumentMonitor(
 
     // Declaration of "Next" (according to `contractCall.fields` and `contractCall.method` / `.methodArgs`)
     const envRecord = tlaJsonRecord([
-        { name: 'height', kind: 'TlaInt', value: contractCall.height },
-        { name: 'timestamp', kind: 'TlaInt', value: contractCall.timestamp },
+        // env.ledger().sequence()
+        {
+            name: 'sequence',
+            value: tlaJsonValEx('TlaInt', contractCall.height),
+        },
+        // env.ledger().timestamp()
+        {
+            name: 'timestamp',
+            value: tlaJsonValEx('TlaInt', contractCall.timestamp),
+        },
+        // env.current_contract_address()
+        {
+            name: 'current_contract_address',
+            value: tlaJsonValEx('TlaStr', contractCall.contractId),
+        },
+        // extra environment that's useful in monitor specifications
+        {
+            name: 'invoked_function_name',
+            value: tlaJsonValEx('TlaStr', contractCall.method),
+        },
+        {
+            name: 'invoked_function_return_value',
+            value: tlaJsonOptionOfNative(contractCall.returnValue)
+        },
     ])
 
     const currentInstrumented = tlaJsonAnd(
@@ -229,6 +251,11 @@ export function isTlaName(name: string): boolean {
  *   { "2": 3, "4": 5 }  ~~>  SetAsFun({ <<"2", 3>>, <<"4", 5>> })
  */
 export function tlaJsonOfNative(v: any, forceVec: boolean = false): any {
+    assert(
+        v !== null && v !== undefined,
+        `Expected value, got null or undefined`
+    )
+
     if (typeof v === 'object') {
         if (Array.isArray(v)) {
             // a JS array
@@ -318,6 +345,31 @@ export function tlaJsonOfNative(v: any, forceVec: boolean = false): any {
     return tlaJsonValEx(tlaJsonTypeOfPrimitive(v), v)
 }
 
+/**
+ * Return the Apalache JSON IR representation of a native JS value `v`, wrapped inside an option type.
+ *
+ * If `v` is `null` or `undefined`, returns `None`. Otherwise, returns `Some(nativeValue)`.
+ */
+export function tlaJsonOptionOfNative(v: any): any {
+    if (v) {
+        return {
+            type: 'Untyped',
+            kind: 'OperEx',
+            oper: 'OPER_APP',
+            args: [
+                {
+                    type: 'Untyped',
+                    kind: 'NameEx',
+                    name: 'Some',
+                },
+                tlaJsonOfNative(v),
+            ],
+        }
+    } else {
+        return tlaJsonNone
+    }
+}
+
 /**
  * Return an Apalache TLA+ expression of the form `conjuncts`_0 /\ ... /\ `conjuncts`_n.
  * @param conjuncts Body conjuncts
@@ -376,14 +428,14 @@ function tlaJsonValEx(kind: string, value: any): any {
  * @param bindings Interleaved array of field names and field values.
  * @returns The record in Apalache IR JSON: https://apalache.informal.systems/docs/adr/005adr-json.html
  */
-function tlaJsonRecord(bindings: any): any {
+function tlaJsonRecord(bindings: { name; value }[]): any {
     return {
         type: 'Untyped',
         kind: 'OperEx',
         oper: 'RECORD',
-        args: bindings.flatMap((binding) => [
-            tlaJsonValEx('TlaStr', binding.name),
-            tlaJsonValEx(binding.kind, binding.value),
+        args: bindings.flatMap(({ name, value }) => [
+            tlaJsonValEx('TlaStr', name),
+            value,
         ]),
     }
 }
@@ -403,6 +455,23 @@ function tlaJsonApplication(operName: string, args: any): any {
     }
 }
 
+/**
+ * The Apalache TLA+ expression `None` (of type `None(UNIT)`)
+ * See https://apalache.informal.systems/docs/lang/option-types.html
+ */
+const tlaJsonNone = {
+    type: 'Untyped',
+    kind: 'OperEx',
+    oper: 'OPER_APP',
+    args: [
+        {
+            type: 'Untyped',
+            kind: 'NameEx',
+            name: 'None',
+        },
+    ],
+}
+
 /**
  * The Apalache TLA+ expression `Gen(1)`.
  */
diff --git a/solarkraft/test/unit/instrument.test.ts b/solarkraft/test/unit/instrument.test.ts
index a4a8a9b..512192f 100644
--- a/solarkraft/test/unit/instrument.test.ts
+++ b/solarkraft/test/unit/instrument.test.ts
@@ -10,6 +10,7 @@ import {
     tlaJsonTypeOfPrimitive,
     tlaJsonOfNative,
     isTlaName,
+    tlaJsonOptionOfNative,
 } from '../../src/instrument.js'
 
 import { instrumentedMonitor as expected } from './verify.instrumentedMonitor.js'
@@ -257,4 +258,41 @@ describe('Apalache JSON instrumentor', () => {
         assert.isFalse(isTlaName('3'))
         assert.isFalse(isTlaName('_'))
     })
+
+    it('converts option types', () => {
+        const tlaJsonNone = {
+            type: 'Untyped',
+            kind: 'OperEx',
+            oper: 'OPER_APP',
+            args: [
+                {
+                    type: 'Untyped',
+                    kind: 'NameEx',
+                    name: 'None',
+                },
+            ],
+        }
+        assert.deepEqual(tlaJsonOptionOfNative(null), tlaJsonNone)
+        assert.deepEqual(tlaJsonOptionOfNative(undefined), tlaJsonNone)
+        assert.deepEqual(tlaJsonOptionOfNative(42), {
+            type: 'Untyped',
+            kind: 'OperEx',
+            oper: 'OPER_APP',
+            args: [
+                {
+                    type: 'Untyped',
+                    kind: 'NameEx',
+                    name: 'Some',
+                },
+                {
+                    type: 'Untyped',
+                    kind: 'ValEx',
+                    value: {
+                        kind: 'TlaInt',
+                        value: 42,
+                    },
+                },
+            ],
+        })
+    })
 })
diff --git a/solarkraft/test/unit/verify.instrumentedMonitor.ts b/solarkraft/test/unit/verify.instrumentedMonitor.ts
index 119dc6a..937d215 100644
--- a/solarkraft/test/unit/verify.instrumentedMonitor.ts
+++ b/solarkraft/test/unit/verify.instrumentedMonitor.ts
@@ -84,7 +84,7 @@ const instrumentedMonitor = {
                                                 type: 'Untyped',
                                                 value: {
                                                     kind: 'TlaStr',
-                                                    value: 'height',
+                                                    value: 'sequence',
                                                 },
                                             },
                                             {
@@ -111,6 +111,38 @@ const instrumentedMonitor = {
                                                     value: 1716393856,
                                                 },
                                             },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: 'current_contract_address',
+                                                },
+                                            },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: '0xqwer',
+                                                },
+                                            },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: 'invoked_function_name',
+                                                },
+                                            },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: 'Claim',
+                                                },
+                                            },
                                         ],
                                     },
                                     {
diff --git a/solarkraft/test/unit/verify.instrumentedMonitor2.ts b/solarkraft/test/unit/verify.instrumentedMonitor2.ts
index cd6af1d..669620d 100644
--- a/solarkraft/test/unit/verify.instrumentedMonitor2.ts
+++ b/solarkraft/test/unit/verify.instrumentedMonitor2.ts
@@ -116,7 +116,7 @@ const instrumentedMonitor = {
                                                 type: 'Untyped',
                                                 value: {
                                                     kind: 'TlaStr',
-                                                    value: 'height',
+                                                    value: 'sequence',
                                                 },
                                             },
                                             {
@@ -143,6 +143,38 @@ const instrumentedMonitor = {
                                                     value: 1716393856,
                                                 },
                                             },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: 'current_contract_address',
+                                                },
+                                            },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: '0xqwer',
+                                                },
+                                            },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: 'invoked_function_name',
+                                                },
+                                            },
+                                            {
+                                                kind: 'ValEx',
+                                                type: 'Untyped',
+                                                value: {
+                                                    kind: 'TlaStr',
+                                                    value: 'Claim',
+                                                },
+                                            },
                                         ],
                                     },
                                     {