diff --git a/deps/cryptol b/deps/cryptol
index 08cd609c4c..34404d7930 160000
--- a/deps/cryptol
+++ b/deps/cryptol
@@ -1 +1 @@
-Subproject commit 08cd609c4c58ebb5a4cd22ad053d8255ce8d1fc5
+Subproject commit 34404d7930d82b8b96c5ccc32d8ae5a7ba033e5e
diff --git a/saw-remote-api/python/poetry.lock b/saw-remote-api/python/poetry.lock
index 9e42ce7fb7..c10a5a223e 100644
--- a/saw-remote-api/python/poetry.lock
+++ b/saw-remote-api/python/poetry.lock
@@ -1,14 +1,14 @@
 [[package]]
 name = "argo-client"
-version = "0.0.9"
+version = "0.0.10"
 description = "A JSON RPC client library."
 category = "main"
 optional = false
-python-versions = ">=3.7"
+python-versions = ">=3.7.0,<4"
 
 [package.dependencies]
-mypy = "*"
-requests = "*"
+requests = ">=2.26.0,<3.0.0"
+urllib3 = ">=1.26.5"
 
 [[package]]
 name = "bitvector"
@@ -28,7 +28,7 @@ python-versions = "*"
 
 [[package]]
 name = "charset-normalizer"
-version = "2.0.7"
+version = "2.0.9"
 description = "The Real First Universal Charset Detector. Open, modern and actively maintained alternative to Chardet."
 category = "main"
 optional = false
@@ -39,14 +39,14 @@ unicode_backport = ["unicodedata2"]
 
 [[package]]
 name = "cryptol"
-version = "2.12.0"
+version = "2.12.2"
 description = "Cryptol client for the Cryptol 2.12 RPC server"
 category = "main"
 optional = false
-python-versions = ">=3.7.0"
+python-versions = ">=3.7.0,<4"
 
 [package.dependencies]
-argo-client = "0.0.9"
+argo-client = "0.0.10"
 BitVector = ">=3.4.9,<4.0.0"
 requests = ">=2.25.1,<3.0.0"
 
@@ -62,7 +62,7 @@ python-versions = ">=3.5"
 name = "mypy"
 version = "0.812"
 description = "Optional static typing for Python"
-category = "main"
+category = "dev"
 optional = false
 python-versions = ">=3.5"
 
@@ -78,7 +78,7 @@ dmypy = ["psutil (>=4.0)"]
 name = "mypy-extensions"
 version = "0.4.3"
 description = "Experimental type system extensions for programs checked with the mypy typechecker."
-category = "main"
+category = "dev"
 optional = false
 python-versions = "*"
 
@@ -104,15 +104,15 @@ use_chardet_on_py3 = ["chardet (>=3.0.2,<5)"]
 name = "typed-ast"
 version = "1.4.3"
 description = "a fork of Python 2 and 3 ast modules with type comment support"
-category = "main"
+category = "dev"
 optional = false
 python-versions = "*"
 
 [[package]]
 name = "typing-extensions"
-version = "4.0.0"
+version = "4.0.1"
 description = "Backported and Experimental Type Hints for Python 3.6+"
-category = "main"
+category = "dev"
 optional = false
 python-versions = ">=3.6"
 
@@ -132,12 +132,12 @@ socks = ["PySocks (>=1.5.6,!=1.5.7,<2.0)"]
 [metadata]
 lock-version = "1.1"
 python-versions = "^3.8"
