diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index 326f9bb7b..0320f3ec9 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -796,14 +796,35 @@ struct
         in
         F.mk_e_app effect (if is_lemma then args else typ :: args)
 
+  (** Prints doc comments out of a list of attributes *)
+  let pdoc_comments attrs =
+    attrs
+    |> List.filter_map ~f:(fun (attr : attr) ->
+           match attr.kind with
+           | DocComment { kind; body } -> Some (kind, body)
+           | _ -> None)
+    |> List.map ~f:(fun (kind, string) ->
+           match kind with
+           | DCKLine ->
+               String.split_lines string
+               |> List.map ~f:(fun s -> "///" ^ s)
+               |> String.concat_lines
+           | DCKBlock -> "(**" ^ string ^ "*)")
+    |> List.map ~f:(fun s -> `VerbatimIntf (s, `NoNewline))
+
   let rec pitem (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    try pitem_unwrapped e
+    try
+      match pitem_unwrapped e with
+      | [] -> []
+      | printed_items ->
+          (* Print comments only for items that are being printed *)
+          pdoc_comments e.attrs @ printed_items
     with Diagnostics.SpanFreeError.Exn error ->
       let error = Diagnostics.SpanFreeError.payload error in
       let error = [%show: Diagnostics.Context.t * Diagnostics.kind] error in
@@ -816,8 +837,8 @@ struct
   and pitem_unwrapped (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
     match e.v with
@@ -1283,10 +1304,13 @@ struct
                    "Malformed `Quote` item: could not find a ItemQuote payload")
           |> Option.value ~default:Types.{ intf = true; impl = false }
         in
-        (if fstar_opts.intf then [ `VerbatimIntf (pquote e.span quote) ]
+        (if fstar_opts.intf then
+         [ `VerbatimIntf (pquote e.span quote, `Newline) ]
         else [])
         @
-        if fstar_opts.impl then [ `VerbatimImpl (pquote e.span quote) ] else []
+        if fstar_opts.impl then
+          [ `VerbatimImpl (pquote e.span quote, `Newline) ]
+        else []
     | HaxError details ->
         [
           `Comment
@@ -1302,8 +1326,8 @@ module type S = sig
     item ->
     [> `Impl of F.AST.decl
     | `Intf of F.AST.decl
-    | `VerbatimImpl of string
-    | `VerbatimIntf of string
+    | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+    | `VerbatimIntf of string * [ `NoNewline | `Newline ]
     | `Comment of string ]
     list
 end
@@ -1316,7 +1340,8 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
             end) : S)
 
 let strings_of_item ~signature_only (bo : BackendOptions.t) m items
-    (item : item) : [> `Impl of string | `Intf of string ] list =
+    (item : item) :
+    ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
     |> List.find ~f:(fun (clause : Types.inclusion_clause) ->
@@ -1353,26 +1378,44 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
   Print.pitem item
   |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> List.concat_map ~f:(function
-       | `Impl i -> [ mk_impl (decl_to_string i) ]
-       | `Intf i -> [ mk_intf (decl_to_string i) ]
-       | `VerbatimIntf s -> if interface_mode then [ `Intf s ] else [ `Impl s ]
-       | `VerbatimImpl s -> if interface_mode then [ `Impl s ] else [ `Impl s ]
+       | `Impl i -> [ (mk_impl (decl_to_string i), `Newline) ]
+       | `Intf i -> [ (mk_intf (decl_to_string i), `Newline) ]
+       | `VerbatimIntf (s, nl) ->
+           [ ((if interface_mode then `Intf s else `Impl s), nl) ]
+       | `VerbatimImpl (s, nl) ->
+           [ ((if interface_mode then `Impl s else `Impl s), nl) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
-           if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])
+           if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
+           else [ (`Impl s, `Newline) ])
 
 let string_of_items ~signature_only (bo : BackendOptions.t) m items :
     string * string =
   let strings =
     List.concat_map ~f:(strings_of_item ~signature_only bo m items) items
-    |> List.map ~f:(function
-         | `Impl s -> `Impl (String.strip s)
-         | `Intf s -> `Intf (String.strip s))
+    |> List.map
+         ~f:
+           ((function
+              | `Impl s -> `Impl (String.strip s)
+              | `Intf s -> `Intf (String.strip s))
+           *** Fn.id)
     |> List.filter
-         ~f:((function `Impl s | `Intf s -> String.is_empty s) >> not)
+         ~f:(fst >> (function `Impl s | `Intf s -> String.is_empty s) >> not)
   in
   let string_for filter =
-    List.filter_map ~f:filter strings |> String.concat ~sep:"\n\n"
+    let l =
+      List.filter_map
+        ~f:(fun (s, space) ->
+          let* s = filter s in
+          Some (s, space))
+        strings
+    in
+    let n = List.length l - 1 in
+    List.mapi
+      ~f:(fun i (s, space) ->
+        s ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n")
+      l
+    |> String.concat ~sep:"\n"
   in
   ( string_for (function `Impl s -> Some s | _ -> None),
     string_for (function `Intf s -> Some s | _ -> None) )
diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml
index e1f70f90c..c86d7e03d 100644
--- a/engine/lib/import_thir.ml
+++ b/engine/lib/import_thir.ml
@@ -101,6 +101,19 @@ let c_logical_op : Thir.logical_op -> logical_op = function
 let c_attr (attr : Thir.attribute) : attr =
   let kind =
     match attr.kind with
+    | DocComment (kind, body) ->
+        let kind =
+          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
+        in
+        DocComment { kind; body }
+    | Normal
+        {
+          item =
+            { args = Eq (_, Hir { symbol; _ }); path = "doc"; tokens = None };
+          tokens = None;
+        } ->
+        DocComment { kind = DCKLine; body = symbol }
+        (* Looks for `#[doc = "something"]` *)
     | Normal { item = { args; path; tokens = subtokens }; tokens } ->
         let args_tokens =
           match args with Delimited { tokens; _ } -> Some tokens | _ -> None
@@ -110,11 +123,6 @@ let c_attr (attr : Thir.attribute) : attr =
           Option.value ~default:"" (args_tokens || tokens || subtokens)
         in
         Tool { path; tokens }
-    | DocComment (kind, body) ->
-        let kind =
-          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
-        in
-        DocComment { kind; body }
   in
   { kind; span = Span.of_thir attr.span }
 
@@ -125,15 +133,14 @@ let c_item_attrs (attrs : Thir.item_attributes) : attrs =
      that parent/self structure in our AST. See
      https://github.com/hacspec/hax/issues/123. *)
   let self = c_attrs attrs.attributes in
-  let parent = c_attrs attrs.parent_attributes in
   let parent =
-    (* Repeating associateditem or uid is harmful *)
-    List.filter
-      ~f:(fun payload ->
+    c_attrs attrs.parent_attributes
+    |> List.filter ~f:([%matches? ({ kind = DocComment _; _ } : attr)] >> not)
+    |> (* Repeating associateditem or uid is harmful, same for comments *)
+    List.filter ~f:(fun payload ->
         match Attr_payloads.payloads [ payload ] with
         | [ ((Uid _ | AssociatedItem _), _) ] -> false
         | _ -> true)
-      parent
   in
   self @ parent
 
diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs
index e9482ce69..00400f27b 100644
--- a/engine/names/extract/build.rs
+++ b/engine/names/extract/build.rs
@@ -123,7 +123,8 @@ fn target_dir(suffix: &str) -> camino::Utf8PathBuf {
 }
 
 fn get_json() -> String {
-    let mut cmd = Command::new("cargo-hax");
+    let mut cmd =
+        Command::new(std::env::var("HAX_CARGO_COMMAND_PATH").unwrap_or("cargo-hax".to_string()));
     cmd.args([
         "hax",
         "-C",
diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs
index 09ea00209..e7bcdaac9 100644
--- a/frontend/exporter/src/traits.rs
+++ b/frontend/exporter/src/traits.rs
@@ -492,7 +492,7 @@ pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>(
         Ok(selection) => selection,
         Err(error) => fatal!(
             s,
-            "Cannot hanlde error `{:?}` selecting `{:?}`",
+            "Cannot handle error `{:?}` selecting `{:?}`",
             error,
             trait_ref
         ),
diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs
index 3e4060d1a..60a2aba72 100644
--- a/frontend/exporter/src/types/copied.rs
+++ b/frontend/exporter/src/types/copied.rs
@@ -290,7 +290,7 @@ impl<'tcx, S: BaseState<'tcx>> SInto<S, DefId> for rustc_hir::hir_id::OwnerId {
 #[derive(
     AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitFloatType, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitFloatType, state: S as gstate)]
 pub enum LitFloatType {
     Suffixed(FloatTy),
     Unsuffixed,
@@ -660,7 +660,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Vec<GenericArg>>
 
 /// Reflects both [`rustc_middle::ty::subst::GenericArg`] and [`rustc_middle::ty::subst::GenericArgKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -1948,7 +1948,7 @@ pub enum StrStyle {
 
 /// Reflects [`rustc_ast::ast::LitKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitKind, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitKind, state: S as gstate)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2000,7 +2000,7 @@ pub enum CommentKind {
 
 /// Reflects [`rustc_ast::ast::AttrArgs`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::AttrArgs, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgs, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2008,14 +2008,40 @@ pub enum AttrArgs {
     Empty,
     Delimited(DelimArgs),
 
+    Eq(Span, AttrArgsEq),
+    // #[todo]
+    // Todo(String),
+}
+
+/// Reflects [`rustc_ast::ast::AttrArgsEq`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgsEq, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub enum AttrArgsEq {
+    Hir(MetaItemLit),
     #[todo]
-    Todo(String),
-    // Eq(Span, AttrArgsEq),
+    Ast(String),
+    // Ast(P<Expr>),
+}
+
+/// Reflects [`rustc_ast::ast::MetaItemLit`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::MetaItemLit, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub struct MetaItemLit {
+    pub symbol: Symbol,
+    pub suffix: Option<Symbol>,
+    pub kind: LitKind,
+    pub span: Span,
 }
 
 /// Reflects [`rustc_ast::ast::AttrItem`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::AttrItem, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrItem, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2034,7 +2060,7 @@ impl<S> SInto<S, String> for rustc_ast::tokenstream::LazyAttrTokenStream {
 
 /// Reflects [`rustc_ast::ast::NormalAttr`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::NormalAttr, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::NormalAttr, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2045,7 +2071,7 @@ pub struct NormalAttr {
 
 /// Reflects [`rustc_ast::AttrKind`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::AttrKind, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::AttrKind, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
diff --git a/test-harness/src/command_hax_ext.rs b/test-harness/src/command_hax_ext.rs
index ff404a25f..ff830bc8c 100644
--- a/test-harness/src/command_hax_ext.rs
+++ b/test-harness/src/command_hax_ext.rs
@@ -33,9 +33,23 @@ impl CommandHaxExt for Command {
                 let root = std::env::current_dir().unwrap();
                 let root = root.parent().unwrap();
                 let engine_dir = root.join("engine");
-                // Make sure binaries are built
+                // Make sure binaries are built. Note this doesn't
+                // include `hax-engine-names-extract`: its build
+                // script requires the driver and CLI of `hax` to be
+                // available.
                 assert!(Command::new("cargo")
-                        .args(&["build", "--workspace", "--bins"])
+                            .args(&["build", "--bins"])
+                            .status()
+                            .unwrap()
+                            .success());
+                let cargo_hax = cargo_bin(CARGO_HAX);
+                let driver = cargo_bin("driver-hax-frontend-exporter");
+                // Now the driver & CLI are installed, call `cargo
+                // build` injecting their paths
+                assert!(Command::new("cargo")
+                        .args(&["build", "--workspace", "--bin", "hax-engine-names-extract"])
+                        .env("HAX_CARGO_COMMAND_PATH", &cargo_hax)
+                        .env("HAX_RUSTC_DRIVER_BINARY", &driver)
                         .status()
                         .unwrap()
                         .success());
@@ -49,8 +63,8 @@ impl CommandHaxExt for Command {
                         .unwrap()
                         .success());
                 Some(Paths {
-                    driver: cargo_bin("driver-hax-frontend-exporter"),
-                    cargo_hax: cargo_bin(CARGO_HAX),
+                    driver,
+                    cargo_hax,
                     engine: engine_dir.join("_build/install/default/bin/hax-engine"),
                 })
             };
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
index bfeaf0a6c..6998ed94e 100644
--- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap	
@@ -108,6 +108,10 @@ let v_MAX: usize = sz 10
 
 type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
 
+/// Triple dash comment
+(** Multiline double star comment Maecenas blandit accumsan feugiat.
+    Done vitae ullamcorper est.
+    Curabitur id dui eget sem viverra interdum. *)
 let mutation_example
       (use_generic_update_at: t_MyArray)
       (use_specialized_update_at: t_Slice u8)
@@ -153,6 +157,8 @@ let u32_max: u32 = 90000ul
 
 unfold let some_function _ = "hello from F*"
 
+/// A doc comment on `add3`
+///another doc comment on add3
 let add3 (x y z: u32)
     : Prims.Pure u32
       (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)
diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
index 86e4eb07f..759bc8f1d 100644
--- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap	
@@ -34,12 +34,14 @@ open FStar.Mul
 
 class t_Trait (v_Self: Type) = { __marker_trait_t_Trait:Prims.unit }
 
+/// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
 
 let main_a_b (_: Prims.unit) : Prims.unit = ()
 
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
+/// Direct dependencies
 let main_a (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
     : Prims.unit =
   let _:Prims.unit = main_a_a () in
@@ -76,6 +78,7 @@ type t_Foo = | Foo : t_Foo
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
+/// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = main_a (Foo <: t_Foo) in
   let _:Prims.unit = main_b () in
diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
index 9d392ab5e..b3a95740d 100644
--- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap	
@@ -35,6 +35,11 @@ module Interface_only
 open Core
 open FStar.Mul
 
+/// This item contains unsafe blocks and raw references, two features
+/// not supported by hax. Thanks to the `-i` flag and the `+:`
+/// modifier, `f` is still extractable as an interface.
+/// Expressions within type are still extracted, as well as pre- and
+/// post-conditions.
 val f (x: u8)
     : Prims.Pure (t_Array u8 (sz 4))
       (requires x <. 254uy)
@@ -45,6 +50,9 @@ val f (x: u8)
 
 type t_Bar = | Bar : t_Bar
 
+/// Non-inherent implementations are extracted, their bodies are not
+/// dropped. This might be a bit surprising: see
+/// https://github.com/hacspec/hax/issues/616.
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl: Core.Convert.t_From t_Bar Prims.unit =
   {
@@ -55,6 +63,7 @@ let impl: Core.Convert.t_From t_Bar Prims.unit =
 
 val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True)
 
+/// If you need to drop the body of a method, please hoist it:
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_1: Core.Convert.t_From t_Bar u8 =
   {
diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap
index abfe8b043..bada19155 100644
--- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap	
@@ -56,6 +56,7 @@ let debug (label value: u32) : Prims.unit =
   in
   ()
 
+/// `f` stacks mutliple let bindings declaring different `a`s.
 let f (_: Prims.unit) : Prims.unit =
   let a_1_:u32 = 104ul in
   let a_2_:u32 = 205ul in
@@ -66,6 +67,13 @@ let f (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = debug 1ul a_1_ in
   debug 4ul a
 
+/// `f` is expanded into `f_expand` below, while the execution of `f` gives:
+/// ```plaintext
+///  [3] a=306
+///  [2] a=205
+///  [1] a=104
+///  [last] a=123
+/// ```
 let ff_expand (_: Prims.unit) : Prims.unit =
   let a:i32 = 104l in
   let a:i32 = 205l in
diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap
index 5ae7f9b1a..ee3c46e86 100644
--- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
+++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap	
@@ -1,6 +1,5 @@
 ---
 source: test-harness/src/harness.rs
-assertion_line: 214
 expression: snapshot
 info:
   kind:
@@ -36,15 +35,18 @@ module Side_effects
 open Core
 open FStar.Mul
 
+/// Helper function
 let add3 (x y z: u32) : u32 =
   Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z
 
+/// Question mark without error coercion
 let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32)
     : Core.Result.t_Result i8 u32 =
   match y with
   | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32
   | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32
 
+/// Question mark with an error coercion
 let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
     : Core.Result.t_Result i8 u32 =
   match y with
@@ -52,6 +54,7 @@ let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16)
   | Core.Result.Result_Err err ->
     Core.Result.Result_Err (Core.Convert.f_from err) <: Core.Result.t_Result i8 u32
 
+/// Exercise early returns with control flow and loops
 let early_returns (x: u32) : u32 =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! _:Prims.unit =
         if x >. 3ul
@@ -104,6 +107,7 @@ let early_returns (x: u32) : u32 =
       <:
       Core.Ops.Control_flow.t_ControlFlow u32 u32)
 
+/// Exercise local mutation with control flow and loops
 let local_mutation (x: u32) : u32 =
   let y:u32 = 0ul in
   let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in
@@ -144,6 +148,7 @@ let local_mutation (x: u32) : u32 =
     let x:u32 = hoist15 in
     Core.Num.impl__u32__wrapping_add x y
 
+/// Test question mark on `Option`s with some control flow
 let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (match x with
       | Core.Option.Option_Some hoist19 ->
@@ -249,6 +254,7 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.
         <:
         Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8))
 
+/// Test question mark on `Result`s with local mutation
 let question_mark (x: u32) : Core.Result.t_Result u32 u32 =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! x:u32 =
         if x >. 40ul
@@ -300,6 +306,7 @@ type t_Bar = {
   f_b:(t_Array (bool & bool) (sz 6) & bool)
 }
 
+/// Combine `?` and early return
 let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B =
   Rust_primitives.Hax.Control_flow_monad.Mexception.run (if x >. 123uy <: bool
       then
@@ -336,6 +343,7 @@ type t_Foo = {
   f_bar:t_Bar
 }
 
+/// Test assignation on non-trivial places
 let assign_non_trivial_lhs (foo: t_Foo) : t_Foo =
   let foo:t_Foo = { foo with f_x = true } <: t_Foo in
   let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in
diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs
index cab615b18..76a05cd69 100644
--- a/tests/attributes/src/lib.rs
+++ b/tests/attributes/src/lib.rs
@@ -3,6 +3,8 @@ use hax_lib as hax;
 // dummy max value
 const u32_max: u32 = 90000;
 
+/// A doc comment on `add3`
+#[doc = "another doc comment on add3"]
 #[hax::requires(x > 10 && y > 10 && z > 10 && x + y + z < u32_max)]
 #[hax::ensures(|result| hax_lib::implies(true, || result > 32))]
 fn add3(x: u32, y: u32, z: u32) -> u32 {
@@ -84,6 +86,10 @@ mod refined_indexes {
         }
     }
 
+    /// Triple dash comment
+    /** Multiline double star comment Maecenas blandit accumsan feugiat.
+    Done vitae ullamcorper est.
+    Curabitur id dui eget sem viverra interdum. */
     fn mutation_example(
         use_generic_update_at: &mut MyArray,
         use_specialized_update_at: &mut [u8],