diff --git a/Cargo.lock b/Cargo.lock
index e6ef7dc45..9b0986b5a 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -505,6 +505,7 @@ dependencies = [
 name = "hax-engine-names"
 version = "0.1.0-pre.1"
 dependencies = [
+ "hax-lib",
  "hax-lib-protocol",
 ]
 
diff --git a/cli/driver/src/driver.rs b/cli/driver/src/driver.rs
index 88faeb1c2..5120911ec 100644
--- a/cli/driver/src/driver.rs
+++ b/cli/driver/src/driver.rs
@@ -41,7 +41,7 @@ use callbacks_wrapper::*;
 use features::*;
 
 use const_format::formatcp;
-use hax_cli_options::{Command, ENV_VAR_OPTIONS_FRONTEND};
+use hax_cli_options::{BackendOptions, Command, ExporterCommand, ENV_VAR_OPTIONS_FRONTEND};
 
 use rustc_driver::{Callbacks, Compilation};
 use rustc_interface::{interface, Queries};
@@ -165,6 +165,13 @@ fn main() {
                 "--cfg".into(),
                 hax_lib_macros_types::HAX_CFG_OPTION_NAME.into(),
             ])
+            .chain(match &options.command {
+                Some(Command::ExporterCommand(ExporterCommand::Backend(BackendOptions {
+                    backend,
+                    ..
+                }))) => vec!["--cfg".into(), format!("hax_backend_{backend}")],
+                _ => vec![],
+            })
             .chain(features.into_iter().map(|s| format!("-Zcrate-attr={}", s)))
             .chain(rustc_args[1..].iter().cloned())
             .collect();
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
index c90877015..41058c99c 100644
--- a/engine/backends/coq/coq/coq_backend.ml
+++ b/engine/backends/coq/coq/coq_backend.ml
@@ -39,6 +39,7 @@ module SubtypeToInputLanguage
              and type for_loop = Features.Off.for_loop
              and type while_loop = Features.Off.while_loop
              and type for_index_loop = Features.Off.for_index_loop
+             and type quote = Features.Off.quote
              and type state_passing_loop = Features.Off.state_passing_loop) =
 struct
   module FB = InputLanguage
diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
index 5b3f14fed..260ea21e9 100644
--- a/engine/backends/coq/ssprove/ssprove_backend.ml
+++ b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -39,6 +39,7 @@ module SubtypeToInputLanguage
              and type monadic_action = Features.Off.monadic_action
              and type arbitrary_lhs = Features.Off.arbitrary_lhs
              and type nontrivial_lhs = Features.Off.nontrivial_lhs
+             and type quote = Features.Off.quote
              and type block = Features.Off.block) =
 struct
   module FB = InputLanguage
diff --git a/engine/backends/easycrypt/easycrypt_backend.ml b/engine/backends/easycrypt/easycrypt_backend.ml
index 1977f7cc0..115ebda06 100644
--- a/engine/backends/easycrypt/easycrypt_backend.ml
+++ b/engine/backends/easycrypt/easycrypt_backend.ml
@@ -57,6 +57,7 @@ module RejectNotEC (FA : Features.T) = struct
         let block = reject
         let for_loop = reject
         let while_loop = reject
+        let quote = reject
         let construct_base _ _ = Features.On.construct_base
         let for_index_loop _ _ = Features.On.for_index_loop
 
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index b49966631..870df9abe 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -11,6 +11,7 @@ include
       include On.Slice
       include On.Macro
       include On.Construct_base
+      include On.Quote
     end)
     (struct
       let backend = Diagnostics.Backend.FStar
@@ -52,6 +53,7 @@ struct
         include Features.SUBTYPE.On.Construct_base
         include Features.SUBTYPE.On.Slice
         include Features.SUBTYPE.On.Macro
+        include Features.SUBTYPE.On.Quote
       end)
 
   let metadata = Phase_utils.Metadata.make (Reject (NotInBackendLang backend))
@@ -85,6 +87,9 @@ let doc_to_string : PPrint.document -> string =
 let term_to_string : F.AST.term -> string =
   FStar_Parser_ToDocument.term_to_document >> doc_to_string
 
+let pat_to_string : F.AST.pattern -> string =
+  FStar_Parser_ToDocument.pat_to_document >> doc_to_string
+
 let decl_to_string : F.AST.decl -> string =
   FStar_Parser_ToDocument.decl_to_document >> doc_to_string
 
@@ -568,6 +573,14 @@ struct
              kind = UnsupportedMacro { id = [%show: global_ident] macro };
              span = e.span;
            }