-content-hash = "2e8d483be348117d70d8a2683748a807483cb4fba322c2be61dfe826bd7ef9fd"
+content-hash = "ffca6578b36152988e9e38f2f828a6807ae038cf3ff2722610a03af90f4b7586"
 
 [metadata.files]
 argo-client = [
-    {file = "argo-client-0.0.9.tar.gz", hash = "sha256:762e16d7428046ecf1d4fd50d877cba9a3c21eac260806030876f76acac81325"},
-    {file = "argo_client-0.0.9-py3-none-any.whl", hash = "sha256:c482e3ba3346c7677fc1c8a470b173ba0d59736d6c628b0193a13b8e3aeeb9f1"},
+    {file = "argo-client-0.0.10.tar.gz", hash = "sha256:a95e07201a5e23758e7bc6b2e1d594c61a71df02ff534ad7a8db32fdb991ed0b"},
+    {file = "argo_client-0.0.10-py3-none-any.whl", hash = "sha256:d86e07bfc421faf9f25be6af2d4a0c7fd2ddef7a759488f6c05baa2ff2c1e390"},
 ]
 bitvector = [
     {file = "BitVector-3.5.0.tar.gz", hash = "sha256:cac2fbccf11e325115827ed7be03e5fd62615227b0bbf3fa5a18a842a221839c"},
@@ -147,12 +147,12 @@ certifi = [
     {file = "certifi-2021.10.8.tar.gz", hash = "sha256:78884e7c1d4b00ce3cea67b44566851c4343c120abd683433ce934a68ea58872"},
 ]
 charset-normalizer = [
-    {file = "charset-normalizer-2.0.7.tar.gz", hash = "sha256:e019de665e2bcf9c2b64e2e5aa025fa991da8720daa3c1138cadd2fd1856aed0"},
-    {file = "charset_normalizer-2.0.7-py3-none-any.whl", hash = "sha256:f7af805c321bfa1ce6714c51f254e0d5bb5e5834039bc17db7ebe3a4cec9492b"},
+    {file = "charset-normalizer-2.0.9.tar.gz", hash = "sha256:b0b883e8e874edfdece9c28f314e3dd5badf067342e42fb162203335ae61aa2c"},
+    {file = "charset_normalizer-2.0.9-py3-none-any.whl", hash = "sha256:1eecaa09422db5be9e29d7fc65664e6c33bd06f9ced7838578ba40d58bdf3721"},
 ]
 cryptol = [
-    {file = "cryptol-2.12.0-py3-none-any.whl", hash = "sha256:32230c361f79bfd621c7c7872d338c8e315d55c368c38730fa792d4626321204"},
-    {file = "cryptol-2.12.0.tar.gz", hash = "sha256:bedde0bc55fff411bfd9575b5fd77890ce855a921340d2e805453c64fbae652e"},
+    {file = "cryptol-2.12.2-py3-none-any.whl", hash = "sha256:d543f2a92b0000f869576c89eeee2fa19ddeb064193a13ce8e55f1e6a388a60b"},
+    {file = "cryptol-2.12.2.tar.gz", hash = "sha256:ca2d84557354387b8f856902e18333fb1b6792cbf0e10173e1b64854af085ec7"},
 ]
 idna = [
     {file = "idna-3.3-py3-none-any.whl", hash = "sha256:84d9dd047ffa80596e0f246e2eab0b391788b0503584e8945f2368256d2735ff"},
@@ -223,8 +223,8 @@ typed-ast = [
     {file = "typed_ast-1.4.3.tar.gz", hash = "sha256:fb1bbeac803adea29cedd70781399c99138358c26d05fcbd23c13016b7f5ec65"},
 ]
 typing-extensions = [
-    {file = "typing_extensions-4.0.0-py3-none-any.whl", hash = "sha256:829704698b22e13ec9eaf959122315eabb370b0884400e9818334d8b677023d9"},
-    {file = "typing_extensions-4.0.0.tar.gz", hash = "sha256:2cdf80e4e04866a9b3689a51869016d36db0814d84b8d8a568d22781d45d27ed"},
+    {file = "typing_extensions-4.0.1-py3-none-any.whl", hash = "sha256:7f001e5ac290a0c0401508864c7ec868be4e701886d5b573a9528ed3973d9d3b"},
+    {file = "typing_extensions-4.0.1.tar.gz", hash = "sha256:4ca091dea149f945ec56afb48dae714f21e8692ef22a395223bcd328961b6a0e"},
 ]
 urllib3 = [
     {file = "urllib3-1.26.7-py2.py3-none-any.whl", hash = "sha256:c4fdf4019605b6e5423637e01bc9fe4daef873709a7973e195ceba0a62bbc844"},
diff --git a/saw-remote-api/python/pyproject.toml b/saw-remote-api/python/pyproject.toml
index a5c8c0dae4..c0793d0e35 100644
--- a/saw-remote-api/python/pyproject.toml
+++ b/saw-remote-api/python/pyproject.toml
@@ -14,8 +14,8 @@ include = [
 python = "^3.8"
 requests = "^2.25.1"
 BitVector = "^3.4.9"
-cryptol = "2.12.0" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
-argo-client = "~0.0.6"
+cryptol = "2.12.2" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
+argo-client = "0.0.10"
 
 [tool.poetry.dev-dependencies]
 mypy = "^0.812"
diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py
index 309383ef9c..4a2a412368 100644
--- a/saw-remote-api/python/saw_client/__init__.py
+++ b/saw-remote-api/python/saw_client/__init__.py
@@ -633,8 +633,7 @@ def prove(goal: cryptoltypes.CryptolJSON,
     argument.
     """
     conn = __get_designated_connection()
-    res = conn.prove(cryptoltypes.to_cryptol(goal),
-                     proof_script.to_json()).result()
+    res = conn.prove(goal, proof_script.to_json()).result()
     pr = ProofResult()
     if res['status'] == 'valid':
         pr.valid = True
diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py
index c2d80afad1..d6d0263cac 100644
--- a/saw-remote-api/python/saw_client/commands.py
+++ b/saw-remote-api/python/saw_client/commands.py
@@ -177,7 +177,7 @@ def __init__(
             goal : cryptoltypes.CryptolJSON,
             script : ProofScript,
             timeout : Optional[float]) -> None:
-        params = {'goal': goal,
+        params = {'goal': cryptoltypes.to_cryptol(goal),
                   'script': script}
         super(Prove, self).__init__('SAW/prove', params, connection, timeout=timeout)
 
diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py
index 1c327f792b..5d5ff39a0c 100644
--- a/saw-remote-api/python/saw_client/crucible.py
+++ b/saw-remote-api/python/saw_client/crucible.py
@@ -1,10 +1,11 @@
 from abc import ABCMeta, abstractmethod
 from cryptol import cryptoltypes
+from cryptol.quoting import to_cryptol_str_customf
 from .utils import deprecated
 from dataclasses import dataclass
 import dataclasses
 import re
-from typing import Any, Dict, List, Optional, Set, Union, overload
+from typing import Any, Dict, List, Tuple, Optional, Set, Union, overload
 from typing_extensions import Literal
 import inspect
 import uuid
@@ -12,6 +13,8 @@
 from .llvm_type import *
 from .jvm_type import *
 
+JSON = Union[None, bool, int, float, str, Dict, Tuple, List]
+
 class SetupVal(metaclass=ABCMeta):
     """Represent a ``SetupValue`` in SawScript, which "corresponds to
     values that can occur during symbolic execution, which includes both 'Term'
@@ -19,7 +22,7 @@ class SetupVal(metaclass=ABCMeta):
     (both structures and arrays)."
     """
     @abstractmethod
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         """JSON representation for this ``SetupVal`` (i.e., how it is represented in expressions, etc).
 
         N.B., should be a JSON object with a ``'setup value'`` field with a unique tag which the
@@ -50,7 +53,7 @@ class NamedSetupVal(SetupVal):
     """Represents those ``SetupVal``s which are a named reference to some value, e.e., a variable
     or reference to allocated memory."""
     @abstractmethod
-    def to_init_json(self) -> Any:
+    def to_init_json(self) -> JSON:
         """JSON representation with the information for those ``SetupVal``s which require additional
         information to initialize/allocate them vs that which is required later to reference them.
 
@@ -69,20 +72,19 @@ def __init__(self, code : Union[str, cryptoltypes.CryptolJSON]):
             self.expression = code
 
     def __call__(self, *args : cryptoltypes.CryptolJSON) -> 'CryptolTerm':
-        out_term = self.expression
-        for a in args:
-            out_term = cryptoltypes.CryptolApplication(out_term, a)
-
-        return CryptolTerm(out_term)
+        return CryptolTerm(cryptoltypes.CryptolApplication(self.expression, *args))
 
     def __repr__(self) -> str:
         return f"CryptolTerm({self.expression!r})"
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'Cryptol', 'expression': cryptoltypes.to_cryptol(self.expression)}
 
-    def __to_cryptol__(self, ty : Any) -> Any:
-        return self.expression.__to_cryptol__(ty)
+    def __to_cryptol__(self) -> cryptoltypes.JSON:
+        return self.expression.__to_cryptol__()
+
+    def __to_cryptol_str__(self) -> str:
+        return self.expression.__to_cryptol_str__()
 
 class FreshVar(NamedSetupVal):
     __name : Optional[str]
@@ -92,10 +94,13 @@ def __init__(self, spec : 'Contract', type : Union['LLVMType', 'JVMType'], sugge
         self.spec = spec
         self.type = type
 
-    def __to_cryptol__(self, ty : Any) -> Any:
-        return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__(ty)
+    def __to_cryptol__(self) -> cryptoltypes.JSON:
+        return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol__()
+
+    def __to_cryptol_str__(self) -> str:
+        return cryptoltypes.CryptolLiteral(self.name()).__to_cryptol_str__()
 
-    def to_init_json(self) -> Any:
+    def to_init_json(self) -> JSON:
         #FIXME it seems we don't actually use two names ever... just the one...do we actually need both?
         name = self.name()
         return {"server name": name,
@@ -107,17 +112,9 @@ def name(self) -> str:
             self.__name = self.spec.get_fresh_name()
         return self.__name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'named', 'name': self.name()}
 
-    def __gt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm:
-        gt = CryptolTerm("(>)")
-        return gt(self, other)
-
-    def __lt__(self, other : cryptoltypes.CryptolJSON) -> CryptolTerm:
-        lt = CryptolTerm("(<)")
-        return lt(self, other)
-
 
 class Allocated(NamedSetupVal):
     name : Optional[str]
@@ -130,7 +127,7 @@ def __init__(self, spec : 'Contract', type : Union['LLVMType','JVMType'], *,
         self.mutable = mutable
         self.alignment = alignment
 
-    def to_init_json(self) -> Any:
+    def to_init_json(self) -> JSON:
         if self.name is None:
             self.name = self.spec.get_fresh_name()
         return {"server name": self.name,
@@ -138,7 +135,7 @@ def to_init_json(self) -> Any:
                 "mutable": self.mutable,
                 "alignment": self.alignment}
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         if self.name is None:
             self.name = self.spec.get_fresh_name()
         return {'setup value': 'named', 'name': self.name}
@@ -149,7 +146,7 @@ class StructVal(SetupVal):
     def __init__(self, fields : List[SetupVal]) -> None:
         self.fields = fields
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'tuple', 'elements': [fld.to_json() for fld in self.fields]}
 
 class ElemVal(SetupVal):
@@ -160,7 +157,7 @@ def __init__(self, base : SetupVal, index : int) -> None:
         self.base = base
         self.index = index
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'element lvalue',
                 'base': self.base.to_json(), 'index': self.index}
 
@@ -172,7 +169,7 @@ def __init__(self, base : SetupVal, field_name : str) -> None:
         self.base = base
         self.field_name = field_name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'field',
                 'base': self.base.to_json(), 'field': self.field_name}
 
@@ -182,7 +179,7 @@ class GlobalInitializerVal(SetupVal):
     def __init__(self, name : str) -> None:
         self.name = name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'global initializer', 'name': self.name}
 
 class GlobalVarVal(SetupVal):
@@ -191,11 +188,11 @@ class GlobalVarVal(SetupVal):
     def __init__(self, name : str) -> None:
         self.name = name
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'global lvalue', 'name': self.name}
 
 class NullVal(SetupVal):
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'null'}
 
 class ArrayVal(SetupVal):
@@ -204,7 +201,7 @@ class ArrayVal(SetupVal):
     def __init__(self, elements : List[SetupVal]) -> None:
         self.elements = elements
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'setup value': 'array',
                 'elements': [element.to_json() for element in self.elements]}
 
@@ -242,7 +239,7 @@ class Condition:
     def __init__(self, condition : CryptolTerm) -> None:
         self.cryptol_term = condition
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return cryptoltypes.to_cryptol(self.cryptol_term)
 
 
@@ -257,7 +254,7 @@ def __init__(self, pointer : SetupVal, target : SetupVal, *,
         self.check_target_type = check_target_type
         self.condition = condition
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         check_target_type_json: Optional[Dict[str, Any]]
         if self.check_target_type is None:
             check_target_type_json = None
@@ -296,11 +293,11 @@ class GhostValue:
     """A class containing the statement that a given ghost variable should have the
     value given by a Cryptol expression.
     """
-    def __init__(self, name: str, value: CryptolTerm) -> None:
+    def __init__(self, name: str, value: cryptoltypes.CryptolJSON) -> None:
         self.name = name
         self.value = value
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {"server name": self.name,
                 "value": cryptoltypes.to_cryptol(self.value)}
 
@@ -314,7 +311,7 @@ class State:
     points_to_bitfield : List[PointsToBitfield] = dataclasses.field(default_factory=list)
     ghost_values : List[GhostValue] = dataclasses.field(default_factory=list)
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return {'variables': [v.to_init_json() for v in self.fresh],
                 'conditions': [c.to_json() for c in self.conditions],
                 'allocated': [a.to_init_json() for a in self.allocated],
@@ -330,7 +327,7 @@ def to_json(self) -> Any:
 
 @dataclass
 class Void:
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         return None
 
 void = Void()
@@ -362,7 +359,7 @@ class Contract:
     __definition_lineno : Optional[int]
     __definition_filename : Optional[str]
     __unique_id : uuid.UUID
-    __cached_json : Optional[Any]
+    __cached_json : JSON
 
     def __init__(self) -> None:
         self.__pre_state = State(self)
@@ -482,7 +479,7 @@ def points_to_bitfield(self, pointer : SetupVal, field_name : str,
         else:
             raise Exception("wrong state")
 
-    def ghost_value(self, var: GhostVariable, value: CryptolTerm) -> None:
+    def ghost_value(self, var: GhostVariable, value: cryptoltypes.CryptolJSON) -> None:
         """Declare that the given ghost variable should have a value specified by the given Cryptol expression.
 
         Usable either before or after `execute_func`.
@@ -524,6 +521,12 @@ def precondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.Crypto
         else:
             raise Exception("preconditions must be specified before execute_func is called in the contract")
 
+    def precondition_f(self, s : str) -> None:
+        """Declares a precondition using a ``cry_f``-style format string, i.e.
+        ``precondition_f(...)`` is equivalent to ``precondition(cry_f(...))``"""
+        expression = to_cryptol_str_customf(s, frames=1, filename="<precondition_f>")
+        return self.precondition(expression)
+
     def postcondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.CryptolJSON]) -> None:
         """Establishes ``proposition`` as a postcondition for the function ```Contract```
         being specified.
@@ -538,6 +541,12 @@ def postcondition(self, proposition : Union[str, CryptolTerm, cryptoltypes.Crypt
         else:
             raise Exception("postconditions must be specified after execute_func is called in the contract")
 
+    def postcondition_f(self, s : str) -> None:
+        """Declares a postcondition using a ``cry_f``-style format string, i.e.
+        ``postcondition_f(...)`` is equivalent to ``postcondition(cry_f(...))``"""
+        expression = to_cryptol_str_customf(s, frames=1, filename="<postcondition_f>")
+        return self.postcondition(expression)
+
     def returns(self, val : Union[Void,SetupVal]) -> None:
         if self.__state == 'post':
             if self.__returns is None:
@@ -547,6 +556,12 @@ def returns(self, val : Union[Void,SetupVal]) -> None:
         else:
             raise ValueError("Not in postcondition")
 
+    def returns_f(self, s : str) -> None:
+        """Declares a return value using a ``cry_f``-style format string, i.e.
+        ``returns_f(...)`` is equivalent to ``returns(cry_f(...))``"""
+        expression = to_cryptol_str_customf(s, frames=1, filename="<returns_f>")
+        return self.returns(CryptolTerm(expression))
+
     def lemma_name(self, hint  : Optional[str] = None) -> str:
         if hint is None:
             hint = self.__class__.__name__
@@ -563,7 +578,7 @@ def definition_lineno(self) -> Optional[int]:
     def definition_filename(self) -> Optional[str]:
         return self.__definition_filename
 
-    def to_json(self) -> Any:
+    def to_json(self) -> JSON:
         if self.__cached_json is not None:
             return self.__cached_json
         else:
@@ -608,12 +623,49 @@ def global_var(name: str) -> SetupVal:
     """Returns a pointer to the named global ``name`` (i.e., a ``GlobalVarVal``)."""
     return GlobalVarVal(name)
 
-# FIXME Is `Any` too permissive here -- can we be a little more precise?
-def cryptol(data : Any) -> 'CryptolTerm':
-    """Constructs a Cryptol value from ``data`` (i.e., a ``CryptolTerm``, which is also a ``SetupVal``).
-
-    ``data`` should be a string literal representing Cryptol syntax or the result of a Cryptol-realted server computation."""
-    return CryptolTerm(data)
+def cry(s : str) -> CryptolTerm:
+    """Embed a string of Cryptol syntax as a ``CryptolTerm`` (which is also a
+       ``SetupVal``) - also see ``cry_f``."""
+    return CryptolTerm(s)
+
+def cry_f(s : str) -> CryptolTerm:
+    """Embed a string of Cryptol syntax as a ``CryptolTerm`` (which is also a
+       ``SetupVal``), where the given string is parsed as an f-string, and the
+       values within brackets are converted to Cryptol syntax using
+       ``to_cryptol_str`` from the Cryptol Python library.
+
+       Like f-strings, values in brackets (``{``, ``}``) are parsed as python
+       expressions in the caller's context of local and global variables, and
+       to include a literal bracket in the final string, it must be doubled
+       (i.e. ``{{`` or ``}}``). The latter is needed when using explicit type
+       application or record syntax. For example, if ``x = [0,1]`` then
+       ``cry_f('length `{{2}} {x}')`` is equal to ``cry('length `{2} [0,1]')``
+       and ``cry_f('{{ x = {x} }}')`` is equal to ``cry('{ x = [0,1] }')``.
+
+       When formatting Cryptol, it is recomended to use this function rather
+       than any of Python's built-in methods of string formatting (e.g.
+       f-strings, ``str.format``) as the latter will not always produce valid
+       Cryptol syntax. Specifically, this function differs from these methods
+       in the cases of ``BV``s, string literals, function application (this
+       function will add parentheses as needed), and dicts. For example,
+       ``cry_f('{ {"x": 5, "y": 4} }')`` equals ``cry('{x = 5, y = 4}')``
+       but ``f'{ {"x": 5, "y": 4} }'`` equals ``'{"x": 5, "y": 4}'``. Only
+       the former is valid Cryptol syntax for a record.
+       
+       Note that any conversion or format specifier will always result in the
+       argument being rendered as a Cryptol string literal with the conversion
+       and/or formating applied. For example, `cry('f {5}')` is equal to
+       ``cry('f 5')`` but ``cry_f('f {5!s}')`` is equal to ``cry(`f "5"`)``
+       and ``cry_f('f {5:+.2%}')`` is equal to ``cry('f "+500.00%"')``.
+
+       :example:
+
+       >>> x = BV(size=7, value=1)
+       >>> y = cry_f('fun1 {x}')
+       >>> cry_f('fun2 {y}')
+       'fun2 (fun1 (1 : [7]))'
+    """
+    return CryptolTerm(to_cryptol_str_customf(s, frames=1))
 
 def array(*elements: SetupVal) -> SetupVal:
     """Returns an array with the provided ``elements`` (i.e., an ``ArrayVal``).
diff --git a/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py b/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py
index d93049516d..e977e3c556 100644
--- a/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py
+++ b/saw-remote-api/python/tests/saw-in-progress/HMAC/spec/HMAC.py
@@ -1,9 +1,8 @@
 import os
 import os.path
 from cryptol.cryptoltypes import to_cryptol
-from saw import *
-from saw.llvm import Contract, LLVMType, LLVMArrayType, uint8_t, uint32_t, void, SetupVal, FreshVar, cryptol, struct
-import saw.llvm_types as ty
+from saw_client import *
+from saw_client.llvm import *
 from env_server import *
 
 # N.B., transliteration from HMAC.saw
@@ -29,8 +28,8 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, *, re
     
     :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh
              variable will be assigned ``name`` if provided/available.)"""
-    var = c.declare_var(ty, name)
-    ptr = c.alloc(c, ty, points_to=var, read_only=read_only)
+    var = c.fresh_var(ty, name)
+    ptr = c.alloc(ty, points_to=var, read_only=read_only)
     return (var, ptr)
 
 # TODO(AMK) Um... what is this:
@@ -89,16 +88,16 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None, *, re
 
 
 def setup_hash_state(c : Contract, pstate : SetupVal) -> Tuple[Any, FreshVar]:
-    alg0 = c.fresh_var(ty.i32, "alg")
-    h0 = c.fresh_var(ty.array(8, ty.i64), "h0")
-    Nl0 = c.fresh_var(ty.i64, "Nl")
-    Nh0 = c.fresh_var(ty.i64, "Nh")
-    u0 = c.fresh_var(ty.array(16, ty.i64), "u")
-    num0 = c.fresh_var(ty.i32, "h0")
-    is_ready_for_input0 = c.fresh_var(ty.i8, "is_ready_for_input")
-    currently_in_hash0 = c.fresh_var(ty.i64, "currently_in_hash")
-    md_len0 = c.fresh_var(ty.i32, "md_len")
-    (_, pimpl) = ptr_to_fresh(c, ty.alias('struct.s2n_hash'), "impl", read_only=True)
+    alg0 = c.fresh_var(i32, "alg")
+    h0 = c.fresh_var(array_ty(8, i64), "h0")
+    Nl0 = c.fresh_var(i64, "Nl")
+    Nh0 = c.fresh_var(i64, "Nh")
+    u0 = c.fresh_var(array_ty(16, i64), "u")
+    num0 = c.fresh_var(i32, "h0")
+    is_ready_for_input0 = c.fresh_var(i8, "is_ready_for_input")
+    currently_in_hash0 = c.fresh_var(i64, "currently_in_hash")
+    md_len0 = c.fresh_var(i32, "md_len")
+    (_, pimpl) = ptr_to_fresh(c, alias_ty('struct.s2n_hash'), "impl", read_only=True)
     c.points_to(pstate, 
         struct(
             pimpl,
diff --git a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
index a97cbe4465..435ad18110 100755
--- a/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
+++ b/saw-remote-api/python/tests/saw-in-progress/drbg/drbg.py
@@ -1,15 +1,16 @@
 #!/usr/bin/env python3
 import os
 import os.path
-from saw import *
-from saw.llvm import Contract
-from saw.proofscript import yices
-from cryptol import cry, cryptoltypes
+from saw_client import *
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, array_ty, alias_ty, i8, i32, i64
+from saw_client.proofscript import yices, ProofScript
+from cryptol import cryptoltypes
 #from saw.dashboard import Dashboard
 
 dir_path = os.path.dirname(os.path.realpath(__file__))
-conn = connect("cabal -v0 run exe:saw-remote-api socket")
-view(DebugLog(err=None))
+connect("cabal -v0 run exe:saw-remote-api socket")
+view(DebugLog()) #err=None
 view(LogResults())
 #view(Dashboard(path=__file__))
 
@@ -23,13 +24,13 @@
 mod = llvm_load_module(bcname)
 
 def bytes_type(size):
-    return llvm_types.array(size, llvm_types.i8)
+    return array_ty(size, i8)
 
 blocksize = 16 # blocklen / 8
 keysize = 16 # keylen / 8
 seedsize = 32
 
-blob_type = llvm_types.alias('struct.s2n_blob')
+blob_type = alias_ty('struct.s2n_blob')
 ctx_type = bytes_type(keysize)
 
 def alloc_bytes(spec, n):
@@ -39,16 +40,16 @@ def alloc_blob(spec, n):
     p = spec.alloc(type=blob_type, read_only=True)
     datap = alloc_bytes(spec, n)
     spec.points_to(llvm.field(p, "data"), datap)
-    spec.points_to(llvm.field(p, "size"), llvm.cryptol("`{n}:[32]".format(n=n)))
-    spec.points_to(llvm.field(p, "allocated"), llvm.cryptol("0:[32]"))
-    spec.points_to(llvm.field(p, "growable"), llvm.cryptol("0:[8]"))
+    spec.points_to(llvm.field(p, "size"), cry_f("`{n}:[32]"))
+    spec.points_to(llvm.field(p, "allocated"), cry("0:[32]"))
+    spec.points_to(llvm.field(p, "growable"), cry("0:[8]"))
     return (p, datap)
 
 def alloc_blob_readonly(spec, n):
     p = spec.alloc(type=blob_type, read_only=True)
-    datap = spec.alloc(llvm_types.array(n, llvm_types.i8), read_only = True)
+    datap = spec.alloc(array_ty(n, i8), read_only = True)
     spec.points_to(llvm.field(p, "data"), datap)
-    spec.points_to(llvm.field(p, "size"), llvm.cryptol("`{n}: [32]".format(n=n)))
+    spec.points_to(llvm.field(p, "size"), cry_f("`{n}: [32]"))
     return(p, datap)
 
 def alloc_init(spec, ty, v):
@@ -77,25 +78,16 @@ def ptr_to_fresh_readonly(spec, n, ty):
     return (x, p)
 
 def drbg_state(spec, n):
-    state = spec.alloc(llvm_types.alias("struct.s2n_drbg"))
+    state = spec.alloc(alias_ty("struct.s2n_drbg"))
     (key, keyp) = ptr_to_fresh(spec, "key", ctx_type)
-    bytes_used = spec.fresh_var(llvm_types.i64, n+"bytes_used")
-    mixes = spec.fresh_var(llvm_types.i64, n+"mixes")
+    bytes_used = spec.fresh_var(i64, n+"bytes_used")
+    mixes = spec.fresh_var(i64, n+"mixes")
     v = spec.fresh_var(bytes_type(blocksize), n+"v")
     spec.points_to(llvm.field(state, "bytes_used"), bytes_used)
     spec.points_to(llvm.field(state, "mixes"), mixes)
     spec.points_to(llvm.field(state, "ctx"), keyp)
     spec.points_to(llvm.field(state, "v"), v)
-    return (state, keyp,
-            "{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}".format(bytes_used=bytes_used.name(), key=key.name(), v=v.name()))
-    #return (state, keyp,
-    #        llvm.cryptol("{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}".format(bytes_used=bytes_used.name(), key=key.name(), v=v.name())))
-    #return (state, keyp, { 'bytes_used': bytes_used , 'ctx': { 'key': llvm.cryptol("join {}".format(key.name())) } , v: llvm.cryptol("join {}".format(v)) })
-
-    #       , {{ { bytes_used = bytes_used
-    #           , ctx = { key = join key }
-    #           , v = join v
-    #           } }}
+    return (state, keyp, cry_f("{{ bytes_used = {bytes_used}, ctx = {{ key = join {key} }}, v = join {v} }}"))
 
 class blob_zero_spec(Contract):
     def __init__(self,n):
@@ -105,8 +97,8 @@ def __init__(self,n):
     def specification(self):
         (p, datap) = alloc_blob(self, self.n)
         self.execute_func(p)
-        self.points_to(datap, llvm.cryptol("zero:[{n}][8]".format(n=self.n)))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.points_to(datap, cry_f("zero:[{self.n}][8]"))
+        self.returns(cry("0:[32]"))
 
 class increment_drbg_counter_spec(Contract):
     def specification(self):
@@ -114,16 +106,16 @@ def specification(self):
         v = self.fresh_var(bytes_type(blocksize), "v")
         self.points_to(datap, v)
         self.execute_func(p)
-        self.points_to(datap, llvm.cryptol("split ((join {v}) +1): [{blocksize}][8]".format(v=v.name(),blocksize=blocksize)))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.points_to(datap, cry_f("split ((join {v}) +1): [{blocksize}][8]"))
+        self.returns(cry("0:[32]"))
 
 class bytes_used_spec(Contract):
     def specification(self):
         (sp, keyp, s) = drbg_state(self,"drbg")
-        bytes_used = alloc_init(self, llvm_types.i64, llvm.cryptol("0:[64]"))
+        bytes_used = alloc_init(self, i64, cry("0:[64]"))
         self.execute_func(sp, bytes_used)
-        self.points_to(bytes_used, llvm.cryptol("{s}.bytes_used".format(s=s)))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.points_to(bytes_used, cry_f("{s}.bytes_used"))
+        self.returns(cry("0:[32]"))
 
 class block_encrypt_spec(Contract):
     def specification(self):
@@ -131,8 +123,8 @@ def specification(self):
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", bytes_type(blocksize))
         outp = alloc_bytes(self, blocksize)
         self.execute_func(keyp, msgp, outp)
-        self.points_to(outp, llvm.cryptol("encrypt_128 {key} {msg}".format(key=key.name(), msg=msg.name())))
-        self.returns(llvm.cryptol("0 : [32]"))
+        self.points_to(outp, cry_f("encrypt_128 {key} {msg}"))
+        self.returns(cry("0 : [32]"))
 
 class encryptUpdate_spec(Contract):
     def __init__(self,n):
@@ -143,12 +135,12 @@ def specification(self):
         # but it is constant in the DRBG cryptol specification.
         (key, keyp) = ptr_to_fresh_readonly(self, "key", ctx_type)
         outp = alloc_bytes(self, self.n)
-        lenp = alloc_init(self, llvm_types.i32, llvm.cryptol("{} : [32]".format(self.n)))
+        lenp = alloc_init(self, i32, cry_f("{self.n} : [32]"))
         (msg, msgp) = ptr_to_fresh_readonly(self, "msg", (bytes_type(self.n)))
-        self.execute_func(keyp, outp, lenp, msgp, llvm.cryptol("`{blocksize} : [32]".format(blocksize=blocksize)))
-        self.points_to(outp, llvm.cryptol("encrypt_128 {} {}".format(key.name(), msg.name())))
-        self.points_to(lenp, llvm.cryptol("{} : [32]".format(self.n)))
-        self.returns (llvm.cryptol("1 : [32]"))
+        self.execute_func(keyp, outp, lenp, msgp, cry_f("`{blocksize} : [32]"))
+        self.points_to(outp, cry_f("encrypt_128 {key} {msg}"))
+        self.points_to(lenp, cry_f("{self.n} : [32]"))
+        self.returns (cry("1 : [32]"))
 
 class bits_spec(Contract):
     def __init__(self, n):
@@ -158,19 +150,19 @@ def specification(self):
         (sp, keyp, s) = drbg_state(self, "drbg")
         (outp, datap) = alloc_blob(self, self.n)
         self.execute_func(sp, outp)
-        res = "drbg_generate_internal `{{n={n}*8}} ({s})".format(n=self.n,s=s)
+        res = cry_f("drbg_generate_internal `{{n={self.n}*8}} {s}")
         # Remove some of the parens here to get really bad error messages
-        c = llvm.cryptol("split (({res}).0) : [{n}][8]".format(res=res, n=self.n))
+        c = cry("split (({res}).0) : [{self.n}][8]")
         self.points_to(datap, c)
-        ensure_drbg_state(self, sp, keyp, "({res}).1".format(res=res))
-        self.returns (llvm.cryptol(" 0 : [32] "))
+        ensure_drbg_state(self, sp, keyp, cry_f("{res}.1"))
+        self.returns (cry(" 0 : [32] "))
 
 def ensure_drbg_state(spec, p, keyp, s):
-    spec.points_to(llvm.field(p, "bytes_used"), llvm.cryptol("({s}).bytes_used".format(s=s)))
+    spec.points_to(llvm.field(p, "bytes_used"), cry_f("{s}.bytes_used"))
     spec.points_to(llvm.field(p, "ctx"), keyp)
-    spec.points_to(keyp, llvm.cryptol("split (({s}).ctx.key) : [{keysize}][8]".format(s=s,keysize=keysize)))
-    spec.points_to(llvm.field(p, "v"), llvm.cryptol("split (({s}).v) : [{blocksize}][8]".format(s=s,blocksize=blocksize)))
-    mixes = spec.fresh_var(llvm_types.i64, "mixes")
+    spec.points_to(keyp, cry_f("split ({s}.ctx.key) : [{keysize}][8]"))
+    spec.points_to(llvm.field(p, "v"), cry_f("split ({s}.v) : [{blocksize}][8]"))
+    mixes = spec.fresh_var(i64, "mixes")
     spec.points_to(llvm.field(p, "mixes"), mixes)
 
 #////////////////////////////////////////////////////////////////////////////////
@@ -179,7 +171,7 @@ def ensure_drbg_state(spec, p, keyp, s):
 
 class getenv_spec(Contract):
     def specification(self):
-        p = self.alloc(llvm_types.i8)
+        p = self.alloc(i8)
         self.execute_func(p)
         self.returns(llvm.null)
 
@@ -212,15 +204,15 @@ class cipher_cleanup_spec(Contract):
     def specification(self):
         ctx = self.alloc(ctx_type)
         self.execute_func(ctx)
-        self.points_to(ctx, llvm.cryptol("zero : [{keysize}][8]".format(keysize=keysize)))
-        self.returns(llvm.cryptol("1:[32]"))
+        self.points_to(ctx, cry_f("zero : [{keysize}][8]"))
+        self.returns(cry("1:[32]"))
 
 class cipher_key_length_spec(Contract):
     def specification(self):
         ctx = self.alloc(ctx_type, read_only = True)
         self.execute_func(ctx)
         # Specialized to AES-128 for now
-        self.returns(llvm.cryptol("16:[32]"))
+        self.returns(cry("16:[32]"))
 
 class encryptInit_spec(Contract):
     def specification(self):
@@ -233,7 +225,7 @@ def specification(self):
         #self.execute_func(ctx, stp, llvm.null, keyp, llvm.null)
         self.execute_func(ctx, llvm.null, llvm.null, keyp, llvm.null)
         self.points_to(ctx, key)
-        self.returns(llvm.cryptol("1:[32]"))
+        self.returns(cry("1:[32]"))
 
 class get_public_random_spec(Contract):
     def __init__(self):
@@ -243,13 +235,13 @@ def specification(self):
         (p, datap) = alloc_blob(self, seedsize)
         self.execute_func(p)
         # TODO: blocked on 'fake_entropy'
-        #self.points_to(datap, llvm.cryptol("split fake_entropy : [{seedsize}][8]".format(seedsize=seedsize)))
-        self.returns(llvm.cryptol("0: [32]"))
+        #self.points_to(datap, cry_f("split fake_entropy : [{seedsize}][8]"))
+        self.returns(cry("0: [32]"))
 
 class supports_rdrand_spec(Contract):
     def specification(self):
         self.execute_func()
-        r = self.fresh_var(llvm_types.i8, "supports_rdrand")
+        r = self.fresh_var(i8, "supports_rdrand")
         self.returns(r)
 
 #////////////////////////////////////////////////////////////////////////////////
@@ -283,7 +275,7 @@ def specification(self):
         self.points_to(datap, data)
         self.execute_func(sp, providedp)
         ensure_drbg_state(self, sp, keyp, "drbg_update (join {data}) ({s})".format(data=data.name(), s=s))
-        self.returns(llvm.cryptol("0:[32]"))
+        self.returns(cry("0:[32]"))
 
 class seed_spec(Contract):
     def __init__(self, n):
@@ -298,7 +290,7 @@ def specification(self):
         expr = "drbg_reseed ({s}) (fake_entropy) (join ({data}))".format(s=s,
                 data=data.name())
         ensure_drbg_state(self, sp, keyp, expr)
-        self.returns(llvm.cryptol("0:[32]"))
+        self.returns(cry("0:[32]"))
 
 zero_ov_block = llvm_verify(mod, 's2n_blob_zero', blob_zero_spec(blocksize))
 zero_ov_seed = llvm_verify(mod, "s2n_blob_zero", blob_zero_spec(seedsize))
@@ -308,14 +300,15 @@ def specification(self):
 llvm_verify(mod, "s2n_drbg_bytes_used", bytes_used_spec())
 
 
-blk_enc_ov = llvm_verify(mod, "s2n_drbg_block_encrypt", contract = block_encrypt_spec(), lemmas = [encryptUpdate_ov], script = yices(unints=['block_encrypt']))
+blk_enc_ov = llvm_verify(mod, "s2n_drbg_block_encrypt", contract = block_encrypt_spec(),
+        lemmas = [encryptUpdate_ov], script = ProofScript([yices(unints=['block_encrypt'])]))
 
 bits_ov = llvm_verify(mod, "s2n_drbg_bits", contract = bits_spec(seedsize),
-        lemmas = [inc_ov, encryptUpdate_ov, blk_enc_ov], script = yices(['block_encrypt']))
+        lemmas = [inc_ov, encryptUpdate_ov, blk_enc_ov], script = ProofScript([yices(['block_encrypt'])]))
 
 update_ov = llvm_verify(mod, "s2n_drbg_update", lemmas = [bits_ov,
     encryptInit_ov, aes_128_ecb_ov, cipher_key_length_ov], contract=
-    update_spec(seedsize), script = yices(["block_encrypt"]))
+    update_spec(seedsize), script = ProofScript([yices(["block_encrypt"])]))
 
 # TODO: this lemma cannot be proven yet, see drbg-helpers.cry for the definition
 # of "fake_entropy"
diff --git a/saw-remote-api/python/tests/saw/test_alloc_aligned.py b/saw-remote-api/python/tests/saw/test_alloc_aligned.py
index a82212b21f..e1881e14ce 100644
--- a/saw-remote-api/python/tests/saw/test_alloc_aligned.py
+++ b/saw-remote-api/python/tests/saw/test_alloc_aligned.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, FreshVar, SetupVal, cryptol, struct, LLVMType, array_ty, i8, i64
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, FreshVar, SetupVal, struct, LLVMType, array_ty, i8, i64
 from typing import Tuple
 
 
@@ -16,7 +17,7 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tu
 
 
 def int_to_64_cryptol(length: int):
-    return cryptol("`{i}:[64]".format(i=length))
+    return cry_f("`{length}:[64]")
 
 
 def buffer_type(length: int) -> LLVMType:
diff --git a/saw-remote-api/python/tests/saw/test_basic_java.py b/saw-remote-api/python/tests/saw/test_basic_java.py
index 066b78f0fe..a4ab2be61d 100644
--- a/saw-remote-api/python/tests/saw/test_basic_java.py
+++ b/saw-remote-api/python/tests/saw/test_basic_java.py
@@ -3,7 +3,8 @@
 
 import saw_client as saw
 
-from saw_client.jvm import Contract, java_int, cryptol
+from saw_client.crucible import cry, cry_f
+from saw_client.jvm import Contract, java_int
 
 class Add(Contract):
     def __init__(self) -> None:
@@ -15,7 +16,7 @@ def specification(self) -> None:
 
         self.execute_func(x, y)
 
-        self.returns(cryptol("(+)")(x,y))
+        self.returns_f("{x} + {y}")
 
 class Double(Contract):
     def __init__(self) -> None:
@@ -26,7 +27,7 @@ def specification(self) -> None:
 
         self.execute_func(x)
 
-        self.returns(cryptol("(+)")(x,x))
+        self.returns_f("{x} + {x}")
 
 class AddTest(unittest.TestCase):
     def test_add(self):
diff --git a/saw-remote-api/python/tests/saw/test_ghost.py b/saw-remote-api/python/tests/saw/test_ghost.py
index be831b47de..c88b11832f 100644
--- a/saw-remote-api/python/tests/saw/test_ghost.py
+++ b/saw-remote-api/python/tests/saw/test_ghost.py
@@ -1,20 +1,21 @@
 import saw_client as saw
-from saw_client.llvm import Contract, CryptolTerm, cryptol, void, i32, GhostVariable
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, CryptolTerm, void, i32, GhostVariable
 
 import unittest
 from pathlib import Path
 
 def pre_counter(contract: Contract, counter: GhostVariable):
     n = contract.fresh_var(i32, "n")
-    contract.precondition(n < cryptol("128"))
+    contract.precondition_f("{n} < 128")
     contract.ghost_value(counter, n)
     return n
 
 def post_counter(contract: Contract, counter: GhostVariable, n: CryptolTerm):
-    contract.ghost_value(counter, cryptol("(+)")(n, cryptol("1")))
+    contract.ghost_value(counter, cry_f("{n} + 1"))
 
 class GetAndIncrementContract(Contract):
-    def __init__(self, counter: str) -> None:
+    def __init__(self, counter: GhostVariable) -> None:
         super().__init__()
         self.counter = counter
 
@@ -25,17 +26,17 @@ def specification(self) -> None:
         self.returns(n)
 
 class FContract(Contract):
-    def __init__(self, counter: str) -> None:
+    def __init__(self, counter: GhostVariable) -> None:
         super().__init__()
         self.counter = counter
 
     def specification(self) -> None:
         n = pre_counter(self, self.counter)
         i = self.fresh_var(i32, "i")
-        self.precondition(i < cryptol("512"))
+        self.precondition_f("{i} < 512")
         self.execute_func(i)
         post_counter(self, self.counter, n)
-        self.returns(cryptol("(*)")(i, n))
+        self.returns_f("{i} * {n}")
 
 class GhostTest(unittest.TestCase):
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
index 99b613612f..c48055023e 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_assert_null.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cryptol, null, i32
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, null, i32
 
 
 class FContract1(Contract):
@@ -10,14 +11,14 @@ def specification(self):
 
         self.execute_func(p)
 
-        self.returns(cryptol("0 : [32]"))
+        self.returns(cry("0 : [32]"))
 
 
 class FContract2(Contract):
     def specification(self):
         self.execute_func(null())
 
-        self.returns(cryptol("1 : [32]"))
+        self.returns(cry("1 : [32]"))
 
 
 class LLVMAssertNullTest(unittest.TestCase):
diff --git a/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py b/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
index cea240f5dd..0045ce6a62 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_lax_pointer_ordering.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, FreshVar, LLVMType, SetupVal, array_ty, cryptol, i64, void
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, FreshVar, LLVMType, SetupVal, array_ty, i64, void
 from saw_client.option import LaxPointerOrdering
 
 
@@ -29,7 +30,7 @@ def specification(self):
 
         self.execute_func(c_ptr, a_ptr, b_ptr)
 
-        self.points_to(c_ptr, cryptol(f'zipWith`{{ {LEN} }} (+) {a.name()} {b.name()}'))
+        self.points_to(c_ptr, cry_f('zipWith`{{ {LEN} }} (+) {a} {b}'))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_pointer.py b/saw-remote-api/python/tests/saw/test_llvm_pointer.py
index a1a80aabbd..3721a18a7a 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_pointer.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_pointer.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cryptol, void, i8, ptr_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, void, i8, ptr_ty
 
 
 class FContract(Contract):
@@ -12,7 +13,7 @@ def specification(self):
 
         p = self.alloc(i8)
         self.points_to(x, p)
-        self.points_to(p, cryptol("42 : [8]"))
+        self.points_to(p, cry("42 : [8]"))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
index 10f3f5e6d7..c8c7bf2ade 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_points_to_bitfield.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, LLVMIntType, alias_ty, cryptol, i8, void
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, LLVMIntType, alias_ty, i8, void
 from saw_client.option import LaxLoadsAndStores
 
 
@@ -17,7 +18,7 @@ def specification(self):
 
         self.execute_func(ss)
 
-        self.returns(cryptol(f'zext {z.name()} : [8]'))
+        self.returns_f('zext {z} : [8]')
 
 
 class GetYContract(Contract):
@@ -38,7 +39,7 @@ def specification(self):
 
         self.execute_func(ss, z)
 
-        self.points_to_bitfield(ss, 'x2', cryptol(f'drop {z.name()} : [2]'))
+        self.points_to_bitfield(ss, 'x2', cry_f('drop {z} : [2]'))
         self.returns(void)
 
 
@@ -47,7 +48,7 @@ def specification(self):
         ss = self.alloc(alias_ty('struct.s'))
         z = self.fresh_var(i2, 'z')
 
-        self.execute_func(ss, cryptol(f'zext {z.name()} : [8]'))
+        self.execute_func(ss, cry_f('zext {z} : [8]'))
 
         self.points_to_bitfield(ss, 'x2', z)
         self.returns(void)
diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct.py b/saw-remote-api/python/tests/saw/test_llvm_struct.py
index ff583ea03d..66eca1cf3c 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_struct.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_struct.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, SetupVal, FreshVar, cryptol, struct, LLVMType, void, array_ty, i32, alias_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, SetupVal, FreshVar, struct, LLVMType, void, array_ty, i32, alias_ty
 
 
 def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]:
@@ -22,7 +23,7 @@ def specification(self):
         self.execute_func(p)
 
         self.points_to(p, struct(x_p))
-        self.points_to(x_p, cryptol('[0, 0] : [2][32]'))
+        self.points_to(x_p, cry('[0, 0] : [2][32]'))
         self.returns(void)
 
 
@@ -33,7 +34,7 @@ def specification(self):
 
         self.execute_func(p)
 
-        self.returns(cryptol(f'{x.name()}@0 + {x.name()}@1'))
+        self.returns_f('{x}@0 + {x}@1')
 
 
 class IdContract(Contract):
diff --git a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
index 86feb33502..6c1679e96d 100644
--- a/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
+++ b/saw-remote-api/python/tests/saw/test_llvm_struct_type.py
@@ -1,7 +1,8 @@
 from pathlib import Path
 import unittest
 from saw_client import *
-from saw_client.llvm import Contract, cryptol, struct, void, i32, array_ty, struct_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, struct, void, i32, array_ty, struct_ty
 
 
 class FContract(Contract):
@@ -12,7 +13,7 @@ def specification(self):
 
         self.execute_func(pw)
 
-        self.points_to(pw, struct(cryptol('zero:[2][4][32]')))
+        self.points_to(pw, struct(cry('zero:[2][4][32]')))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_points_to_at_type.py b/saw-remote-api/python/tests/saw/test_points_to_at_type.py
index 6991a31114..e072ccb609 100644
--- a/saw-remote-api/python/tests/saw/test_points_to_at_type.py
+++ b/saw-remote-api/python/tests/saw/test_points_to_at_type.py
@@ -2,7 +2,8 @@
 import unittest
 from saw_client import *
 from saw_client.exceptions import VerificationError
-from saw_client.llvm import Contract, LLVMType, PointerType, cryptol, void, i32, array_ty
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, LLVMType, PointerType, void, i32, array_ty
 from typing import Union
 
 
@@ -18,7 +19,7 @@ def specification(self) -> None:
 
         self.execute_func(p)
 
-        self.points_to(p, cryptol("{x} # {x}".format(x=x.name())))
+        self.points_to(p, cry_f("{x} # {x}"))
         self.returns(void)
 
 
diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py
index 45afeff63d..29cca88576 100644
--- a/saw-remote-api/python/tests/saw/test_salsa20.py
+++ b/saw-remote-api/python/tests/saw/test_salsa20.py
@@ -2,7 +2,8 @@
 import unittest
 from cryptol.cryptoltypes import to_cryptol
 from saw_client import *
-from saw_client.llvm import Contract, void, SetupVal, FreshVar, cryptol, i8, i32, LLVMType, LLVMArrayType
+from saw_client.crucible import cry, cry_f
+from saw_client.llvm import Contract, void, SetupVal, FreshVar, i8, i32, LLVMType, LLVMArrayType
 from saw_client.proofscript import z3
 
 
@@ -23,7 +24,7 @@ def oneptr_update_func(c : Contract, ty : LLVMType, fn_name : str) -> None:
 
     c.execute_func(x_p)
 
-    c.points_to(x_p, cryptol(fn_name)(x))
+    c.points_to(x_p, cry(fn_name)(x))
     c.returns(void)
     return None
 
@@ -32,12 +33,12 @@ class RotlContract(Contract):
     def specification(self) -> None:
         value = self.fresh_var(i32, "value")
         shift = self.fresh_var(i32, "shift")
-        self.precondition(shift > cryptol("0"))
-        self.precondition(shift < cryptol("32"))
+        self.precondition_f("{shift} > 0")
+        self.precondition_f("{shift} < 32")
 
         self.execute_func(value, shift)
 
-        self.returns(cryptol("(<<<)")(value, shift))
+        self.returns_f("{value} <<< {shift}")
 
 
 
@@ -55,11 +56,11 @@ def specification(self) -> None:
 
         self.execute_func(y0_p, y1_p, y2_p, y3_p)
 
-        res = cryptol("quarterround")([y0, y1, y2, y3])
-        self.points_to(y0_p, cryptol("(@)")(res, cryptol("0")))
-        self.points_to(y1_p, cryptol("(@)")(res, cryptol("1")))
-        self.points_to(y2_p, cryptol("(@)")(res, cryptol("2")))
-        self.points_to(y3_p, cryptol("(@)")(res, cryptol("3")))
+        res = cry_f("quarterround {[y0, y1, y2, y3]}")
+        self.points_to(y0_p, cry_f("{res}@0"))
+        self.points_to(y1_p, cry_f("{res}@1"))
+        self.points_to(y2_p, cry_f("{res}@2"))
+        self.points_to(y3_p, cry_f("{res}@3"))
         self.returns(void)
 
 
@@ -102,7 +103,7 @@ def specification(self):
         self.execute_func(k_p, n_p, ks_p)
 
         self.returns(void)
-        self.points_to(ks_p, cryptol("Salsa20_expansion`{a=2}")((k, n)))
+        self.points_to(ks_p, cry_f("Salsa20_expansion `{{a=2}} {(k, n)}"))
 
 
 
@@ -116,10 +117,10 @@ def specification(self):
         (v, v_p) = ptr_to_fresh(self, LLVMArrayType(i8, 8))
         (m, m_p) = ptr_to_fresh(self, LLVMArrayType(i8, self.size))
 
-        self.execute_func(k_p, v_p, cryptol('0 : [32]'), m_p, cryptol(f'{self.size!r} : [32]'))
+        self.execute_func(k_p, v_p, cry('0 : [32]'), m_p, cry_f('{self.size} : [32]'))
 
-        self.points_to(m_p, cryptol("Salsa20_encrypt")((k, v, m)))
-        self.returns(cryptol('0 : [32]'))
+        self.points_to(m_p, cry_f("Salsa20_encrypt {(k, v, m)}"))
+        self.returns(cry('0 : [32]'))
 
 class Salsa20EasyTest(unittest.TestCase):
     def test_salsa20(self):