diff --git a/src/Juvix/Compiler/Builtins/Anoma.hs b/src/Juvix/Compiler/Builtins/Anoma.hs
index a8c62b927c..b0ac198a3c 100644
--- a/src/Juvix/Compiler/Builtins/Anoma.hs
+++ b/src/Juvix/Compiler/Builtins/Anoma.hs
@@ -117,3 +117,106 @@ checkAnomaSha256 f = do
   unless
     (ftype == (nat_ --> byteArray))
     $ builtinsErrorText l "anomaSha256 must be of type Nat -> ByteArray"
+
+checkResource :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => InductiveDef -> Sem r ()
+checkResource d = do
+  let err = builtinsErrorText (getLoc d)
+  unless (null (d ^. inductiveParameters)) (err "AnomaResource should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "AnomaResource should be in the small universe")
+  unless (length (d ^. inductiveConstructors) == 1) (err "AnomaResource should have exactly one constructor")
+
+checkAction :: (Members '[Error ScoperError] r) => InductiveDef -> Sem r ()
+checkAction d = do
+  let err = builtinsErrorText (getLoc d)
+  unless (null (d ^. inductiveParameters)) (err "AnomaAction should have no type parameters")
+  unless (isSmallUniverse' (d ^. inductiveType)) (err "AnomaAction should be in the small universe")
+  unless (length (d ^. inductiveConstructors) == 1) (err "AnomaAction should have exactly one constructor")
+
+checkDelta :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
+checkDelta d =
+  unless (isSmallUniverse' (d ^. axiomType)) $
+    builtinsErrorText (getLoc d) "AnomaDelta should be in the small universe"
+
+checkKind :: (Members '[Error ScoperError] r) => AxiomDef -> Sem r ()
+checkKind d =
+  unless (isSmallUniverse' (d ^. axiomType)) $
+    builtinsErrorText (getLoc d) "AnomaDelta should be in the small universe"
+
+checkResourceCommitment :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceCommitment f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper (getLoc f) BuiltinAnomaResource
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (resource --> nat_)) $
+    builtinsErrorText (getLoc f) "resourceCommitment must be of type AnomaResource -> Nat"
+
+checkResourceNullifier :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceNullifier f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper l BuiltinAnomaResource
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (resource --> nat_)) $
+    builtinsErrorText l "resourceNullifier must be of type AnomaResource -> Nat"
+
+checkResourceKind :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceKind f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper l BuiltinAnomaResource
+  kind <- getBuiltinNameScoper l BuiltinAnomaKind
+  unless (f ^. axiomType === (resource --> kind)) $
+    builtinsErrorText l "resourceNullifier must be of type AnomaResource -> Nat"
+
+checkResourceDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkResourceDelta f = do
+  let l = getLoc f
+  resource <- getBuiltinNameScoper l BuiltinAnomaResource
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === (resource --> delta)) $
+    builtinsErrorText l "resourceDelta must be of type AnomaResource -> AnomaDelta"
+
+checkProveAction :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkProveAction f = do
+  let l = getLoc f
+  action <- getBuiltinNameScoper l BuiltinAnomaAction
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (action --> nat_)) $
+    builtinsErrorText l "proveAction must be of type AnomaAction -> Nat"
+
+checkProveDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkProveDelta f = do
+  let l = getLoc f
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  nat_ <- getBuiltinNameScoper l BuiltinNat
+  unless (f ^. axiomType === (delta --> nat_)) $
+    builtinsErrorText l "proveDelta must be of type AnomaDelta -> Nat"
+
+checkActionDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkActionDelta f = do
+  let l = getLoc f
+  action <- getBuiltinNameScoper l BuiltinAnomaAction
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === (action --> delta)) $
+    builtinsErrorText l "actionDelta must be of type AnomaAction -> AnomaDelta"
+
+checkActionsDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkActionsDelta f = do
+  let l = getLoc f
+  action <- getBuiltinNameScoper l BuiltinAnomaAction
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  list_ <- getBuiltinNameScoper l BuiltinList
+  unless (f ^. axiomType === (list_ @@ action --> delta)) $
+    builtinsErrorText l "actionsDelta must be of type List AnomaAction -> AnomaDelta"
+
+checkDeltaBinaryOp :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkDeltaBinaryOp f = do
+  let l = getLoc f
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === (delta --> delta --> delta)) $
+    builtinsErrorText l "deltaAdd must be of type AnomaDelta -> AnomaDelta -> AnomaDelta"
+
+checkZeroDelta :: (Members '[Reader BuiltinsTable, Error ScoperError] r) => AxiomDef -> Sem r ()
+checkZeroDelta f = do
+  let l = getLoc f
+  delta <- getBuiltinNameScoper l BuiltinAnomaDelta
+  unless (f ^. axiomType === delta) $
+    builtinsErrorText (getLoc f) "zeroDelta must be of Delta"
diff --git a/src/Juvix/Compiler/Concrete/Data/Builtins.hs b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
index 0a4d22d004..5af45c2c1b 100644
--- a/src/Juvix/Compiler/Concrete/Data/Builtins.hs
+++ b/src/Juvix/Compiler/Concrete/Data/Builtins.hs
@@ -57,6 +57,8 @@ builtinConstructors = \case
   BuiltinPair -> [BuiltinPairConstr]
   BuiltinPoseidonState -> [BuiltinMkPoseidonState]
   BuiltinEcPoint -> [BuiltinMkEcPoint]
+  BuiltinAnomaResource -> [BuiltinMkAnomaResource]
+  BuiltinAnomaAction -> [BuiltinMkAnomaAction]
 
 data BuiltinInductive
   = BuiltinNat
@@ -67,6 +69,8 @@ data BuiltinInductive
   | BuiltinPair
   | BuiltinPoseidonState
   | BuiltinEcPoint
+  | BuiltinAnomaResource
+  | BuiltinAnomaAction
   deriving stock (Show, Eq, Ord, Enum, Bounded, Generic, Data)
 
 instance Hashable BuiltinInductive
@@ -85,6 +89,8 @@ instance Pretty BuiltinInductive where
     BuiltinPair -> Str.pair
     BuiltinPoseidonState -> Str.cairoPoseidonState
     BuiltinEcPoint -> Str.cairoEcPoint
+    BuiltinAnomaResource -> Str.anomaResource
+    BuiltinAnomaAction -> Str.anomaAction
 
 instance Pretty BuiltinConstructor where
   pretty = \case
@@ -101,6 +107,8 @@ instance Pretty BuiltinConstructor where
     BuiltinPairConstr -> Str.pair
     BuiltinMkPoseidonState -> Str.cairoMkPoseidonState
     BuiltinMkEcPoint -> Str.cairoMkEcPoint
+    BuiltinMkAnomaResource -> Str.anomaMkResource
+    BuiltinMkAnomaAction -> Str.anomaMkAction
 
 data BuiltinConstructor
   = BuiltinNatZero
@@ -116,6 +124,8 @@ data BuiltinConstructor
   | BuiltinPairConstr
   | BuiltinMkPoseidonState
   | BuiltinMkEcPoint
+  | BuiltinMkAnomaResource
+  | BuiltinMkAnomaAction
   deriving stock (Show, Eq, Ord, Generic, Data)
 
 instance Hashable BuiltinConstructor
@@ -228,6 +238,19 @@ data BuiltinAxiom
   | BuiltinAnomaByteArrayToAnomaContents
   | BuiltinAnomaByteArrayFromAnomaContents
   | BuiltinAnomaSha256
+  | BuiltinAnomaDelta
+  | BuiltinAnomaKind
+  | BuiltinAnomaResourceCommitment
+  | BuiltinAnomaResourceNullifier
+  | BuiltinAnomaResourceKind
+  | BuiltinAnomaResourceDelta
+  | BuiltinAnomaActionDelta
+  | BuiltinAnomaActionsDelta
+  | BuiltinAnomaZeroDelta
+  | BuiltinAnomaAddDelta
+  | BuiltinAnomaSubDelta
+  | BuiltinAnomaProveAction
+  | BuiltinAnomaProveDelta
   | BuiltinPoseidon
   | BuiltinEcOp
   | BuiltinRandomEcPoint
@@ -275,6 +298,19 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaByteArrayToAnomaContents -> KNameFunction
     BuiltinAnomaByteArrayFromAnomaContents -> KNameFunction
     BuiltinAnomaSha256 -> KNameFunction
+    BuiltinAnomaDelta -> KNameInductive
+    BuiltinAnomaKind -> KNameInductive
+    BuiltinAnomaResourceCommitment -> KNameFunction
+    BuiltinAnomaResourceNullifier -> KNameFunction
+    BuiltinAnomaResourceKind -> KNameFunction
+    BuiltinAnomaResourceDelta -> KNameFunction
+    BuiltinAnomaActionDelta -> KNameFunction
+    BuiltinAnomaActionsDelta -> KNameFunction
+    BuiltinAnomaZeroDelta -> KNameFunction
+    BuiltinAnomaAddDelta -> KNameFunction
+    BuiltinAnomaSubDelta -> KNameFunction
+    BuiltinAnomaProveAction -> KNameFunction
+    BuiltinAnomaProveDelta -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -329,6 +365,19 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
     BuiltinAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
     BuiltinAnomaSha256 -> Str.anomaSha256
+    BuiltinAnomaDelta -> Str.anomaDelta
+    BuiltinAnomaKind -> Str.anomaKind
+    BuiltinAnomaResourceCommitment -> Str.anomaResourceCommitment
+    BuiltinAnomaResourceNullifier -> Str.anomaResourceNullifier
+    BuiltinAnomaResourceKind -> Str.anomaResourceKind
+    BuiltinAnomaResourceDelta -> Str.anomaResourceDelta
+    BuiltinAnomaActionDelta -> Str.anomaActionDelta
+    BuiltinAnomaActionsDelta -> Str.anomaActionsDelta
+    BuiltinAnomaZeroDelta -> Str.anomaZeroDelta
+    BuiltinAnomaAddDelta -> Str.anomaAddDelta
+    BuiltinAnomaSubDelta -> Str.anomaSubDelta
+    BuiltinAnomaProveDelta -> Str.anomaProveDelta
+    BuiltinAnomaProveAction -> Str.anomaProveAction
     BuiltinPoseidon -> Str.cairoPoseidon
     BuiltinEcOp -> Str.cairoEcOp
     BuiltinRandomEcPoint -> Str.cairoRandomEcPoint
diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
index 605bb1b969..aabf4a5b98 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@@ -63,6 +63,12 @@ getIntSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinInt
 getPoseidonStateSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
 getPoseidonStateSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinPoseidonState
 
+getAnomaResourceSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getAnomaResourceSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinAnomaResource
+
+getAnomaActionSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
+getAnomaActionSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinAnomaAction
+
 getEcPointSymbol :: (Member InfoTableBuilder r) => Sem r Symbol
 getEcPointSymbol = (^. inductiveSymbol) <$> getBuiltinInductiveInfo BuiltinEcPoint
 
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 938922a6ec..2934a55f81 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -228,6 +228,17 @@ geval opts herr tab env0 = eval' env0
       OpAnomaByteArrayToAnomaContents -> anomaByteArrayToAnomaContents
       OpAnomaByteArrayFromAnomaContents -> anomaByteArrayFromAnomaContents
       OpAnomaSha256 -> anomaSha256
+      OpAnomaResourceCommitment -> normalizeOrUnsupported opcode
+      OpAnomaResourceNullifier -> normalizeOrUnsupported opcode
+      OpAnomaResourceKind -> normalizeOrUnsupported opcode
+      OpAnomaResourceDelta -> normalizeOrUnsupported opcode
+      OpAnomaActionDelta -> normalizeOrUnsupported opcode
+      OpAnomaActionsDelta -> normalizeOrUnsupported opcode
+      OpAnomaProveAction -> normalizeOrUnsupported opcode
+      OpAnomaProveDelta -> normalizeOrUnsupported opcode
+      OpAnomaZeroDelta -> normalizeOrUnsupported opcode
+      OpAnomaAddDelta -> normalizeOrUnsupported opcode
+      OpAnomaSubDelta -> normalizeOrUnsupported opcode
       OpPoseidonHash -> poseidonHashOp
       OpEc -> ecOp
       OpRandomEcPoint -> randomEcPointOp
@@ -384,6 +395,15 @@ geval opts herr tab env0 = eval' env0
                           Exception.throw (EvalError ("assertion failed: " <> printNode val) Nothing)
         {-# INLINE assertOp #-}
 
+        normalizeOrUnsupported :: BuiltinOp -> [Node] -> Node
+        normalizeOrUnsupported op args =
+          if
+              | opts ^. evalOptionsNormalize || opts ^. evalOptionsNoFailure ->
+                  mkBuiltinApp' op (eval' env <$> args)
+              | otherwise ->
+                  err ("unsupported builtin operation: " <> show op)
+        {-# INLINE normalizeOrUnsupported #-}
+
         anomaGetOp :: [Node] -> Node
         anomaGetOp = unary $ \arg ->
           if
diff --git a/src/Juvix/Compiler/Core/Extra/Utils.hs b/src/Juvix/Compiler/Core/Extra/Utils.hs
index ccfc9c9efe..fc01e58422 100644
--- a/src/Juvix/Compiler/Core/Extra/Utils.hs
+++ b/src/Juvix/Compiler/Core/Extra/Utils.hs
@@ -195,6 +195,17 @@ isDebugOp = \case
       OpAnomaSignDetached -> False
       OpAnomaVerifyDetached -> False
       OpAnomaVerifyWithMessage -> False
+      OpAnomaResourceCommitment -> False
+      OpAnomaResourceNullifier -> False
+      OpAnomaResourceKind -> False
+      OpAnomaResourceDelta -> False
+      OpAnomaActionDelta -> False
+      OpAnomaActionsDelta -> False
+      OpAnomaProveAction -> False
+      OpAnomaProveDelta -> False
+      OpAnomaZeroDelta -> False
+      OpAnomaAddDelta -> False
+      OpAnomaSubDelta -> False
       OpEc -> False
       OpFieldAdd -> False
       OpFieldDiv -> False
@@ -482,6 +493,17 @@ builtinOpArgTypes = \case
   OpAnomaByteArrayToAnomaContents -> [mkDynamic']
   OpAnomaByteArrayFromAnomaContents -> [mkTypeInteger', mkTypeInteger']
   OpAnomaSha256 -> [mkTypeInteger']
+  OpAnomaResourceCommitment -> [mkDynamic']
+  OpAnomaResourceNullifier -> [mkDynamic']
+  OpAnomaResourceKind -> [mkDynamic']
+  OpAnomaResourceDelta -> [mkDynamic']
+  OpAnomaActionDelta -> [mkDynamic']
+  OpAnomaActionsDelta -> [mkDynamic']
+  OpAnomaProveAction -> [mkDynamic']
+  OpAnomaProveDelta -> [mkDynamic']
+  OpAnomaZeroDelta -> []
+  OpAnomaAddDelta -> [mkDynamic', mkDynamic']
+  OpAnomaSubDelta -> [mkDynamic', mkDynamic']
   OpPoseidonHash -> [mkDynamic']
   OpEc -> [mkDynamic', mkTypeField', mkDynamic']
   OpRandomEcPoint -> []
diff --git a/src/Juvix/Compiler/Core/Keywords.hs b/src/Juvix/Compiler/Core/Keywords.hs
index 0d6655e727..504963300e 100644
--- a/src/Juvix/Compiler/Core/Keywords.hs
+++ b/src/Juvix/Compiler/Core/Keywords.hs
@@ -8,13 +8,24 @@ where
 import Juvix.Data.Keyword
 import Juvix.Data.Keyword.All
   ( delimSemicolon,
+    kwAnomaActionDelta,
+    kwAnomaActionsDelta,
+    kwAnomaAddDelta,
     kwAnomaDecode,
     kwAnomaEncode,
+    kwAnomaProveAction,
+    kwAnomaProveDelta,
+    kwAnomaResourceCommitment,
+    kwAnomaResourceDelta,
+    kwAnomaResourceKind,
+    kwAnomaResourceNullifier,
     kwAnomaSha256,
     kwAnomaSign,
     kwAnomaSignDetached,
+    kwAnomaSubDelta,
     kwAnomaVerifyDetached,
     kwAnomaVerifyWithMessage,
+    kwAnomaZeroDelta,
     kwAny,
     kwAssert,
     kwAssign,
diff --git a/src/Juvix/Compiler/Core/Language/Builtins.hs b/src/Juvix/Compiler/Core/Language/Builtins.hs
index de8637eba9..d836b55634 100644
--- a/src/Juvix/Compiler/Core/Language/Builtins.hs
+++ b/src/Juvix/Compiler/Core/Language/Builtins.hs
@@ -40,6 +40,17 @@ data BuiltinOp
   | OpAnomaByteArrayToAnomaContents
   | OpAnomaByteArrayFromAnomaContents
   | OpAnomaSha256
+  | OpAnomaResourceCommitment
+  | OpAnomaResourceNullifier
+  | OpAnomaResourceKind
+  | OpAnomaResourceDelta
+  | OpAnomaActionDelta
+  | OpAnomaActionsDelta
+  | OpAnomaProveAction
+  | OpAnomaProveDelta
+  | OpAnomaZeroDelta
+  | OpAnomaAddDelta
+  | OpAnomaSubDelta
   | OpPoseidonHash
   | OpEc
   | OpRandomEcPoint
@@ -47,7 +58,7 @@ data BuiltinOp
   | OpUInt8FromInt
   | OpByteArrayFromListByte
   | OpByteArrayLength
-  deriving stock (Eq, Generic)
+  deriving stock (Eq, Generic, Show)
 
 instance Serialize BuiltinOp
 
@@ -114,6 +125,17 @@ builtinOpArgsNum = \case
   OpAnomaByteArrayToAnomaContents -> 1
   OpAnomaByteArrayFromAnomaContents -> 2
   OpAnomaSha256 -> 1
+  OpAnomaResourceCommitment -> 1
+  OpAnomaResourceNullifier -> 1
+  OpAnomaResourceKind -> 1
+  OpAnomaResourceDelta -> 1
+  OpAnomaActionDelta -> 1
+  OpAnomaActionsDelta -> 1
+  OpAnomaProveAction -> 1
+  OpAnomaProveDelta -> 1
+  OpAnomaZeroDelta -> 0
+  OpAnomaAddDelta -> 2
+  OpAnomaSubDelta -> 2
   OpPoseidonHash -> 1
   OpEc -> 3
   OpRandomEcPoint -> 0
@@ -164,6 +186,17 @@ builtinIsFoldable = \case
   OpAnomaVerifyWithMessage -> False
   OpAnomaByteArrayToAnomaContents -> False
   OpAnomaByteArrayFromAnomaContents -> False
+  OpAnomaResourceCommitment -> False
+  OpAnomaResourceNullifier -> False
+  OpAnomaResourceKind -> False
+  OpAnomaResourceDelta -> False
+  OpAnomaActionDelta -> False
+  OpAnomaActionsDelta -> False
+  OpAnomaProveAction -> False
+  OpAnomaProveDelta -> False
+  OpAnomaZeroDelta -> False
+  OpAnomaAddDelta -> False
+  OpAnomaSubDelta -> False
   OpAnomaSha256 -> False
   OpPoseidonHash -> False
   OpEc -> False
@@ -199,7 +232,18 @@ builtinsAnoma =
     OpAnomaSignDetached,
     OpAnomaByteArrayToAnomaContents,
     OpAnomaByteArrayFromAnomaContents,
-    OpAnomaSha256
+    OpAnomaSha256,
+    OpAnomaResourceCommitment,
+    OpAnomaResourceNullifier,
+    OpAnomaResourceKind,
+    OpAnomaResourceDelta,
+    OpAnomaActionDelta,
+    OpAnomaActionsDelta,
+    OpAnomaProveAction,
+    OpAnomaProveDelta,
+    OpAnomaZeroDelta,
+    OpAnomaAddDelta,
+    OpAnomaSubDelta
   ]
 
 builtinsUInt8 :: [BuiltinOp]
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index d25bd9a810..5494a0abf8 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -64,6 +64,17 @@ instance PrettyCode BuiltinOp where
     OpAnomaByteArrayToAnomaContents -> return primAnomaByteArrayToAnomaContents
     OpAnomaByteArrayFromAnomaContents -> return primAnomaByteArrayFromAnomaContents
     OpAnomaSha256 -> return primAnomaSha256
+    OpAnomaResourceCommitment -> return primResourceCommitment
+    OpAnomaResourceNullifier -> return primResourceNullifier
+    OpAnomaResourceKind -> return primResourceKind
+    OpAnomaResourceDelta -> return primResourceDelta
+    OpAnomaActionDelta -> return primActionDelta
+    OpAnomaActionsDelta -> return primActionsDelta
+    OpAnomaProveAction -> return primProveAction
+    OpAnomaProveDelta -> return primProveDelta
+    OpAnomaZeroDelta -> return primZeroDelta
+    OpAnomaAddDelta -> return primAddDelta
+    OpAnomaSubDelta -> return primSubDelta
     OpPoseidonHash -> return primPoseidonHash
     OpEc -> return primEc
     OpRandomEcPoint -> return primRandomEcPoint
@@ -601,6 +612,8 @@ instance PrettyCode InfoTable where
               BuiltinNat -> False
               BuiltinInt -> False
               BuiltinBool -> False
+              BuiltinAnomaResource -> True
+              BuiltinAnomaAction -> True
             Just _ -> False
             Nothing -> True
 
@@ -908,6 +921,39 @@ primAnomaByteArrayFromAnomaContents = primitive Str.anomaByteArrayFromAnomaConte
 primAnomaSha256 :: Doc Ann
 primAnomaSha256 = primitive Str.anomaSha256
 
+primResourceCommitment :: Doc Ann
+primResourceCommitment = primitive Str.anomaResourceCommitment
+
+primResourceNullifier :: Doc Ann
+primResourceNullifier = primitive Str.anomaResourceNullifier
+
+primResourceKind :: Doc Ann
+primResourceKind = primitive Str.anomaResourceKind
+
+primResourceDelta :: Doc Ann
+primResourceDelta = primitive Str.anomaResourceDelta
+
+primActionDelta :: Doc Ann
+primActionDelta = primitive Str.anomaActionDelta
+
+primActionsDelta :: Doc Ann
+primActionsDelta = primitive Str.anomaActionsDelta
+
+primProveDelta :: Doc Ann
+primProveDelta = primitive Str.anomaProveDelta
+
+primProveAction :: Doc Ann
+primProveAction = primitive Str.anomaProveAction
+
+primZeroDelta :: Doc Ann
+primZeroDelta = primitive Str.anomaZeroDelta
+
+primAddDelta :: Doc Ann
+primAddDelta = primitive Str.anomaAddDelta
+
+primSubDelta :: Doc Ann
+primSubDelta = primitive Str.anomaSubDelta
+
 primPoseidonHash :: Doc Ann
 primPoseidonHash = primitive Str.cairoPoseidon
 
diff --git a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
index dcc48e2899..8e6d16154e 100644
--- a/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
+++ b/src/Juvix/Compiler/Core/Transformation/ComputeTypeInfo.hs
@@ -81,6 +81,17 @@ computeNodeTypeInfo md = umapL go
           OpAnomaByteArrayFromAnomaContents -> Info.getNodeType node
           OpAnomaByteArrayToAnomaContents -> mkTypeInteger'
           OpAnomaSha256 -> mkTypeByteArray'
+          OpAnomaResourceCommitment -> mkTypeInteger'
+          OpAnomaResourceNullifier -> mkTypeInteger'
+          OpAnomaResourceKind -> mkDynamic'
+          OpAnomaResourceDelta -> mkDynamic'
+          OpAnomaActionDelta -> mkDynamic'
+          OpAnomaActionsDelta -> mkDynamic'
+          OpAnomaProveAction -> mkTypeInteger'
+          OpAnomaProveDelta -> mkTypeInteger'
+          OpAnomaZeroDelta -> mkDynamic'
+          OpAnomaAddDelta -> mkDynamic'
+          OpAnomaSubDelta -> mkDynamic'
           OpPoseidonHash -> case _builtinAppArgs of
             [arg] -> Info.getNodeType arg
             _ -> error "incorrect poseidon builtin application"
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index a3322d92e9..9dfb797380 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -228,6 +228,8 @@ goConstructor sym ctor = do
       Just Internal.BuiltinPairConstr -> freshTag
       Just Internal.BuiltinMkPoseidonState -> freshTag
       Just Internal.BuiltinMkEcPoint -> freshTag
+      Just Internal.BuiltinMkAnomaAction -> freshTag
+      Just Internal.BuiltinMkAnomaResource -> freshTag
       Nothing -> freshTag
 
     ctorType :: Sem r Type
@@ -647,6 +649,19 @@ goAxiomInductive a = whenJust (a ^. Internal.axiomBuiltin) builtinInductive
       Internal.BuiltinAnomaByteArrayToAnomaContents -> return ()
       Internal.BuiltinAnomaByteArrayFromAnomaContents -> return ()
       Internal.BuiltinAnomaSha256 -> return ()
+      Internal.BuiltinAnomaDelta -> registerInductiveAxiom (Just BuiltinAnomaDelta) []
+      Internal.BuiltinAnomaKind -> registerInductiveAxiom (Just BuiltinAnomaKind) []
+      Internal.BuiltinAnomaResourceCommitment -> return ()
+      Internal.BuiltinAnomaResourceNullifier -> return ()
+      Internal.BuiltinAnomaResourceDelta -> return ()
+      Internal.BuiltinAnomaResourceKind -> return ()
+      Internal.BuiltinAnomaActionDelta -> return ()
+      Internal.BuiltinAnomaActionsDelta -> return ()
+      Internal.BuiltinAnomaProveDelta -> return ()
+      Internal.BuiltinAnomaProveAction -> return ()
+      Internal.BuiltinAnomaZeroDelta -> return ()
+      Internal.BuiltinAnomaAddDelta -> return ()
+      Internal.BuiltinAnomaSubDelta -> return ()
       Internal.BuiltinPoseidon -> return ()
       Internal.BuiltinEcOp -> return ()
       Internal.BuiltinRandomEcPoint -> return ()
@@ -861,6 +876,82 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               natType
               (mkBuiltinApp' OpAnomaSha256 [mkVar' 0])
           )
+      Internal.BuiltinAnomaDelta -> return ()
+      Internal.BuiltinAnomaKind -> return ()
+      Internal.BuiltinAnomaResourceCommitment -> do
+        resourceType <- getAnomaResourceType
+        registerAxiomDef
+          ( mkLambda'
+              resourceType
+              (mkBuiltinApp' OpAnomaResourceCommitment [mkVar' 0])
+          )
+      Internal.BuiltinAnomaResourceNullifier -> do
+        resourceType <- getAnomaResourceType
+        registerAxiomDef
+          ( mkLambda'
+              resourceType
+              (mkBuiltinApp' OpAnomaResourceNullifier [mkVar' 0])
+          )
+      Internal.BuiltinAnomaResourceKind -> do
+        resourceType <- getAnomaResourceType
+        registerAxiomDef
+          ( mkLambda'
+              resourceType
+              (mkBuiltinApp' OpAnomaResourceKind [mkVar' 0])
+          )
+      Internal.BuiltinAnomaResourceDelta -> do
+        resourceType <- getAnomaResourceType
+        registerAxiomDef
+          ( mkLambda'
+              resourceType
+              (mkBuiltinApp' OpAnomaResourceDelta [mkVar' 0])
+          )
+      Internal.BuiltinAnomaActionDelta -> do
+        actionType <- getAnomaActionType
+        registerAxiomDef
+          ( mkLambda'
+              actionType
+              (mkBuiltinApp' OpAnomaActionDelta [mkVar' 0])
+          )
+      Internal.BuiltinAnomaActionsDelta -> do
+        registerAxiomDef
+          ( mkLambda'
+              mkDynamic'
+              (mkBuiltinApp' OpAnomaActionsDelta [mkVar' 0])
+          )
+      Internal.BuiltinAnomaProveAction -> do
+        actionType <- getAnomaActionType
+        registerAxiomDef
+          ( mkLambda'
+              actionType
+              (mkBuiltinApp' OpAnomaProveAction [mkVar' 0])
+          )
+      Internal.BuiltinAnomaProveDelta -> do
+        registerAxiomDef
+          ( mkLambda'
+              mkDynamic'
+              (mkBuiltinApp' OpAnomaProveDelta [mkVar' 0])
+          )
+      Internal.BuiltinAnomaZeroDelta -> do
+        registerAxiomDef (mkBuiltinApp' OpAnomaZeroDelta [])
+      Internal.BuiltinAnomaAddDelta -> do
+        registerAxiomDef
+          ( mkLambda'
+              mkDynamic'
+              ( mkLambda'
+                  mkDynamic'
+                  (mkBuiltinApp' OpAnomaAddDelta [mkVar' 1, mkVar' 0])
+              )
+          )
+      Internal.BuiltinAnomaSubDelta -> do
+        registerAxiomDef
+          ( mkLambda'
+              mkDynamic'
+              ( mkLambda'
+                  mkDynamic'
+                  (mkBuiltinApp' OpAnomaSubDelta [mkVar' 1, mkVar' 0])
+              )
+          )
       Internal.BuiltinPoseidon -> do
         psName <- getPoseidonStateName
         psSym <- getPoseidonStateSymbol
@@ -914,6 +1005,24 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
     getEcPointName :: Sem r Text
     getEcPointName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinEcPoint
 
+    getAnomaResourceName :: Sem r Text
+    getAnomaResourceName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinAnomaResource
+
+    getAnomaActionName :: Sem r Text
+    getAnomaActionName = (^. inductiveName) <$> getBuiltinInductiveInfo BuiltinAnomaAction
+
+    getAnomaResourceType :: Sem r Type
+    getAnomaResourceType = do
+      resourceName <- getAnomaResourceName
+      resourceSymbol <- getAnomaResourceSymbol
+      return (mkTypeConstr (setInfoName resourceName mempty) resourceSymbol [])
+
+    getAnomaActionType :: Sem r Type
+    getAnomaActionType = do
+      actionName <- getAnomaActionName
+      actionSymbol <- getAnomaActionSymbol
+      return (mkTypeConstr (setInfoName actionName mempty) actionSymbol [])
+
     registerAxiomDef :: Node -> Sem r ()
     registerAxiomDef body = do
       let name = a ^. Internal.axiomName
@@ -1285,6 +1394,19 @@ goApplication a = do
         Just Internal.BuiltinAnomaByteArrayToAnomaContents -> app
         Just Internal.BuiltinAnomaByteArrayFromAnomaContents -> app
         Just Internal.BuiltinAnomaSha256 -> app
+        Just Internal.BuiltinAnomaDelta -> app
+        Just Internal.BuiltinAnomaKind -> app
+        Just Internal.BuiltinAnomaResourceCommitment -> app
+        Just Internal.BuiltinAnomaResourceNullifier -> app
+        Just Internal.BuiltinAnomaResourceDelta -> app
+        Just Internal.BuiltinAnomaResourceKind -> app
+        Just Internal.BuiltinAnomaActionDelta -> app
+        Just Internal.BuiltinAnomaActionsDelta -> app
+        Just Internal.BuiltinAnomaZeroDelta -> app
+        Just Internal.BuiltinAnomaAddDelta -> app
+        Just Internal.BuiltinAnomaSubDelta -> app
+        Just Internal.BuiltinAnomaProveAction -> app
+        Just Internal.BuiltinAnomaProveDelta -> app
         Just Internal.BuiltinPoseidon -> app
         Just Internal.BuiltinEcOp -> app
         Just Internal.BuiltinRandomEcPoint -> app
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index c6063475c5..20ce8f5c1a 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -585,6 +585,18 @@ builtinAppExpr varsNum vars = do
       <|> (kw kwByteArrayFromListByte $> OpByteArrayFromListByte)
       <|> (kw kwByteArrayLength $> OpByteArrayLength)
       <|> (kw kwAnomaSha256 $> OpAnomaSha256)
+      <|> (kw kwAnomaResourceCommitment $> OpAnomaResourceCommitment)
+      <|> (kw kwAnomaResourceNullifier $> OpAnomaResourceNullifier)
+      <|> (kw kwAnomaResourceKind $> OpAnomaResourceKind)
+      <|> (kw kwAnomaResourceDelta $> OpAnomaResourceDelta)
+      <|> (kw kwAnomaActionDelta $> OpAnomaActionDelta)
+      <|> (kw kwAnomaActionsDelta $> OpAnomaActionsDelta)
+      <|> (kw kwAnomaProveAction $> OpAnomaProveAction)
+      <|> (kw kwAnomaProveDelta $> OpAnomaProveDelta)
+      <|> (kw kwAnomaZeroDelta $> OpAnomaZeroDelta)
+      <|> (kw kwAnomaAddDelta $> OpAnomaAddDelta)
+      <|> (kw kwAnomaSubDelta $> OpAnomaSubDelta)
+
   args <- P.many (atom varsNum vars)
   return $ mkBuiltinApp' op args
 
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 7e791afa2c..06ded95a4c 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -73,6 +73,8 @@ fromCore fsize tab =
       BuiltinBoolFalse -> False
       BuiltinIntOfNat -> False
       BuiltinIntNegSuc -> False
+      BuiltinMkAnomaResource -> True
+      BuiltinMkAnomaAction -> True
 
     shouldKeepType :: BuiltinType -> Bool
     shouldKeepType = \case
@@ -110,6 +112,19 @@ fromCore fsize tab =
         BuiltinAnomaByteArrayToAnomaContents -> False
         BuiltinAnomaByteArrayFromAnomaContents -> False
         BuiltinAnomaSha256 -> False
+        BuiltinAnomaDelta -> False
+        BuiltinAnomaKind -> False
+        BuiltinAnomaResourceCommitment -> False
+        BuiltinAnomaResourceDelta -> False
+        BuiltinAnomaResourceNullifier -> False
+        BuiltinAnomaResourceKind -> False
+        BuiltinAnomaActionDelta -> False
+        BuiltinAnomaActionsDelta -> False
+        BuiltinAnomaAddDelta -> False
+        BuiltinAnomaSubDelta -> False
+        BuiltinAnomaZeroDelta -> False
+        BuiltinAnomaProveAction -> False
+        BuiltinAnomaProveDelta -> False
         BuiltinPoseidon -> False
         BuiltinEcOp -> False
         BuiltinRandomEcPoint -> False
@@ -129,6 +144,8 @@ fromCore fsize tab =
         BuiltinNat -> False
         BuiltinInt -> False
         BuiltinBool -> False
+        BuiltinAnomaResource -> True
+        BuiltinAnomaAction -> True
 
 translateFunctionInfo :: InfoTable -> IdentifierInfo -> Stripped.FunctionInfo
 translateFunctionInfo tab IdentifierInfo {..} =
diff --git a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
index 4fe877717d..23c2e2bb99 100644
--- a/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
+++ b/src/Juvix/Compiler/Internal/Extra/DependencyBuilder.hs
@@ -197,6 +197,8 @@ checkBuiltinInductiveStartNode i = whenJust (i ^. inductiveBuiltin) go
       BuiltinPair -> return ()
       BuiltinPoseidonState -> return ()
       BuiltinEcPoint -> return ()
+      BuiltinAnomaResource -> return ()
+      BuiltinAnomaAction -> return ()
 
     addInductiveStartNode :: Sem r ()
     addInductiveStartNode = addStartNode (i ^. inductiveName)
diff --git a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
index 6e83ac024a..b493bde059 100644
--- a/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
+++ b/src/Juvix/Compiler/Internal/Translation/FromConcrete.hs
@@ -520,6 +520,8 @@ checkBuiltinInductive d b = localBuiltins $ case b of
   BuiltinPair -> checkPairDef d
   BuiltinPoseidonState -> checkPoseidonStateDef d
   BuiltinEcPoint -> checkEcPointDef d
+  BuiltinAnomaResource -> checkResource d
+  BuiltinAnomaAction -> checkAction d
 
 localBuiltins :: (Members '[Reader S.InfoTable] r) => Sem (Reader BuiltinsTable ': r) a -> Sem r a
 localBuiltins m = do
@@ -601,6 +603,19 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaByteArrayFromAnomaContents -> checkAnomaByteArrayFromAnomaContents d
   BuiltinAnomaByteArrayToAnomaContents -> checkAnomaByteArrayToAnomaContents d
   BuiltinAnomaSha256 -> checkAnomaSha256 d
+  BuiltinAnomaDelta -> checkDelta d
+  BuiltinAnomaKind -> checkKind d
+  BuiltinAnomaResourceCommitment -> checkResourceCommitment d
+  BuiltinAnomaResourceNullifier -> checkResourceNullifier d
+  BuiltinAnomaResourceKind -> checkResourceKind d
+  BuiltinAnomaResourceDelta -> checkResourceDelta d
+  BuiltinAnomaActionDelta -> checkActionDelta d
+  BuiltinAnomaActionsDelta -> checkActionsDelta d
+  BuiltinAnomaZeroDelta -> checkZeroDelta d
+  BuiltinAnomaAddDelta -> checkDeltaBinaryOp d
+  BuiltinAnomaSubDelta -> checkDeltaBinaryOp d
+  BuiltinAnomaProveDelta -> checkProveDelta d
+  BuiltinAnomaProveAction -> checkProveAction d
   BuiltinPoseidon -> checkPoseidon d
   BuiltinEcOp -> checkEcOp d
   BuiltinRandomEcPoint -> checkRandomEcPoint d
diff --git a/src/Juvix/Compiler/Nockma/Evaluator.hs b/src/Juvix/Compiler/Nockma/Evaluator.hs
index bcae856bcf..aa55ab4bde 100644
--- a/src/Juvix/Compiler/Nockma/Evaluator.hs
+++ b/src/Juvix/Compiler/Nockma/Evaluator.hs
@@ -229,7 +229,7 @@ evalProfile inistack initerm =
           case _anomaLibCallRef of
             AnomaLibValue (AnomaRmValue v) -> case v of
               RmZeroDelta -> nonInterceptCall
-            AnomaLibFunction (AnomaRmFunction _) -> error "Resource Machine client library functions are not supported"
+            AnomaLibFunction (AnomaRmFunction _) -> nonInterceptCall
             AnomaLibFunction (AnomaStdlibFunction f) -> case f of
               StdlibDec -> unaArith pred
               StdlibAdd -> binArith (+)
diff --git a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
index 152ce86994..bc0c0311aa 100644
--- a/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
+++ b/src/Juvix/Compiler/Nockma/Translation/FromTree.hs
@@ -571,6 +571,17 @@ compile = \case
         Tree.OpAnomaByteArrayFromAnomaContents -> return (goAnomaByteArrayFromAnomaContents args)
         Tree.OpAnomaByteArrayToAnomaContents -> return (goAnomaByteArrayToAnomaContents args)
         Tree.OpAnomaSha256 -> goAnomaSha256 args
+        Tree.OpAnomaResourceCommitment -> callRm RmCommit args
+        Tree.OpAnomaResourceNullifier -> callRm RmNullify args
+        Tree.OpAnomaResourceKind -> callRm RmKind args
+        Tree.OpAnomaResourceDelta -> callRm RmResourceDelta args
+        Tree.OpAnomaActionDelta -> callRm RmActionDelta args
+        Tree.OpAnomaActionsDelta -> callRm RmMakeDelta args
+        Tree.OpAnomaProveAction -> callRm RmProveAction args
+        Tree.OpAnomaProveDelta -> callRm RmProveDelta args
+        Tree.OpAnomaZeroDelta -> rmValue RmZeroDelta
+        Tree.OpAnomaAddDelta -> callRm RmDeltaAdd args
+        Tree.OpAnomaSubDelta -> callRm RmDeltaSub args
 
     goByteArrayOp :: Tree.NodeByteArray -> Sem r (Term Natural)
     goByteArrayOp Tree.NodeByteArray {..} = do
@@ -861,6 +872,10 @@ callAnomaLib fun args = do
 callStdlib :: (Member (Reader CompilerCtx) r) => StdlibFunction -> [Term Natural] -> Sem r (Term Natural)
 callStdlib f = callAnomaLib (AnomaStdlibFunction f)
 
+-- | Convenience function to call an Anoma Resource Machine function
+callRm :: (Member (Reader CompilerCtx) r) => RmFunction -> [Term Natural] -> Sem r (Term Natural)
+callRm f = callAnomaLib (AnomaRmFunction f)
+
 -- | Get a value from the Anoma library
 anomaLibValue :: (Member (Reader CompilerCtx) r) => AnomaValue -> Sem r (Term Natural)
 anomaLibValue v = do
diff --git a/src/Juvix/Compiler/Tree/Keywords.hs b/src/Juvix/Compiler/Tree/Keywords.hs
index 580033bce5..febd235204 100644
--- a/src/Juvix/Compiler/Tree/Keywords.hs
+++ b/src/Juvix/Compiler/Tree/Keywords.hs
@@ -9,16 +9,27 @@ import Juvix.Compiler.Tree.Keywords.Base
 import Juvix.Data.Keyword.All
   ( kwAdd_,
     kwAlloc,
+    kwAnomaActionDelta,
+    kwAnomaActionsDelta,
+    kwAnomaAddDelta,
     kwAnomaByteArrayFromAnomaContents,
     kwAnomaByteArrayToAnomaContents,
     kwAnomaDecode,
     kwAnomaEncode,
     kwAnomaGet,
+    kwAnomaProveAction,
+    kwAnomaProveDelta,
+    kwAnomaResourceCommitment,
+    kwAnomaResourceDelta,
+    kwAnomaResourceKind,
+    kwAnomaResourceNullifier,
     kwAnomaSha256,
     kwAnomaSign,
     kwAnomaSignDetached,
+    kwAnomaSubDelta,
     kwAnomaVerifyDetached,
     kwAnomaVerifyWithMessage,
+    kwAnomaZeroDelta,
     kwArgsNum,
     kwAssert,
     kwAtoi,
diff --git a/src/Juvix/Compiler/Tree/Language/Builtins.hs b/src/Juvix/Compiler/Tree/Language/Builtins.hs
index b505e2339e..48eac16287 100644
--- a/src/Juvix/Compiler/Tree/Language/Builtins.hs
+++ b/src/Juvix/Compiler/Tree/Language/Builtins.hs
@@ -102,4 +102,26 @@ data AnomaOp
     OpAnomaByteArrayFromAnomaContents
   | -- | Hash a value using SHA256
     OpAnomaSha256
-  deriving stock (Eq)
+  | -- | Compute the commitment of a Resource
+    OpAnomaResourceCommitment
+  | -- | Compute the nullifier of a Resource
+    OpAnomaResourceNullifier
+  | -- | Compute the kind of a Resource
+    OpAnomaResourceKind
+  | -- | Compute the delta of a Resource
+    OpAnomaResourceDelta
+  | -- | Compute the delta of an Action
+    OpAnomaActionDelta
+  | -- | Compute the delta of a list of Actions
+    OpAnomaActionsDelta
+  | -- | Compute the proof of an Action
+    OpAnomaProveAction
+  | -- | Compute the proof of a Delta
+    OpAnomaProveDelta
+  | -- | The zero Delta
+    OpAnomaZeroDelta
+  | -- | Add Deltas
+    OpAnomaAddDelta
+  | -- | Subtract Deltas
+    OpAnomaSubDelta
+  deriving stock (Eq, Show)
diff --git a/src/Juvix/Compiler/Tree/Pretty/Base.hs b/src/Juvix/Compiler/Tree/Pretty/Base.hs
index 8892a82d7b..72b8a4cab7 100644
--- a/src/Juvix/Compiler/Tree/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Tree/Pretty/Base.hs
@@ -287,6 +287,17 @@ instance PrettyCode AnomaOp where
     OpAnomaByteArrayFromAnomaContents -> Str.anomaByteArrayFromAnomaContents
     OpAnomaByteArrayToAnomaContents -> Str.anomaByteArrayToAnomaContents
     OpAnomaSha256 -> Str.anomaSha256
+    OpAnomaResourceCommitment -> Str.anomaResourceCommitment
+    OpAnomaResourceNullifier -> Str.anomaResourceNullifier
+    OpAnomaResourceKind -> Str.anomaResourceKind
+    OpAnomaResourceDelta -> Str.anomaResourceDelta
+    OpAnomaActionDelta -> Str.anomaActionDelta
+    OpAnomaActionsDelta -> Str.anomaActionsDelta
+    OpAnomaProveAction -> Str.anomaProveAction
+    OpAnomaProveDelta -> Str.anomaProveDelta
+    OpAnomaZeroDelta -> Str.anomaZeroDelta
+    OpAnomaAddDelta -> Str.anomaAddDelta
+    OpAnomaSubDelta -> Str.anomaSubDelta
 
 instance PrettyCode UnaryOpcode where
   ppCode = \case
diff --git a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
index 395ea136f3..f30ce9a9e8 100644
--- a/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
+++ b/src/Juvix/Compiler/Tree/Transformation/CheckNoAnoma.hs
@@ -10,23 +10,10 @@ checkNoAnoma = walkT checkNode
   where
     checkNode :: Symbol -> Node -> Sem r ()
     checkNode _ = \case
-      Anoma NodeAnoma {..} -> case _nodeAnomaOpcode of
-        OpAnomaGet -> unsupportedErr "OpAnomaGet"
-        OpAnomaEncode -> unsupportedErr "OpAnomaEncode"
-        OpAnomaDecode -> unsupportedErr "OpAnomaDecode"
-        OpAnomaVerifyDetached -> unsupportedErr "OpAnomaVerifyDetached"
-        OpAnomaSign -> unsupportedErr "OpAnomaSign"
-        OpAnomaSignDetached -> unsupportedErr "OpAnomaSignDetached"
-        OpAnomaVerifyWithMessage -> unsupportedErr "OpAnomaVerifyWithMessage"
-        OpAnomaByteArrayFromAnomaContents -> unsupportedErr "OpAnomaByteArrayFromAnomaContents"
-        OpAnomaByteArrayToAnomaContents -> unsupportedErr "OpAnomaByteArrayToAnomaContents"
-        OpAnomaSha256 -> unsupportedErr "OpAnomaSha256"
-        where
-          unsupportedErr :: Text -> Sem r ()
-          unsupportedErr opName =
-            throw
-              TreeError
-                { _treeErrorMsg = opName <> " is unsupported",
-                  _treeErrorLoc = _nodeAnomaInfo ^. nodeInfoLocation
-                }
+      Anoma NodeAnoma {..} ->
+        throw
+          TreeError
+            { _treeErrorMsg = show _nodeAnomaOpcode <> " is unsupported",
+              _treeErrorLoc = _nodeAnomaInfo ^. nodeInfoLocation
+            }
       _ -> return ()
diff --git a/src/Juvix/Compiler/Tree/Translation/FromCore.hs b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
index 807f129c9b..d642807a01 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromCore.hs
@@ -352,6 +352,17 @@ genCode infoTable fi =
       Core.OpAnomaByteArrayToAnomaContents -> OpAnomaByteArrayToAnomaContents
       Core.OpAnomaByteArrayFromAnomaContents -> OpAnomaByteArrayFromAnomaContents
       Core.OpAnomaSha256 -> OpAnomaSha256
+      Core.OpAnomaResourceCommitment -> OpAnomaResourceCommitment
+      Core.OpAnomaResourceNullifier -> OpAnomaResourceNullifier
+      Core.OpAnomaResourceKind -> OpAnomaResourceKind
+      Core.OpAnomaResourceDelta -> OpAnomaResourceDelta
+      Core.OpAnomaActionDelta -> OpAnomaActionDelta
+      Core.OpAnomaActionsDelta -> OpAnomaActionsDelta
+      Core.OpAnomaProveAction -> OpAnomaProveAction
+      Core.OpAnomaProveDelta -> OpAnomaProveDelta
+      Core.OpAnomaZeroDelta -> OpAnomaZeroDelta
+      Core.OpAnomaAddDelta -> OpAnomaAddDelta
+      Core.OpAnomaSubDelta -> OpAnomaSubDelta
       _ -> impossible
 
     getArgsNum :: Symbol -> Int
diff --git a/src/Juvix/Compiler/Tree/Translation/FromSource.hs b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
index 6c6e4f766c..19534e0d3a 100644
--- a/src/Juvix/Compiler/Tree/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Tree/Translation/FromSource.hs
@@ -156,6 +156,17 @@ parseAnoma =
     <|> parseAnoma' kwAnomaByteArrayToAnomaContents OpAnomaByteArrayToAnomaContents
     <|> parseAnoma' kwAnomaByteArrayFromAnomaContents OpAnomaByteArrayFromAnomaContents
     <|> parseAnoma' kwAnomaSha256 OpAnomaSha256
+    <|> parseAnoma' kwAnomaResourceCommitment OpAnomaResourceCommitment
+    <|> parseAnoma' kwAnomaResourceNullifier OpAnomaResourceNullifier
+    <|> parseAnoma' kwAnomaResourceKind OpAnomaResourceKind
+    <|> parseAnoma' kwAnomaResourceDelta OpAnomaResourceDelta
+    <|> parseAnoma' kwAnomaActionDelta OpAnomaActionDelta
+    <|> parseAnoma' kwAnomaActionsDelta OpAnomaActionsDelta
+    <|> parseAnoma' kwAnomaProveAction OpAnomaProveAction
+    <|> parseAnoma' kwAnomaProveDelta OpAnomaProveDelta
+    <|> parseAnoma' kwAnomaZeroDelta OpAnomaZeroDelta
+    <|> parseAnoma' kwAnomaAddDelta OpAnomaAddDelta
+    <|> parseAnoma' kwAnomaSubDelta OpAnomaSubDelta
 
 parseAnoma' ::
   (Members '[Reader ParserSig, InfoTableBuilder, State LocalParams] r) =>
diff --git a/src/Juvix/Data/Keyword/All.hs b/src/Juvix/Data/Keyword/All.hs
index eef9de8b87..cfd2cadf5b 100644
--- a/src/Juvix/Data/Keyword/All.hs
+++ b/src/Juvix/Data/Keyword/All.hs
@@ -502,6 +502,39 @@ kwByteArrayLength = asciiKw Str.byteArrayLength
 kwAnomaSha256 :: Keyword
 kwAnomaSha256 = asciiKw Str.anomaSha256
 
+kwAnomaResourceCommitment :: Keyword
+kwAnomaResourceCommitment = asciiKw Str.anomaResourceCommitment
+
+kwAnomaResourceNullifier :: Keyword
+kwAnomaResourceNullifier = asciiKw Str.anomaResourceNullifier
+
+kwAnomaResourceKind :: Keyword
+kwAnomaResourceKind = asciiKw Str.anomaResourceKind
+
+kwAnomaResourceDelta :: Keyword
+kwAnomaResourceDelta = asciiKw Str.anomaResourceDelta
+
+kwAnomaActionDelta :: Keyword
+kwAnomaActionDelta = asciiKw Str.anomaActionDelta
+
+kwAnomaActionsDelta :: Keyword
+kwAnomaActionsDelta = asciiKw Str.anomaActionsDelta
+
+kwAnomaProveAction :: Keyword
+kwAnomaProveAction = asciiKw Str.anomaProveAction
+
+kwAnomaProveDelta :: Keyword
+kwAnomaProveDelta = asciiKw Str.anomaProveDelta
+
+kwAnomaZeroDelta :: Keyword
+kwAnomaZeroDelta = asciiKw Str.anomaZeroDelta
+
+kwAnomaAddDelta :: Keyword
+kwAnomaAddDelta = asciiKw Str.anomaAddDelta
+
+kwAnomaSubDelta :: Keyword
+kwAnomaSubDelta = asciiKw Str.anomaSubDelta
+
 delimBraceL :: Keyword
 delimBraceL = mkDelim Str.braceL
 
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index ce8636f925..f40c9d170a 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -392,6 +392,45 @@ anomaByteArrayFromAnomaContents = "anoma-bytearray-from-anoma-contents"
 anomaSha256 :: (IsString s) => s
 anomaSha256 = "anoma-sha256"
 
+anomaDelta :: (IsString s) => s
+anomaDelta = "anoma-delta"
+
+anomaKind :: (IsString s) => s
+anomaKind = "anoma-kind"
+
+anomaResourceCommitment :: (IsString s) => s
+anomaResourceCommitment = "anoma-resource-commitment"
+
+anomaResourceNullifier :: (IsString s) => s
+anomaResourceNullifier = "anoma-resource-nullifier"
+
+anomaResourceKind :: (IsString s) => s
+anomaResourceKind = "anoma-resource-kind"
+
+anomaResourceDelta :: (IsString s) => s
+anomaResourceDelta = "anoma-resource-delta"
+
+anomaActionDelta :: (IsString s) => s
+anomaActionDelta = "anoma-action-delta"
+
+anomaActionsDelta :: (IsString s) => s
+anomaActionsDelta = "anoma-actions-delta"
+
+anomaZeroDelta :: (IsString s) => s
+anomaZeroDelta = "anoma-zero-delta"
+
+anomaAddDelta :: (IsString s) => s
+anomaAddDelta = "anoma-add-delta"
+
+anomaSubDelta :: (IsString s) => s
+anomaSubDelta = "anoma-sub-delta"
+
+anomaProveDelta :: (IsString s) => s
+anomaProveDelta = "anoma-prove-delta"
+
+anomaProveAction :: (IsString s) => s
+anomaProveAction = "anoma-prove-action"
+
 builtinSeq :: (IsString s) => s
 builtinSeq = "seq"
 
@@ -1079,6 +1118,18 @@ cairoEcPoint = "ec_point"
 cairoMkEcPoint :: (IsString s) => s
 cairoMkEcPoint = "mkEcPoint"
 
+anomaResource :: (IsString s) => s
+anomaResource = "anoma-resource"
+
+anomaAction :: (IsString s) => s
+anomaAction = "anoma-action"
+
+anomaMkResource :: (IsString s) => s
+anomaMkResource = "mkResource"
+
+anomaMkAction :: (IsString s) => s
+anomaMkAction = "mkAction"
+
 rustFn :: (IsString s) => s
 rustFn = "fn"
 
diff --git a/test/Anoma/Compilation/Positive.hs b/test/Anoma/Compilation/Positive.hs
index 7531c7ea82..722332c5db 100644
--- a/test/Anoma/Compilation/Positive.hs
+++ b/test/Anoma/Compilation/Positive.hs
@@ -655,5 +655,17 @@ allTests =
                 64
                 5092006196359674779938793937035252249221936503860319648757996882954518215195609232852607160812968472040491493412050369557521935588220586883008001462395444
               ] |]
+          ],
+      mkAnomaCallTest
+        "Test085: Anoma Resource Machine builtins"
+        $(mkRelDir ".")
+        $(mkRelFile "test085.juvix")
+        []
+        $ checkOutput
+          [ [nock| [[[11 22] 110] 0] |],
+            [nock| [10 11] |],
+            [nock| 478793196187462788804451 |],
+            [nock| 418565088612 |],
+            [nock| 0 |]
           ]
     ]
diff --git a/tests/Anoma/Compilation/positive/test085.juvix b/tests/Anoma/Compilation/positive/test085.juvix
new file mode 100644
index 0000000000..33f7393614
--- /dev/null
+++ b/tests/Anoma/Compilation/positive/test085.juvix
@@ -0,0 +1,98 @@
+module test085;
+
+import Stdlib.Prelude open;
+import Stdlib.Debug.Trace open;
+
+-- This definition does not match the spec. For testing purposes only
+builtin anoma-resource
+type Resource :=
+  mkResource@{
+    label : Nat;
+    logic : Nat;
+    ephemeral : Bool;
+    quantity : Nat;
+    data : Pair Nat Nat;
+    nullifier-key : Nat;
+    nonce : Nat;
+    rseed : Nat
+  };
+
+mkResource' (label logic : Nat) {quantity : Nat := 0} : Resource :=
+  mkResource@{
+    label;
+    logic;
+    ephemeral := false;
+    quantity;
+    data := 0, 0;
+    nullifier-key := 0;
+    nonce := 0;
+    rseed := 0
+  };
+
+-- This definition does not match the spec. For testing purposes only
+builtin anoma-action
+type Action := mkAction Nat;
+
+builtin anoma-delta
+axiom Delta : Type;
+
+builtin anoma-kind
+axiom Kind : Type;
+
+builtin anoma-resource-commitment
+axiom commitment : Resource -> Nat;
+
+builtin anoma-resource-nullifier
+axiom nullifier : Resource -> Nat;
+
+builtin anoma-resource-kind
+axiom kind : Resource -> Kind;
+
+builtin anoma-resource-delta
+axiom resourceDelta : Resource -> Delta;
+
+builtin anoma-action-delta
+axiom actionDelta : Action -> Delta;
+
+builtin anoma-actions-delta
+axiom actionsDelta : List Action -> Delta;
+
+builtin anoma-prove-action
+axiom proveAction : Action -> Nat;
+
+builtin anoma-prove-delta
+axiom proveDelta : Delta -> Nat;
+
+builtin anoma-zero-delta
+axiom zeroDelta : Delta;
+
+builtin anoma-add-delta
+axiom addDelta : Delta -> Delta -> Delta;
+
+builtin anoma-sub-delta
+axiom subDelta : Delta -> Delta -> Delta;
+
+main : Delta :=
+  trace
+      (resourceDelta
+        mkResource'@{
+          label := 11;
+          logic := 22;
+          quantity := 55
+        })
+    -- commitment is too slow to be tested
+    -- >-> trace (commitment (mkResource' 0 0))
+    -- nullifier is too slow to be tested
+    -- >-> trace (nullifier (mkResource' 0 0))
+    -- actionDelta is a crash in the nock library so cannot be tested
+    -- >-> trace (actionDelta (mkAction 0))
+    -- actionsDelta is a crash in the nock library so cannot be tested
+    -- >-> trace (actionsDelta [mkAction 0])
+    -- addDelta is a crash in the nock library so cannot be tested
+    -- >-> trace (addDelta zeroDelta zeroDelta)
+    -- subDelta is a crash in the nock library so cannot be tested
+    -- >-> trace (subDelta zeroDelta zeroDelta)
+    >-> trace (kind (mkResource' 10 11))
+    >-> trace (proveAction (mkAction 0))
+    >-> trace (proveDelta zeroDelta)
+    >-> zeroDelta;