+    | Quote { contents; _ } ->
+        List.map
+          ~f:(function
+            | `Verbatim code -> code
+            | `Expr e -> pexpr e |> term_to_string
+            | `Pat p -> ppat p |> pat_to_string)
+          contents
+        |> String.concat |> F.term_of_string
     | _ -> .
 
   and parm { arm = { arm_pat; body } } = (ppat arm_pat, None, pexpr body)
@@ -1359,6 +1372,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
   Phases.Reject.RawOrMutPointer(Features.Rust)
+  |> Phases.Transform_hax_lib_inline
   |> Phases.Drop_sized_trait
   |> Phases.Simplify_question_marks
   |> Phases.And_mut_defsite
diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml
index 2b765ddbe..983990ebc 100644
--- a/engine/backends/proverif/proverif_backend.ml
+++ b/engine/backends/proverif/proverif_backend.ml
@@ -11,6 +11,7 @@ include
       include On.Question_mark
       include On.Early_exit
       include On.Slice
+      include On.Quote
       include On.Construct_base
     end)
     (struct
@@ -35,6 +36,7 @@ module SubtypeToInputLanguage
              and type slice = Features.On.slice
              and type question_mark = Features.On.question_mark
              and type macro = Features.On.macro
+             and type quote = Features.On.quote
              and type construct_base = Features.On.construct_base
     (* and type as_pattern = Features.Off.as_pattern *)
     (* and type nontrivial_lhs = Features.Off.nontrivial_lhs *)
@@ -883,6 +885,7 @@ module DepGraphR = Dependencies.Make (Features.Rust)
 module TransformToInputLanguage =
   [%functor_application
     Phases.Reject.RawOrMutPointer(Features.Rust)
+    |> Phases.Transform_hax_lib_inline
     |> Phases.Simplify_question_marks
     |> Phases.And_mut_defsite
     |> Phases.Reconstruct_for_loops
diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml
index 9992b46ba..bb03c837f 100644
--- a/engine/lib/ast.ml
+++ b/engine/lib/ast.ml
@@ -258,6 +258,12 @@ functor
         }
       | Closure of { params : pat list; body : expr; captures : expr list }
       | EffectAction of { action : F.monadic_action; argument : expr }
+      | Quote of {
+          contents : [ `Verbatim of string | `Expr of expr | `Pat of pat ] list;
+          witness : F.quote;
+        }
+          (** A quotation is an inlined piece of backend code
+              interleaved with Rust code *)
 
     and expr = { e : expr'; span : span; typ : ty }
 
diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml
index 369901163..fed3bebf4 100644
--- a/engine/lib/ast_utils.ml
+++ b/engine/lib/ast_utils.ml
@@ -54,6 +54,12 @@ module Make (F : Features.T) = struct
     let mut_borrow (e : expr) : expr option =
       match e.e with Borrow { kind = Mut _; e; _ } -> Some e | _ -> None
 
+    let borrow (e : expr) : expr option =
+      match e.e with Borrow { e; _ } -> Some e | _ -> None
+
+    let block (e : expr) : expr option =
+      match e.e with Block (e, _) -> Some e | _ -> None
+
     let deref (e : expr) : expr option =
       match e.e with
       | App { f = { e = GlobalVar (`Primitive Deref); _ }; args = [ e ]; _ } ->
diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml
index db23d9006..64fc30019 100644
--- a/engine/lib/ast_visitors.ml
+++ b/engine/lib/ast_visitors.ml
@@ -434,6 +434,17 @@ functor
               in
               let argument = self#visit_expr env record_payload.argument in
               EffectAction { action; argument }
+          | Quote { contents; witness } ->
+              let contents =
+                self#visit_list
+                  (fun env -> function
+                    | `Verbatim code -> `Verbatim code
+                    | `Expr e -> `Expr (self#visit_expr env e)
+                    | `Pat p -> `Pat (self#visit_pat env p))
+                  env contents
+              in
+              let witness = self#visit_feature_quote env witness in
+              Quote { contents; witness }
 
         method visit_expr (env : 'env) (this : expr) : expr =
           let e = self#visit_expr' env this.e in
@@ -863,6 +874,8 @@ functor
         method visit_feature_nontrivial_lhs
             : 'env -> F.nontrivial_lhs -> F.nontrivial_lhs =
           fun _ x -> x
+
+        method visit_feature_quote : 'env -> F.quote -> F.quote = fun _ x -> x
       end
 
     class virtual ['self] mapreduce =
@@ -1448,6 +1461,22 @@ functor
               in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               (EffectAction { action; argument }, reduce_acc)
+          | Quote { contents; witness } ->
+              let list, reduce_acc =
+                self#visit_list
+                  (fun env -> function
+                    | `Verbatim code -> (`Verbatim code, self#zero)
+                    | `Expr e ->
+                        let e, acc = self#visit_expr env e in
+                        (`Expr e, acc)
+                    | `Pat p ->
+                        let p, acc = self#visit_pat env p in
+                        (`Pat p, acc))
+                  env contents
+              in
+              let witness, reduce_acc' = self#visit_feature_quote env witness in
+              let reduce_acc = self#plus reduce_acc reduce_acc' in
+              (Quote { contents; witness }, reduce_acc)
 
         method visit_expr (env : 'env) (this : expr) : expr * 'acc =
           let e, reduce_acc = self#visit_expr' env this.e in
@@ -2061,6 +2090,9 @@ functor
         method visit_feature_nontrivial_lhs
             : 'env -> F.nontrivial_lhs -> F.nontrivial_lhs * 'acc =
           fun _ x -> (x, self#zero)
+
+        method visit_feature_quote : 'env -> F.quote -> F.quote * 'acc =
+          fun _ x -> (x, self#zero)
       end
 
     class virtual ['self] reduce =
@@ -2570,6 +2602,18 @@ functor
               let reduce_acc' = self#visit_expr env record_payload.argument in
               let reduce_acc = self#plus reduce_acc reduce_acc' in
               reduce_acc
+          | Quote { contents; witness } ->
+              let reduce_acc =
+                self#visit_list
+                  (fun env -> function
+                    | `Verbatim code -> self#zero
+                    | `Expr e -> self#visit_expr env e
+                    | `Pat p -> self#visit_pat env p)
+                  env contents
+              in
+              let reduce_acc' = self#visit_feature_quote env witness in
+              let reduce_acc = self#plus reduce_acc reduce_acc' in
+              reduce_acc
 
         method visit_expr (env : 'env) (this : expr) : 'acc =
           let reduce_acc = self#visit_expr' env this.e in
@@ -3086,5 +3130,8 @@ functor
 
         method visit_feature_nontrivial_lhs : 'env -> F.nontrivial_lhs -> 'acc =
           fun _ _ -> self#zero
+
+        method visit_feature_quote : 'env -> F.quote -> 'acc =
+          fun _ _ -> self#zero
       end
   end
diff --git a/engine/lib/features.ml b/engine/lib/features.ml
index 301eb1755..260c08d0e 100644
--- a/engine/lib/features.ml
+++ b/engine/lib/features.ml
@@ -22,6 +22,7 @@ loop,
   construct_base,
   monadic_action,
   monadic_binding,
+  quote,
   block]
 
 module Full = On
@@ -35,6 +36,7 @@ module Rust = struct
   include Off.Monadic_action
   include Off.Monadic_binding
   include Off.State_passing_loop
+  include Off.Quote
 end
 
 let _ = Enumeration.all
diff --git a/engine/lib/generic_printer/generic_printer.ml b/engine/lib/generic_printer/generic_printer.ml
index 0c8ff1d65..ff1f6754e 100644
--- a/engine/lib/generic_printer/generic_printer.ml
+++ b/engine/lib/generic_printer/generic_printer.ml
@@ -225,6 +225,14 @@ module Make (F : Features.T) (View : Concrete_ident.VIEW_API) = struct
                 |> wrap_parens
             | MacroInvokation _ -> print#assertion_failure "MacroInvokation"
             | EffectAction _ -> print#assertion_failure "EffectAction"
+            | Quote { contents; _ } ->
+                List.map
+                  ~f:(function
+                    | `Verbatim code -> string code
+                    | `Expr e -> print#expr_at Expr_Quote e
+                    | `Pat p -> print#pat_at Expr_Quote p)
+                  contents
+                |> concat
             | App _ | Construct _ -> super#expr' ctx e
 
         method expr_monadic_let
diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml
index 27f497fc9..0a1e67629 100644
--- a/engine/lib/generic_printer/generic_printer_base.ml
+++ b/engine/lib/generic_printer/generic_printer_base.ml
@@ -31,6 +31,7 @@ type ast_position =
   | Expr_Let_lhs
   | Expr_Let_rhs
   | Expr_Let_body
+  | Expr_Quote
   | Expr_Match_scrutinee
   | Expr_QuestionMark
   | Expr_Borrow
diff --git a/engine/lib/phases/phase_drop_references.ml b/engine/lib/phases/phase_drop_references.ml
index f68292e0f..4e4727695 100644
--- a/engine/lib/phases/phase_drop_references.ml
+++ b/engine/lib/phases/phase_drop_references.ml
@@ -68,7 +68,8 @@ struct
 
     and dexpr' (span : span) (e : A.expr') : B.expr' =
       match (UA.unbox_underef_expr { e; span; typ = UA.never_typ }).e with
-      | [%inline_arms If + Literal + Array + Block + QuestionMark] -> auto
+      | [%inline_arms If + Literal + Array + Block + QuestionMark + Quote] ->
+          auto
       | Construct { constructor; is_record; is_struct; fields; base } ->
           Construct
             {
diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.ml b/engine/lib/phases/phase_transform_hax_lib_inline.ml
new file mode 100644
index 000000000..879c273f3
--- /dev/null
+++ b/engine/lib/phases/phase_transform_hax_lib_inline.ml
@@ -0,0 +1,134 @@
+open! Prelude
+open! Ast
+
+module%inlined_contents Make (F : Features.T) = struct
+  open Ast
+  module FA = F
+
+  module FB = struct
+    include F
+    include Features.On.Quote
+  end
+
+  include
+    Phase_utils.MakeBase (F) (FB)
+      (struct
+        let phase_id = Diagnostics.Phase.CfIntoMonads
+      end)
+
+  module Implem : ImplemT.T = struct
+    let metadata = metadata
+
+    module UA = Ast_utils.Make (F)
+    module UB = Ast_utils.Make (FB)
+    module Visitors = Ast_visitors.Make (FB)
+
+    module S = struct
+      module A = FA
+      module B = FB
+      include Features.SUBTYPE.Id
+
+      let quote _ _ = Features.On.quote
+    end
+
+    [%%inline_defs dmutability]
+
+    (** Patterns are "stored" in a
+        [match None { Some <PAT> => (), _ => () }]
+        dummy expression. *)
+    let extract_pattern (e : B.expr) : B.pat option =
+      match e.e with
+      | Block
+          ( {
+              e =
+                Match
+                  {
+                    arms =
+                      [
+                        {
+                          arm =
+                            {
+                              arm_pat =
+                                { p = PConstruct { args = [ arg ]; _ }; _ };
+                              _;
+                            };
+                          _;
+                        };
+                        _;
+                      ];
+                    _;
+                  };
+              _;
+            },
+            _ ) ->
+          Some arg.pat
+      | _ -> None
+
+    (** Extracts the first global_ident found in a pattern *)
+    let first_global_ident (pat : B.pat) : global_ident option =
+      UB.Reducers.collect_global_idents#visit_pat () pat |> Set.choose
+
+    let rec dexpr' span (expr : A.expr') : B.expr' =
+      match expr with
+      | App { f = { e = GlobalVar f; _ }; args = [ payload ]; _ }
+        when Global_ident.eq_name Hax_lib__inline f ->
+          let bindings, str = dexpr payload |> UB.collect_let_bindings in
+          let str =
+            match
+              UB.Expect.(block >> Option.bind ~f:borrow >> Option.bind ~f:deref)
+                str
+            with
+            | Some { e = Literal (String str); _ } -> str
+            | _ ->
+                Error.assertion_failure span
+                  "Malformed call to 'inline': cannot find string payload."
+          in
+          let code =
+            List.map bindings ~f:(fun (pat, e) ->
+                match
+                  UB.Expect.pbinding_simple pat
+                  |> Option.map ~f:(fun ((i, _) : Local_ident.t * _) -> i.name)
+                with
+                | Some "_constructor" ->
+                    let id =
+                      extract_pattern e
+                      |> Option.bind ~f:first_global_ident
+                      |> Option.value_exn
+                    in
+                    `Expr { e with e = GlobalVar id }
+                | Some "_pat" ->
+                    let pat = extract_pattern e |> Option.value_exn in
+                    `Pat pat
+                | _ -> `Expr e)
+          in
+          let verbatim = split_str ~on:"SPLIT_QUOTE" str in
+          let contents =
+            let rec f verbatim
+                (code :
+                  [ `Verbatim of string | `Expr of B.expr | `Pat of B.pat ] list)
+                =
+              match (verbatim, code) with
+              | s :: s', code :: code' -> `Verbatim s :: code :: f s' code'
+              | [ s ], [] -> [ `Verbatim s ]
+              | [], [] -> []
+              | _ ->
+                  Error.assertion_failure span
+                  @@ "Malformed call to 'inline'." ^ "\nverbatim="
+                  ^ [%show: string list] verbatim
+                  ^ "\ncode="
+                  ^ [%show:
+                      [ `Verbatim of string | `Expr of B.expr | `Pat of B.pat ]
+                      list] code
+            in
+            f verbatim code
+          in
+          Quote { contents; witness = Features.On.quote }
+      | [%inline_arms "dexpr'.*"] -> auto
+      [@@inline_ands bindings_of dexpr - dexpr']
+
+    [%%inline_defs "Item.*"]
+  end
+
+  include Implem
+end
+[@@add "subtype.ml"]
diff --git a/engine/lib/phases/phase_transform_hax_lib_inline.mli b/engine/lib/phases/phase_transform_hax_lib_inline.mli
new file mode 100644
index 000000000..87c94a9e6
--- /dev/null
+++ b/engine/lib/phases/phase_transform_hax_lib_inline.mli
@@ -0,0 +1,31 @@
+(** This phase transforms nodes like:
+    {@rust[
+    hax_lib::inline({
+      let _KIND = ...;
+      ...
+      let _KIND = ...;
+      "payload"
+    })
+    ]}
+
+    into [hax_lib::inline("payload'")] where [payload'] is a string
+    with all the binding names substituted.
+
+    Note: above `_KIND` can be `_expr`, `_pat` or `_constructor`.
+*)
+
+module Make (F : Features.T) : sig
+  include module type of struct
+    module FB = struct
+      include F
+      include Features.On.Quote
+    end
+
+    module A = Ast.Make (F)
+    module B = Ast.Make (FB)
+    module ImplemT = Phase_utils.MakePhaseImplemT (A) (B)
+    module FA = F
+  end
+
+  include ImplemT.T
+end
diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml
index a048f3700..369a0b005 100644
--- a/engine/lib/print_rust.ml
+++ b/engine/lib/print_rust.ml
@@ -317,6 +317,7 @@ module Raw = struct
     | Closure { params; body; _ } ->
         let params = List.map ~f:ppat params |> concat ~sep:!"," in
         !"(|" & params & !"| {" & pexpr body & !"})"
+    | Quote _ -> !"quotation!(..)"
   (* | _ -> "todo!()" *)
 
   and plhs (e : lhs) span =
diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml
index 07923e089..ec5533df4 100644
--- a/engine/lib/side_effect_utils.ml
+++ b/engine/lib/side_effect_utils.ml
@@ -486,6 +486,7 @@ struct
                 ~context:(Other "collect_and_hoist_effects_object") ~span:e.span
                 (Unimplemented
                    { issue_id = None; details = Some "EffectAction" })
+          | Quote _ -> (e, m#zero)
       end
 
     let collect_and_hoist_effects (e : expr) : expr * SideEffects.t =
diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml
index 9c71c975a..c793efdea 100644
--- a/engine/lib/subtype.ml
+++ b/engine/lib/subtype.ml
@@ -260,6 +260,14 @@ struct
             body = dexpr body;
             captures = List.map ~f:dexpr captures;
           }
+    | Quote { contents; witness } ->
+        let f = function
+          | `Verbatim code -> `Verbatim code
+          | `Expr e -> `Expr (dexpr e)
+          | `Pat p -> `Pat (dpat p)
+        in
+        Quote
+          { contents = List.map ~f contents; witness = S.quote span witness }
 
   and dloop_kind (span : span) (k : A.loop_kind) : B.loop_kind =
     match k with
diff --git a/engine/names/Cargo.toml b/engine/names/Cargo.toml
index fc8405984..5213e4707 100644
--- a/engine/names/Cargo.toml
+++ b/engine/names/Cargo.toml
@@ -10,4 +10,5 @@ readme.workspace = true
 description = "Dummy crate containing all the Rust names the hax engine should be aware of"
 
 [dependencies]
-hax-lib-protocol = {path = "../../hax-lib-protocol"}
\ No newline at end of file
+hax-lib-protocol = {path = "../../hax-lib-protocol"}
+hax-lib = {path = "../../hax-lib"}
\ No newline at end of file
diff --git a/engine/names/src/lib.rs b/engine/names/src/lib.rs
index 7b067434b..6cf7ff9ef 100644
--- a/engine/names/src/lib.rs
+++ b/engine/names/src/lib.rs
@@ -39,6 +39,8 @@ fn dummy_hax_concrete_ident_wrapper<I: core::iter::Iterator<Item = u8>>(x: I, mu
         Ok(())
     }
 
+    let _ = hax_lib::inline("");
+
     const _: () = {
         use core::{cmp::*, ops::*};
         fn arith<
diff --git a/examples/Cargo.lock b/examples/Cargo.lock
index def235e1f..08ecadb86 100644
--- a/examples/Cargo.lock
+++ b/examples/Cargo.lock
@@ -20,6 +20,13 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
 
+[[package]]
+name = "barrett"
+version = "0.1.0"
+dependencies = [
+ "hax-lib",
+]
+
 [[package]]
 name = "binread"
 version = "2.2.0"
@@ -174,12 +181,6 @@ dependencies = [
  "crypto-common",
 ]
 
-[[package]]
-name = "dyn-clone"
-version = "1.0.16"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "545b22097d44f8a9581187cdf93de7a71e4722bf51200cfaba810865b49a495d"
-
 [[package]]
 name = "either"
 version = "1.9.0"
@@ -222,6 +223,9 @@ checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
 [[package]]
 name = "hax-lib"
 version = "0.1.0-pre.1"
+dependencies = [
+ "hax-lib-macros",
+]
 
 [[package]]
 name = "hax-lib-macros"
@@ -240,7 +244,6 @@ version = "0.1.0-pre.1"
 dependencies = [
  "proc-macro2",
  "quote",
- "schemars",
  "serde",
  "serde_json",
  "uuid",
@@ -315,6 +318,14 @@ version = "1.0.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "af150ab688ff2122fcef229be89cb50dd66af9e01a4ff320cc137eecc9bacc38"
 
+[[package]]
+name = "kyber_compress"
+version = "0.1.0"
+dependencies = [
+ "hax-lib",
+ "hax-lib-macros",
+]
+
 [[package]]
 name = "lazy_static"
 version = "1.4.0"
@@ -497,30 +508,6 @@ version = "1.0.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1ad4cc8da4ef723ed60bced201181d83791ad433213d8c24efffda1eec85d741"
 
-[[package]]
-name = "schemars"
-version = "0.8.16"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "45a28f4c49489add4ce10783f7911893516f15afe45d015608d41faca6bc4d29"
-dependencies = [
- "dyn-clone",
- "schemars_derive",
- "serde",
- "serde_json",
-]
-
-[[package]]
-name = "schemars_derive"
-version = "0.8.16"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c767fd6fa65d9ccf9cf026122c1b555f2ef9a4f0cea69da4d7dbc3e258d30967"
-dependencies = [
- "proc-macro2",
- "quote",
- "serde_derive_internals",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "serde"
 version = "1.0.192"
@@ -550,17 +537,6 @@ dependencies = [
  "syn 2.0.39",
 ]
 
-[[package]]
-name = "serde_derive_internals"
-version = "0.26.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "85bf8229e7920a9f636479437026331ce11aa132b4dde37d121944a44d6e5f3c"
-dependencies = [
- "proc-macro2",
- "quote",
- "syn 1.0.109",
-]
-
 [[package]]
 name = "serde_json"
 version = "1.0.108"
diff --git a/examples/Cargo.toml b/examples/Cargo.toml
index 7aa3a71c6..a202d5f0a 100644
--- a/examples/Cargo.toml
+++ b/examples/Cargo.toml
@@ -1,5 +1,11 @@
 [workspace]
-members = ["chacha20", "limited-order-book", "sha256"]
+members = [
+    "chacha20",
+    "limited-order-book",
+    "sha256",
+    "barrett",
+    "kyber_compress",
+]
 resolver = "2"
 
 [workspace.dependencies]
diff --git a/examples/Makefile b/examples/Makefile
index 0e0533056..69cb20696 100644
--- a/examples/Makefile
+++ b/examples/Makefile
@@ -3,8 +3,12 @@ default:
 	make -C limited-order-book
 	make -C chacha20
 	OTHERFLAGS="--lax" make -C sha256
+	make -C barrett
+	make -C kyber_compress
 
 clean:
 	make -C limited-order-book clean
 	make -C chacha20           clean
 	make -C sha256             clean
+	make -C barrett            clean
+	make -C kyber_compress     clean
diff --git a/examples/README.md b/examples/README.md
index dda89eca5..462d02101 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -5,6 +5,8 @@
 | chacha20           | Typechecks                   |
 | limited-order-book | Typechecks                   |
 | sha256             | Lax-typechecks               |
+| barrett            | Typechecks                   |
+| kyber_compress     | Typechecks                   |
 
 ## How to generate the F\* code and typecheck it for the examples
 
diff --git a/examples/barrett/Cargo.toml b/examples/barrett/Cargo.toml
new file mode 100644
index 000000000..cc92acd1b
--- /dev/null
+++ b/examples/barrett/Cargo.toml
@@ -0,0 +1,9 @@
+[package]
+name = "barrett"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+hax-lib.workspace = true
diff --git a/examples/barrett/Makefile b/examples/barrett/Makefile
new file mode 100644
index 000000000..212cda6e4
--- /dev/null
+++ b/examples/barrett/Makefile
@@ -0,0 +1,7 @@
+.PHONY: default clean
+default:
+	make -C proofs/fstar/extraction
+
+clean:
+	rm -f proofs/fstar/extraction/.depend
+	rm -f proofs/fstar/extraction/*.fst
diff --git a/examples/barrett/proofs/fstar/extraction/Makefile b/examples/barrett/proofs/fstar/extraction/Makefile
new file mode 100644
index 000000000..f976e19da
--- /dev/null
+++ b/examples/barrett/proofs/fstar/extraction/Makefile
@@ -0,0 +1,106 @@
+# This is a generically useful Makefile for F* that is self-contained
+#
+# It is tempting to factor this out into multiple Makefiles but that
+# makes it less portable, so resist temptation, or move to a more
+# sophisticated build system.
+#
+# We expect FSTAR_HOME to be set to your FSTAR repo/install directory
+# We expect HACL_HOME to be set to your HACL* repo location
+# We expect HAX_PROOF_LIBS to be set to the folder containing core, rust_primitives etc.
+# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`.
+#
+# ROOTS contains all the top-level F* files you wish to verify
+# The default target `verify` verified ROOTS and its dependencies
+# To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line
+#
+#
+# To make F* emacs mode use the settings in this file, you need to
+# add the following lines to your .emacs
+#
+# (setq-default fstar-executable "<YOUR_FSTAR_HOME>/bin/fstar.exe")
+# (setq-default fstar-smt-executable "<YOUR_Z3_HOME>/bin/z3")
+#
+# (defun my-fstar-compute-prover-args-using-make ()
+#   "Construct arguments to pass to F* by calling make."
+#   (with-demoted-errors "Error when constructing arg string: %S"
+#     (let* ((fname (file-name-nondirectory buffer-file-name))
+# 	   (target (concat fname "-in"))
+# 	   (argstr (car (process-lines "make" "--quiet" target))))
+#       (split-string argstr))))
+# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
+#
+
+HAX_HOME       ?= $(shell git rev-parse --show-toplevel)
+FSTAR_HOME     ?= $(HAX_HOME)/../../../FStar
+HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
+
+FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
+
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
+
+CACHE_DIR      ?= $(HAX_PROOF_LIBS)/.cache
+HINT_DIR       ?= $(HAX_PROOF_LIBS)/.hints
+
+.PHONY: all verify clean
+
+all:
+	rm -f .depend && $(MAKE) .depend
+	$(MAKE) verify
+
+# By default, we process all the files in the current directory. Here, we
+# *extend* the set of relevant files with the tests.
+ROOTS = Barrett.fst
+
+$(ROOTS): ../../../src/lib.rs
+	cargo hax into fstar --z3rlimit 500
+
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
+	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
+	$(HAX_PROOF_LIBS_HOME)/hax_lib \
+	$(HAX_LIBS_HOME)
+
+FSTAR_FLAGS = --cmi \
+  --warn_error -331 \
+  --cache_checked_modules --cache_dir $(CACHE_DIR) \
+  --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
+  $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
+
+FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS)
+
+
+.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS)
+	$(info $(ROOTS))
+	$(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@
+
+include .depend
+
+$(HINT_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR)
+	$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints
+
+verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
+
+# Targets for interactive mode
+
+%.fst-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints)
+
+%.fsti-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints)
+
+
+# Clean targets
+
+SHELL ?= /usr/bin/env bash
+
+clean:
+	rm -rf $(CACHE_DIR)/*
+	rm *.fst
diff --git a/examples/barrett/src/lib.rs b/examples/barrett/src/lib.rs
new file mode 100644
index 000000000..b5bc7d40e
--- /dev/null
+++ b/examples/barrett/src/lib.rs
@@ -0,0 +1,69 @@
+use hax_lib as hax;
+
+/// Values having this type hold a representative 'x' of the Kyber field.
+/// We use 'fe' as a shorthand for this type.
+pub(crate) type FieldElement = i32;
+
+const BARRETT_SHIFT: i64 = 26;
+const BARRETT_R: i64 = 0x4000000; // 2^26
+
+/// This is calculated as ⌊(BARRETT_R / FIELD_MODULUS) + 1/2⌋
+const BARRETT_MULTIPLIER: i64 = 20159;
+
+pub(crate) const FIELD_MODULUS: i32 = 3329;
+
+/// Signed Barrett Reduction
+///
+/// Given an input `value`, `barrett_reduce` outputs a representative `result`
+/// such that:
+///
+/// - result ≡ value (mod FIELD_MODULUS)
+/// - the absolute value of `result` is bound as follows:
+///
+/// `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)
+///
+/// In particular, if `|value| < BARRETT_R`, then `|result| < FIELD_MODULUS`.
+#[hax::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
+#[hax::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS &&
+                   result % FIELD_MODULUS == value % FIELD_MODULUS)]
+pub fn barrett_reduce(value: FieldElement) -> FieldElement {
+    let t = i64::from(value) * BARRETT_MULTIPLIER;
+    // assert!(9223372036854775807 - (BARRETT_R >> 1) > t);
+    let t = t + (BARRETT_R >> 1);
+
+    let quotient = t >> BARRETT_SHIFT;
+    // assert!(quotient <= 2147483647_i64 || quotient >= -2147483648_i64);
+    let quotient = quotient as i32;
+
+    // assert!(((quotient as i64) * (FIELD_MODULUS as i64)) < 9223372036854775807);
+    let sub = quotient * FIELD_MODULUS;
+
+    hax::fstar!(r"Math.Lemmas.cancel_mul_mod (v $quotient) 3329");
+
+    value - sub
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn it_works() {
+        fn test(val: FieldElement, expected: FieldElement) {
+            let reduced = barrett_reduce(val);
+            assert_eq!(reduced, expected);
+        }
+
+        test(FIELD_MODULUS + 1, 1);
+        test(FIELD_MODULUS, 0);
+        test(FIELD_MODULUS - 1, -1);
+
+        test(FIELD_MODULUS + (FIELD_MODULUS - 1), -1);
+        test(FIELD_MODULUS + (FIELD_MODULUS + 1), 1);
+
+        test(1234, 1234);
+        test(9876, -111);
+
+        test(4327, 4327 % FIELD_MODULUS)
+    }
+}
diff --git a/examples/kyber_compress/Cargo.toml b/examples/kyber_compress/Cargo.toml
new file mode 100644
index 000000000..3749fb057
--- /dev/null
+++ b/examples/kyber_compress/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "kyber_compress"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+hax-lib-macros.workspace = true
+hax-lib.workspace = true
diff --git a/examples/kyber_compress/Makefile b/examples/kyber_compress/Makefile
new file mode 100644
index 000000000..212cda6e4
--- /dev/null
+++ b/examples/kyber_compress/Makefile
@@ -0,0 +1,7 @@
+.PHONY: default clean
+default:
+	make -C proofs/fstar/extraction
+
+clean:
+	rm -f proofs/fstar/extraction/.depend
+	rm -f proofs/fstar/extraction/*.fst
diff --git a/examples/kyber_compress/proofs/fstar/extraction/Makefile b/examples/kyber_compress/proofs/fstar/extraction/Makefile
new file mode 100644
index 000000000..f39ae304f
--- /dev/null
+++ b/examples/kyber_compress/proofs/fstar/extraction/Makefile
@@ -0,0 +1,107 @@
+# This is a generically useful Makefile for F* that is self-contained
+#
+# It is tempting to factor this out into multiple Makefiles but that
+# makes it less portable, so resist temptation, or move to a more
+# sophisticated build system.
+#
+# We expect FSTAR_HOME to be set to your FSTAR repo/install directory
+# We expect HACL_HOME to be set to your HACL* repo location
+# We expect HAX_PROOF_LIBS to be set to the folder containing core, rust_primitives etc.
+# We expect HAX_LIB to be set to the folder containing the crate `hax-lib`.
+#
+# ROOTS contains all the top-level F* files you wish to verify
+# The default target `verify` verified ROOTS and its dependencies
+# To lax-check instead, set `OTHERFLAGS="--lax"` on the command-line
+#
+#
+# To make F* emacs mode use the settings in this file, you need to
+# add the following lines to your .emacs
+#
+# (setq-default fstar-executable "<YOUR_FSTAR_HOME>/bin/fstar.exe")
+# (setq-default fstar-smt-executable "<YOUR_Z3_HOME>/bin/z3")
+#
+# (defun my-fstar-compute-prover-args-using-make ()
+#   "Construct arguments to pass to F* by calling make."
+#   (with-demoted-errors "Error when constructing arg string: %S"
+#     (let* ((fname (file-name-nondirectory buffer-file-name))
+# 	   (target (concat fname "-in"))
+# 	   (argstr (car (process-lines "make" "--quiet" target))))
+#       (split-string argstr))))
+# (setq fstar-subp-prover-args #'my-fstar-compute-prover-args-using-make)
+#
+
+HAX_HOME       ?= $(shell git rev-parse --show-toplevel)
+FSTAR_HOME     ?= $(HAX_HOME)/../../../FStar
+HACL_HOME      ?= $(HAX_HOME)/../../../hacl-star
+
+FSTAR_BIN      ?= $(shell command -v fstar.exe 1>&2 2> /dev/null && echo "fstar.exe" || echo "$(FSTAR_HOME)/bin/fstar.exe")
+
+
+HAX_PROOF_LIBS_HOME ?= $(HAX_HOME)/proof-libs/fstar
+HAX_LIBS_HOME       ?= $(HAX_HOME)/hax-lib/proofs/fstar/extraction
+
+CACHE_DIR      ?= $(HAX_PROOF_LIBS)/.cache
+HINT_DIR       ?= $(HAX_PROOF_LIBS)/.hints
+
+.PHONY: all verify clean
+
+all:
+	rm -f .depend && $(MAKE) .depend
+	$(MAKE) verify
+
+# By default, we process all the files in the current directory. Here, we
+# *extend* the set of relevant files with the tests.
+ROOTS = Kyber_compress.fst
+
+$(ROOTS): ../../../src/lib.rs
+	cargo hax into fstar --z3rlimit 150
+
+FSTAR_INCLUDE_DIRS = $(HACL_HOME)/lib \
+	$(HAX_PROOF_LIBS_HOME)/rust_primitives $(HAX_PROOF_LIBS_HOME)/core \
+	$(HAX_PROOF_LIBS_HOME)/hax_lib \
+	$(HAX_LIBS_HOME)
+
+FSTAR_FLAGS = --cmi \
+  --warn_error -331 \
+  --cache_checked_modules --cache_dir $(CACHE_DIR) \
+  --already_cached "+Prims+FStar+LowStar+C+Spec.Loops+TestLib" \
+  $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
+
+FSTAR = $(FSTAR_BIN) $(FSTAR_FLAGS)
+
+
+.depend: $(HINT_DIR) $(CACHE_DIR) $(ROOTS)
+	$(info $(ROOTS))
+	$(FSTAR) --cmi --dep full $(ROOTS) --extract '* -Prims -LowStar -FStar' > $@
+
+include .depend
+
+$(HINT_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR):
+	mkdir -p $@
+
+$(CACHE_DIR)/%.checked: | .depend $(HINT_DIR) $(CACHE_DIR)
+	$(FSTAR) $(OTHERFLAGS) $< $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(notdir $*).hints
+
+verify: $(addsuffix .checked, $(addprefix $(CACHE_DIR)/,$(ROOTS)))
+
+# Targets for interactive mode
+
+%.fst-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fst.hints)
+
+%.fsti-in:
+	$(info $(FSTAR_FLAGS) \
+	  $(ENABLE_HINTS) --hint_file $(HINT_DIR)/$(basename $@).fsti.hints)
+
+
+# Clean targets
+
+SHELL ?= /usr/bin/env bash
+
+clean:
+	rm -rf $(CACHE_DIR)/*
+	rm *.fst
diff --git a/examples/kyber_compress/src/lib.rs b/examples/kyber_compress/src/lib.rs
new file mode 100644
index 000000000..71d2d3fc4
--- /dev/null
+++ b/examples/kyber_compress/src/lib.rs
@@ -0,0 +1,71 @@
+use hax_lib::{ensures, fstar, requires};
+
+const FIELD_MODULUS: i32 = 3329;
+const UNSIGNED_FIELD_MODULUS: u32 = FIELD_MODULUS as u32;
+
+#[requires(n == 4 || n == 5 || n == 10 || n == 11 || n == 16)]
+#[ensures(|result| result < 2u32.pow(n as u32))]
+fn get_n_least_significant_bits(n: u8, value: u32) -> u32 {
+    let nth_bit = 1 << n;
+    let mask = nth_bit - 1;
+    fstar!("Rust_primitives.Integers.logand_mask_lemma $value (v $n)");
+    value & mask
+}
+
+#[
+  requires(
+        (coefficient_bits == 4 ||
+         coefficient_bits == 5 ||
+         coefficient_bits == 10 ||
+         coefficient_bits == 11) &&
+         fe < (FIELD_MODULUS as u16))]
+#[
+  ensures(|result| result < 1 << coefficient_bits)]
+pub fn compress_unsafe(coefficient_bits: u8, fe: u16) -> i32 {
+    let mut compressed = (fe as u32) << (coefficient_bits + 1);
+    compressed += UNSIGNED_FIELD_MODULUS;
+    compressed /= UNSIGNED_FIELD_MODULUS << 1;
+    compressed &= (1 << coefficient_bits) - 1;
+    fstar!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
+    get_n_least_significant_bits(coefficient_bits, compressed) as i32
+}
+
+#[
+  requires(
+        (coefficient_bits == 4 ||
+         coefficient_bits == 5 ||
+         coefficient_bits == 10 ||
+         coefficient_bits == 11) &&
+         fe < (FIELD_MODULUS as u16))]
+#[
+  ensures(|result| result < 1 << coefficient_bits)]
+pub fn compress(coefficient_bits: u8, fe: u16) -> i32 {
+    let mut compressed = (fe as u64) << coefficient_bits;
+    compressed += 1664 as u64;
+    compressed *= 10_321_340;
+    compressed >>= 35;
+    compressed &= (1 << coefficient_bits) - 1;
+    fstar!("Rust_primitives.Integers.logand_mask_lemma $compressed (v $coefficient_bits)");
+    let compressed = compressed as u32;
+    get_n_least_significant_bits(coefficient_bits, compressed) as i32
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn it_works() {
+        fn test(coefficient_bits: u8, fe: u16) {
+            let c1 = compress_unsafe(coefficient_bits, fe);
+            let c2 = compress(coefficient_bits, fe);
+            assert_eq!(c1, c2);
+        }
+
+        for bits in [4u8, 5, 10, 11] {
+            for fe in 0..3329 {
+                test(bits, fe);
+            }
+        }
+    }
+}
diff --git a/hax-lib-macros/src/lib.rs b/hax-lib-macros/src/lib.rs
index 20c130458..21413a1a0 100644
--- a/hax-lib-macros/src/lib.rs
+++ b/hax-lib-macros/src/lib.rs
@@ -1,3 +1,4 @@
+mod quote;
 mod rewrite_self;
 mod syn_ext;
 mod utils;
@@ -538,3 +539,56 @@ pub fn pv_handwritten(_attr: pm::TokenStream, item: pm::TokenStream) -> pm::Toke
     let attr = AttrPayload::PVHandwritten;
     quote! {#attr #item}.into()
 }
+
+macro_rules! make_quoting_proc_macro {
+    ($backend:ident($cfg_name:ident)) => {
+        #[doc = concat!("Embed ", stringify!($backend), " expression inside a Rust expression. This macro takes only one argument: some raw ", stringify!($backend), " code as a string literal.")]
+        ///
+
+        /// While it is possible to directly write raw backend code,
+        /// sometimes it can be inconvenient. For example, referencing
+        /// Rust names can be a bit cumbersome: for example, the name
+        /// `my_crate::my_module::CONSTANT` might be translated
+        /// differently in a backend (e.g. in the F* backend, it will
+        /// probably be `My_crate.My_module.v_CONSTANT`).
+        ///
+
+        /// To facilitate this, you can write Rust names directly,
+        /// using the prefix `$`: `f $my_crate::my_module__CONSTANT + 3`
+        /// will be replaced with `f My_crate.My_module.v_CONSTANT + 3`
+        /// in the F* backend for instance.
+
+        /// If you want to refer to the Rust constructor
+        /// `Enum::Variant`, you should write `$$Enum::Variant` (note
+        /// the double dollar).
+
+        /// If the name refers to something polymorphic, you need to
+        /// signal it by adding _any_ type informations,
+        /// e.g. `${my_module::function<()>}`. The curly braces are
+        /// needed for such more complex expressions.
+
+        /// You can also write Rust patterns with the `$?{SYNTAX}`
+        /// syntax, where `SYNTAX` is a Rust pattern. The syntax
+        /// `${EXPR}` also allows any Rust expressions
+        /// `EXPR` to be embedded.
+
+        #[proc_macro]
+        pub fn $backend(payload: pm::TokenStream) -> pm::TokenStream {
+            let ts: TokenStream = quote::quote(payload).into();
+            quote!{
+                #[cfg($cfg_name)]
+                {
+                    #ts
+                }
+            }.into()
+        }
+    };
+    ($backend:ident($cfg_name:ident) $($others:tt)+) => {
+        make_quoting_proc_macro!($backend($cfg_name));
+        make_quoting_proc_macro!($($others)+);
+    }
+}
+
+make_quoting_proc_macro!(fstar(hax_backend_fstar)
+                         coq(hax_backend_coq)
+                         proverif(hax_backend_proverif));
diff --git a/hax-lib-macros/src/quote.rs b/hax-lib-macros/src/quote.rs
new file mode 100644
index 000000000..7ccf70c9d
--- /dev/null
+++ b/hax-lib-macros/src/quote.rs
@@ -0,0 +1,152 @@
+//! This module provides the logic for the quotation macros, which
+//! allow for quoting F*/Coq/... code directly from Rust.
+//!
+//! In a F*/Coq/... quote, one can write antiquotations, that is,
+//! embedded Rust snippets. The syntax is `$<PREFIX><PAYLOAD>`. The
+//! payload `<PAYLOAD>` should be a Rust path, or a group with
+//! arbitrary contents `{...contents...}`.
+//!
+//! The `<PREFIX>` describes the kind of the antiquotation:
+//!  - empty prefix, the antiquotation is an expression;
+//!  - `?`, the antiquotation is a pattern;
+//!  - `$`, the antiquotation is a constructor name.
+
+use crate::prelude::*;
+use quote::ToTokens;
+
+/// Marker that indicates a place where a antiquotation will be inserted
+const SPLIT_MARK: &str = "SPLIT_QUOTE";
+
+/// The different kinds of antiquotations
+enum AntiquoteKind {
+    Expr,
+    Constructor,
+    Pat,
+}
+
+impl ToTokens for AntiquoteKind {
+    fn to_tokens(&self, tokens: &mut TokenStream) {
+        tokens.extend(
+            [match self {
+                Self::Expr => quote! {_expr},
+                Self::Constructor => quote! {_constructor},
+                Self::Pat => quote! {_pat},
+            }]
+            .into_iter(),
+        )
+    }
+}
+
+/// An antiquotation
+struct Antiquote {
+    ts: pm::TokenStream,
+    kind: AntiquoteKind,
+}
+
+impl ToTokens for Antiquote {
+    fn to_tokens(&self, tokens: &mut TokenStream) {
+        let ts = TokenStream::from(self.ts.clone());
+        fn wrap_pattern(pat: TokenStream) -> TokenStream {
+            quote! {{#[allow(unreachable_code)]
+                 match None { Some(#pat) => (), _ => () }
+            }}
+        }
+        let ts = match self.kind {
+            AntiquoteKind::Expr => ts,
+            AntiquoteKind::Constructor => wrap_pattern(quote! {#ts {..}}),
+            AntiquoteKind::Pat => wrap_pattern(ts),
+        };
+        tokens.extend([ts].into_iter())
+    }
+}
+
+/// Extract antiquotations (`$[?][$]...`, `$[?][$]{...}`) and parses them.
+fn process_string(s: &str) -> std::result::Result<(String, Vec<Antiquote>), String> {
+    let mut chars = s.chars().peekable();
+    let mut antiquotations = vec![];
+    let mut output = String::new();
+    while let Some(ch) = chars.next() {
+        match ch {
+            '$' => {
+                let mut s = String::new();
+                let mut kind = AntiquoteKind::Expr;
+                if let Some(prefix) = chars.next_if(|ch| *ch == '?' || *ch == '$') {
+                    kind = match prefix {
+                        '?' => AntiquoteKind::Pat,
+                        '$' => AntiquoteKind::Constructor,
+                        _ => unreachable!(),
+                    };
+                }
+                // If the first character is `{`, we parse the block
+                if let Some('{') = chars.peek() {
+                    chars.next(); // Consume `{`
+                    let mut level = 0;
+                    while let Some(ch) = chars.next() {
+                        level += match ch {
+                            '{' => 1,
+                            '}' => -1,
+                            _ => 0,
+                        };
+                        if level < 0 {
+                            break;
+                        }
+                        s.push(ch);
+                    }
+                } else {
+                    while let Some(ch) =
+                        chars.next_if(|ch| !matches!(ch, ' ' | '\t' | '\n' | '(' | '{' | ')'))
+                    {
+                        s.push(ch)
+                    }
+                }
+                if s.is_empty() {
+                    return Err(format!(
+                        "Empty antiquotation just before `{}`",
+                        chars.collect::<String>()
+                    ));
+                }
+                output += SPLIT_MARK;
+                // See https://github.com/rust-lang/rust/issues/58736
+                let ts: std::result::Result<TokenStream, _> = syn::parse_str(&s)
+                    .map_err(|err| format!("Could not parse antiquotation `{s}`: got error {err}"));
+                if let Err(message) = &ts {
+                    // If we don't panic, the error won't show up,
+                    // this is because `parse_str` is not only
+                    // panicking, but also makes rustc to exit earlier.
+                    panic!("{message}");
+                }
+                let ts: pm::TokenStream = ts?.into();
+                antiquotations.push(Antiquote { ts, kind })
+            }
+            _ => output.push(ch),
+        }
+    }
+    Ok((output, antiquotations))
+}
+
+pub(super) fn quote(payload: pm::TokenStream) -> pm::TokenStream {
+    let payload = parse_macro_input!(payload as LitStr).value();
+
+    if payload.find(SPLIT_MARK).is_some() {
+        return quote! {std::compile_error!(std::concat!($SPLIT_MARK, " is reserved"))}.into();
+    }
+
+    let (string, antiquotes) = match process_string(&payload) {
+        Ok(x) => x,
+        Err(message) => return quote! {std::compile_error!(#message)}.into(),
+    };
+    let string = proc_macro2::Literal::string(&string);
+    let string: TokenStream = [proc_macro2::TokenTree::Literal(string)]
+        .into_iter()
+        .collect();
+    let mut code = quote! {#string};
+    for user in antiquotes.iter().rev() {
+        let kind = &user.kind;
+        code = quote! {
+            let #kind = #user;
+            #code
+        };
+    }
+
+    quote! {hax_lib::inline(#[allow(unused_variables)]{#code})}.into()
+}
diff --git a/hax-lib/src/lib.rs b/hax-lib/src/lib.rs
index 34dd40b18..a9286c7ed 100644
--- a/hax-lib/src/lib.rs
+++ b/hax-lib/src/lib.rs
@@ -131,3 +131,7 @@ pub fn implies(lhs: bool, rhs: impl Fn() -> bool) -> bool {
 }
 
 pub use hax_lib_macros::*;
+
+/// Dummy function that carries a string to be printed as such in the output language
+#[doc(hidden)]
+pub fn inline(_: &str) {}
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index a05894349..98d940c6e 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -129,6 +129,8 @@ let add3_lemma (x: u32)
         x <=. 10ul || x >=. (u32_max /! 3ul <: u32) || (add3 x x x <: u32) =. (x *! 3ul <: u32)) =
   ()
 
+let inlined_code__V: u8 = 12uy
+
 let u32_max: u32 = 90000ul
 
 let add3 (x y z: u32)
@@ -147,4 +149,13 @@ type t_Foo = {
   f_y:f_y: u32{f_y >. 3ul};
   f_z:f_z: u32{((f_y +! f_x <: u32) +! f_z <: u32) >. 3ul}
 }
+
+let inlined_code (foo: t_Foo) : Prims.unit =
+  let vv_a:i32 = 13l in
+  let _:Prims.unit =
+    let x = foo.f_x in
+    let { f_y = y } = foo in
+    add3 ((fun _ -> 3ul) foo) vv_a inlined_code__V y
+  in
+  ()
 '''
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index bc41ff43b..7c8dfdf4b 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -43,7 +43,6 @@ impl Foo {
 #[hax::attributes]
 mod refined_arithmetic {
     use core::ops::{Add, Mul};
-    use hax_lib_macros as hax;
 
     struct Foo(u8);
 
@@ -124,3 +123,14 @@ mod newtype_pattern {
         }
     }
 }
+
+fn inlined_code(foo: Foo) {
+    const V: u8 = 12;
+    let v_a = 13;
+    hax::fstar!(
+        r"let x = ${foo.x} in
+          let $?{Foo {y, ..}} = $foo in
+          $add3 ((fun _ -> 3ul) $foo) $v_a $V y
+        "
+    );
+}