diff --git a/src/main/dune b/src/main/dune
index aa75b3ba..ddfc6a44 100644
--- a/src/main/dune
+++ b/src/main/dune
@@ -8,7 +8,7 @@
  (modes native)
  (libraries containers iter result sidekick.sat sidekick.core sidekick-base
    sidekick.smt-solver sidekick-base.smtlib sidekick.drup sidekick.memtrace
-   sidekick-bin.lib)
+   sidekick-bin.lib sidekick.proof_twp)
  (flags :standard -safe-string -color always -open Sidekick_util))
 
 (executable
diff --git a/src/main/main.ml b/src/main/main.ml
index 5569a646..755dfd32 100644
--- a/src/main/main.ml
+++ b/src/main/main.ml
@@ -31,6 +31,7 @@ let p_progress = ref false
 let enable_trace = ref false
 let proof_file = ref ""
 let trace_file = ref ""
+let proof_twp_file = ref ""
 
 (* Arguments parsing *)
 let int_arg r arg =
@@ -83,6 +84,9 @@ let argspec =
       ( "--trace-file",
         Arg.Set_string trace_file,
         " store trace in given file (no cleanup)" );
+      ( "--proof-twp",
+        Arg.Set_string proof_twp_file,
+        " emit .twp proof to given file (talweg-compatible)" );
       "--no-model", Arg.Clear p_model, " do not print model";
       ( "--bool",
         Arg.Symbol
@@ -161,7 +165,7 @@ let mk_sat_tracer () : Sidekick_sat.Tracer.t =
 let main_smt ~config () : _ result =
   let tst = Term.Store.create ~size:4_096 () in
 
-  let enable_proof = !check || !p_proof || !proof_file <> "" in
+  let enable_proof = !check || !p_proof || !proof_file <> "" || !proof_twp_file <> "" in
   Log.debugf 1 (fun k -> k "(@[proof-enable@ %B@])" enable_proof);
 
   run_with_tmp_file ~enable_proof @@ fun trace_file ->
@@ -179,7 +183,17 @@ let main_smt ~config () : _ result =
      (* main proof object *)
      let proof = Proof.create ~config () in
   *)
-  let tracer = mk_smt_tracer ~trace_file () in
+  let twp_state_opt =
+    if !proof_twp_file <> "" then
+      Some (Sidekick_proof_twp.Twp_state.create ())
+    else
+      None
+  in
+  let tracer =
+    match twp_state_opt with
+    | Some st -> Sidekick_proof_twp.Twp_tracer.create st
+    | None -> mk_smt_tracer ~trace_file ()
+  in
   Proof.Tracer.enable tracer enable_proof;
 
   let solver =
@@ -230,6 +244,16 @@ let main_smt ~config () : _ result =
     try E.fold_l (fun () stmt -> Driver.process_stmt driver stmt) () input
     with Exit -> E.return ()
   in
+  (* If --proof-twp is set, write the accumulated .twp buffer to the file *)
+  (match twp_state_opt with
+  | None -> ()
+  | Some st ->
+    let buf = Sidekick_proof_twp.Twp_state.buffer st in
+    (try
+       CCIO.with_out !proof_twp_file (fun oc ->
+           Buffer.output_buffer oc buf)
+     with Sys_error msg ->
+       Log.debugf 0 (fun k -> k "proof-twp: cannot write file: %s" msg)));
   res
 
 let main_cnf () : _ result =
diff --git a/src/proof_twp/dune b/src/proof_twp/dune
new file mode 100644
index 00000000..4800cb4e
--- /dev/null
+++ b/src/proof_twp/dune
@@ -0,0 +1,5 @@
+(library
+ (name sidekick_proof_twp)
+ (public_name sidekick.proof_twp)
+ (libraries sidekick.core sidekick.proof sidekick.sat sidekick.smt-solver containers)
+ (flags :standard -open Sidekick_util -open Sidekick_core))
diff --git a/src/proof_twp/sidekick_proof_twp.ml b/src/proof_twp/sidekick_proof_twp.ml
new file mode 100644
index 00000000..b4a633b3
--- /dev/null
+++ b/src/proof_twp/sidekick_proof_twp.ml
@@ -0,0 +1,10 @@
+(** Sidekick .twp proof emitter.
+
+    This library provides the Twp_tracer, which implements Proof.Tracer.t
+    and emits .twp format proof files directly during solving.
+*)
+
+module Twp_state = Twp_state
+module Twp_term = Twp_term
+module Twp_pterm = Twp_pterm
+module Twp_tracer = Twp_tracer
diff --git a/src/proof_twp/twp_pterm.ml b/src/proof_twp/twp_pterm.ml
new file mode 100644
index 00000000..4fd24644
--- /dev/null
+++ b/src/proof_twp/twp_pterm.ml
@@ -0,0 +1,174 @@
+(** Translate Proof.Pterm.t rules to .twp P-lines.
+
+    Maps each sidekick rule name to the corresponding .twp proof step.
+    Returns the P-index of the emitted step.
+*)
+
+module Proof = Sidekick_proof
+open Twp_state
+
+let emit_pterm_rule (st : Twp_state.t) (r : Proof.Pterm.rule_apply) : int =
+  match r.Proof.Pterm.rule_name with
+
+  | "sat.input" ->
+    (* Input clause assumption.
+       lits = the literals of the clause.
+       For a single literal: P<n> assume E<lit> *)
+    (match r.Proof.Pterm.lit_args with
+    | [ lit ] ->
+      let e_idx = Twp_term.emit_lit st lit in
+      let p = alloc_p st in
+      emit_line st (Printf.sprintf "P%d assume E%d" p e_idx);
+      p
+    | lits ->
+      (* Multi-literal input clause: emit each lit as comments, then sorry *)
+      let p = alloc_p st in
+      List.iter (fun lit ->
+        let e_idx = Twp_term.emit_lit st lit in
+        emit_line st (Printf.sprintf "# sat.input lit E%d" e_idx)
+      ) lits;
+      emit_line st (Printf.sprintf "# sat.input multi-literal (sorry) P%d" p);
+      emit_line st (Printf.sprintf "P%d assume E%d" p Twp_state.e_false);
+      p)
+
+  | "core.lemma-cc" ->
+    (* CC conflict lemma: the lits form a conflict clause (tautology by CC).
+       Encode as: Q<k> seq [pos_lits] [neg_lits] and P<n> ext cc *)
+    let lits = r.Proof.Pterm.lit_args in
+    (* Split: positive lits (hyps) vs negative lits (conclusions for CC) *)
+    let pos_lits = List.filter Lit.sign lits in
+    let neg_lits = List.filter (fun l -> not (Lit.sign l)) lits in
+    let pos_e = List.map (Twp_term.emit_lit st) pos_lits in
+    let neg_e = List.map (fun l ->
+      Twp_term.emit_expr st (Lit.term l)
+    ) neg_lits in
+    let q = alloc_q st in
+    let fmt_e_list es = String.concat " " (List.map (Printf.sprintf "E%d") es) in
+    emit_line st
+      (Printf.sprintf "Q%d seq [%s] [%s]" q (fmt_e_list pos_e) (fmt_e_list neg_e));
+    let p = alloc_p st in
+    emit_line st (Printf.sprintf "P%d ext cc" p);
+    p
+
+  | "core.r1" | "core.res" ->
+    (* Resolution: cut P<a> P<b> *)
+    (match r.Proof.Pterm.premises with
+    | [ p1; p2 ] ->
+      let get_p (s : Proof.Step.id) =
+        let s_int = Sidekick_trace.Entry_id.to_int s in
+        match Hashtbl.find_opt st.step_tbl s_int with
+        | Some n -> n
+        | None ->
+          let n = alloc_p st in
+          emit_line st (Printf.sprintf "# ref step %d not found -> P%d" s_int n);
+          emit_line st (Printf.sprintf "P%d assume E%d" n Twp_state.e_false);
+          n
+      in
+      let p1_idx = get_p p1 in
+      let p2_idx = get_p p2 in
+      let p = alloc_p st in
+      emit_line st (Printf.sprintf "P%d cut P%d P%d" p p1_idx p2_idx);
+      p
+    | _ ->
+      let p = alloc_p st in
+      emit_line st
+        (Printf.sprintf "# core.r1/res: wrong premise count (sorry) P%d" p);
+      emit_line st (Printf.sprintf "P%d assume E%d" p Twp_state.e_false);
+      p)
+
+  | "sat.rc" ->
+    (* SAT redundant clause (RUP).
+       premises = list of step_ids for the premise proofs. *)
+    let hyp_idxs =
+      List.filter_map
+        (fun (s : Proof.Step.id) ->
+          let s_int = Sidekick_trace.Entry_id.to_int s in
+          Hashtbl.find_opt st.step_tbl s_int)
+        r.Proof.Pterm.premises
+    in
+    let fmt_p_list ps = String.concat " " (List.map (Printf.sprintf "P%d") ps) in
+    let p = alloc_p st in
+    emit_line st
+      (Printf.sprintf "P%d ext sk.sat_rup [%s]" p (fmt_p_list hyp_idxs));
+    p
+
+  | "core.define-term" ->
+    (* new_def E<k> *)
+    (match r.Proof.Pterm.term_args with
+    | t :: _ ->
+      let e_idx = Twp_term.emit_expr st t in
+      let p = alloc_p st in
+      emit_line st (Printf.sprintf "P%d new_def E%d" p e_idx);
+      p
+    | [] ->
+      let p = alloc_p st in
+      emit_line st (Printf.sprintf "# core.define-term: no terms (sorry) P%d" p);
+      emit_line st (Printf.sprintf "P%d assume E%d" p Twp_state.e_false);
+      p)
+
+  | "core.with-defs" | "core.preprocess" | "core.rw-clause"
+  | "core.true" | "core.p1" ->
+    (* Sorry-style: emit a dummy step *)
+    let p = alloc_p st in
+    emit_line st
+      (Printf.sprintf "# %s (sorry) P%d" r.Proof.Pterm.rule_name p);
+    emit_line st (Printf.sprintf "P%d assume E%d" p Twp_state.e_false);
+    p
+
+  | name ->
+    (* Unknown rule: sorry *)
+    let p = alloc_p st in
+    emit_line st (Printf.sprintf "# unknown rule '%s' (sorry) P%d" name p);
+    emit_line st (Printf.sprintf "P%d assume E%d" p Twp_state.e_false);
+    p
+
+(** Translate a Pterm.t and emit .twp lines.
+    Returns the P-index of the outermost proof step. *)
+let rec emit_pterm (st : Twp_state.t) (pt : Proof.Pterm.t) : int =
+  match pt with
+  | Proof.Pterm.P_apply r ->
+    emit_pterm_rule st r
+
+  | Proof.Pterm.P_ref step_id ->
+    (* Reference to a previously emitted step *)
+    let s_int = Sidekick_trace.Entry_id.to_int step_id in
+    (match Hashtbl.find_opt st.step_tbl s_int with
+    | Some n -> n
+    | None ->
+      let n = alloc_p st in
+      emit_line st (Printf.sprintf "# P_ref step %d not found -> P%d" s_int n);
+      emit_line st (Printf.sprintf "P%d assume E%d" n Twp_state.e_false);
+      n)
+
+  | Proof.Pterm.P_local local_ref ->
+    (* Local ref within a P_let binding; resolved by emit_pterm_with_locals *)
+    let n = alloc_p st in
+    emit_line st (Printf.sprintf "# P_local s%d (unresolved) -> P%d" local_ref n);
+    emit_line st (Printf.sprintf "P%d assume E%d" n Twp_state.e_false);
+    n
+
+  | Proof.Pterm.P_let (bindings, body) ->
+    (* Process bindings, then process body with the local map *)
+    let local_map : (int, int) Hashtbl.t = Hashtbl.create 4 in
+    List.iter (fun (local_id, pt_inner) ->
+      let p_inner = emit_pterm st pt_inner in
+      Hashtbl.add local_map local_id p_inner
+    ) bindings;
+    emit_pterm_with_locals st body local_map
+
+and emit_pterm_with_locals (st : Twp_state.t) (pt : Proof.Pterm.t)
+    (locals : (int, int) Hashtbl.t) : int =
+  match pt with
+  | Proof.Pterm.P_local local_ref ->
+    (match Hashtbl.find_opt locals local_ref with
+    | Some n -> n
+    | None ->
+      let n = alloc_p st in
+      emit_line st (Printf.sprintf "# unresolved P_local s%d -> P%d" local_ref n);
+      emit_line st (Printf.sprintf "P%d assume E%d" n Twp_state.e_false);
+      n)
+  | Proof.Pterm.P_apply r ->
+    (* For rule_apply within let, we need to resolve premise refs via locals *)
+    (* For simplicity, just call the regular handler *)
+    emit_pterm_rule st r
+  | other -> emit_pterm st other
diff --git a/src/proof_twp/twp_state.ml b/src/proof_twp/twp_state.ml
new file mode 100644
index 00000000..d3818e2f
--- /dev/null
+++ b/src/proof_twp/twp_state.ml
@@ -0,0 +1,87 @@
+(** State for emitting .twp proof files.
+
+    Indices:
+    - E<n> = expression (type, term, etc.)
+    - P<n> = proof step
+    - Q<n> = sequent
+
+    After the preamble the following E-indices are fixed:
+      E1 = type
+      E2 = bool
+      E3 = false
+      E4 = type variable A (for polymorphic =)
+      E5 = A -> bool
+      E6 = A -> A -> bool   (type of =)
+
+    Subsequent E-indices are allocated on demand.
+*)
+
+open Sidekick_core
+
+type t = {
+  buf : Buffer.t;
+  (* maps term id → E-index *)
+  term_tbl : int Term.Tbl.t;
+  (* maps step id → P-index *)
+  step_tbl : (int, int) Hashtbl.t;
+  mutable next_e : int;
+  mutable next_p : int;
+  mutable next_q : int;
+}
+
+(* Fixed E-indices from the preamble *)
+let e_type = 1
+let e_bool = 2
+let e_false = 3
+let _e_tyvar_a = 4
+let _e_a_arrow_bool = 5
+let _e_eq_ty = 6  (* A -> A -> bool, the type of = *)
+
+let create () : t =
+  {
+    buf = Buffer.create 4096;
+    term_tbl = Term.Tbl.create 64;
+    step_tbl = Hashtbl.create 64;
+    next_e = 7;   (* E1-E6 reserved by preamble *)
+    next_p = 1;
+    next_q = 1;
+  }
+
+let emit_line (self : t) (line : string) : unit =
+  Buffer.add_string self.buf line;
+  Buffer.add_char self.buf '\n'
+
+let alloc_e (self : t) : int =
+  let n = self.next_e in
+  self.next_e <- n + 1;
+  n
+
+let alloc_p (self : t) : int =
+  let n = self.next_p in
+  self.next_p <- n + 1;
+  n
+
+let alloc_q (self : t) : int =
+  let n = self.next_q in
+  self.next_q <- n + 1;
+  n
+
+(** Emit the fixed preamble that every .twp file needs.
+    Declares bool, false, and the polymorphic = constant. *)
+let emit_preamble (self : t) : unit =
+  emit_line self "# preamble: bool, false, polymorphic =";
+  emit_line self "E1 type";
+  emit_line self "const bool [] E1";
+  emit_line self "E2 const bool";
+  emit_line self "const false [] E2";
+  emit_line self "E3 const false";
+  (* type variable A : type *)
+  emit_line self "E4 var A E1";
+  (* A -> bool *)
+  emit_line self "E5 arrow E4 E2";
+  (* A -> A -> bool *)
+  emit_line self "E6 arrow E4 E5";
+  (* const = [A] (A -> A -> bool) *)
+  emit_line self "const = [A] E6"
+
+let buffer (self : t) : Buffer.t = self.buf
diff --git a/src/proof_twp/twp_term.ml b/src/proof_twp/twp_term.ml
new file mode 100644
index 00000000..16383007
--- /dev/null
+++ b/src/proof_twp/twp_term.ml
@@ -0,0 +1,154 @@
+(** Translate sidekick Term.t to .twp E-index expressions.
+
+    This module walks Term.t recursively and emits E-lines into the
+    twp_state buffer. Results are memoized by term id.
+
+    With -open Sidekick_core:
+      Term  (includes T_builtins: C_bool, C_eq, C_not, C_true, C_false, C_ite, C_proof)
+      Const  (Const.view : Const.t -> const_view)
+      Str_const  (Str_const.Str : string -> const_view)
+      Lit
+*)
+
+open Twp_state
+
+(* fixed preamble indices from twp_state.ml *)
+let e_type_idx = Twp_state.e_type   (* 1 *)
+let e_bool_idx = Twp_state.e_bool   (* 2 *)
+let e_false_idx = Twp_state.e_false (* 3 *)
+
+(** Escape a name for use as a .twp atom. *)
+let escape_name (s : string) : string =
+  let ok c =
+    match c with
+    | 'a' .. 'z' | 'A' .. 'Z' | '0' .. '9' | '.' | '_' | '-' | '=' -> true
+    | _ -> false
+  in
+  if String.length s > 0 && String.for_all ok s then
+    s
+  else (
+    let buf = Buffer.create (String.length s + 2) in
+    Buffer.add_char buf '"';
+    String.iter
+      (fun c ->
+        if c = '"' then Buffer.add_string buf "\\\""
+        else if c = '\\' then Buffer.add_string buf "\\\\"
+        else Buffer.add_char buf c)
+      s;
+    Buffer.add_char buf '"';
+    Buffer.contents buf
+  )
+
+(** Main entry point: emit the E-lines for [t] and return its E-index.
+    Idempotent: memoized by Term.t identity. *)
+let rec emit_expr (st : Twp_state.t) (t : Term.t) : int =
+  match Term.Tbl.find_opt st.term_tbl t with
+  | Some n -> n
+  | None ->
+    let n = emit_expr_uncached st t in
+    Term.Tbl.replace st.term_tbl t n;
+    n
+
+and emit_expr_uncached (st : Twp_state.t) (t : Term.t) : int =
+  match Term.view t with
+  | Term.E_type _ ->
+    e_type_idx
+
+  | Term.E_const c ->
+    emit_const st t c
+
+  | Term.E_app (f, a) ->
+    let f_idx = emit_expr st f in
+    let a_idx = emit_expr st a in
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "E%d app E%d E%d" n f_idx a_idx);
+    n
+
+  | Term.E_pi (_, dom, body) ->
+    (* Arrow type — for QF_UF, Pi is a non-dependent arrow. *)
+    let dom_idx = emit_expr st dom in
+    let range_idx = emit_expr st body in
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "E%d arrow E%d E%d" n dom_idx range_idx);
+    n
+
+  | Term.E_lam _ | Term.E_var _ | Term.E_bound_var _ | Term.E_app_fold _ ->
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "# unsupported term view at E%d" n);
+    emit_line st (Printf.sprintf "E%d type" n);
+    n
+
+and emit_const (st : Twp_state.t) (t : Term.t) (c : Const.t) : int =
+  (* T_builtins constructors are included in Term module *)
+  match Const.view c with
+  | Term.C_bool -> e_bool_idx
+  | Term.C_false -> e_false_idx
+  | Term.C_true ->
+    let n = alloc_e st in
+    emit_line st "const true [] E2";
+    emit_line st (Printf.sprintf "E%d const true" n);
+    n
+  | Term.C_eq ->
+    (* Bare = constant — will be applied to type arg via E_app *)
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "E%d const =" n);
+    n
+  | Term.C_not ->
+    (* not : bool -> bool *)
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "# C_not (bool->bool) E%d" n);
+    emit_line st (Printf.sprintf "E%d const bool" n);
+    n
+  | Term.C_ite | Term.C_proof ->
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "# unsupported builtin E%d" n);
+    emit_line st (Printf.sprintf "E%d type" n);
+    n
+  | Str_const.Str name ->
+    emit_str_const st t name
+  | _ ->
+    (* For other const_view variants (e.g. uninterpreted sorts/functions from
+       sidekick-base Ty module), extract the name via the printer. *)
+    let name = Format.asprintf "%a" Const.pp c in
+    emit_str_const st t name
+
+and emit_str_const (st : Twp_state.t) (t : Term.t) (name : string) : int =
+  let ty_t = Term.ty t in
+  let is_sort =
+    match Term.view ty_t with
+    | Term.E_type _ -> true
+    | _ -> false
+  in
+  let safe_name = escape_name name in
+  if is_sort then (
+    emit_line st (Printf.sprintf "const %s [] E1" safe_name);
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "E%d const %s" n safe_name);
+    n
+  ) else (
+    let ty_idx = emit_expr st ty_t in
+    emit_line st (Printf.sprintf "const %s [] E%d" safe_name ty_idx);
+    let n = alloc_e st in
+    emit_line st (Printf.sprintf "E%d const %s" n safe_name);
+    n
+  )
+
+(** Emit the E-index for a Lit.t.
+    Positive: emit the term directly.
+    Negative: represent as (t = false). *)
+let emit_lit (st : Twp_state.t) (lit : Lit.t) : int =
+  let t = Lit.term lit in
+  let sign = Lit.sign lit in
+  if sign then
+    emit_expr st t
+  else (
+    let t_idx = emit_expr st t in
+    let eq_bool_n = alloc_e st in
+    emit_line st (Printf.sprintf "E%d const = E%d" eq_bool_n e_bool_idx);
+    let eq_t_n = alloc_e st in
+    emit_line st (Printf.sprintf "E%d app E%d E%d" eq_t_n eq_bool_n t_idx);
+    let eq_t_false_n = alloc_e st in
+    emit_line st
+      (Printf.sprintf "E%d app E%d E%d" eq_t_false_n eq_t_n e_false_idx);
+    eq_t_false_n
+  )
diff --git a/src/proof_twp/twp_tracer.ml b/src/proof_twp/twp_tracer.ml
new file mode 100644
index 00000000..0fa4719c
--- /dev/null
+++ b/src/proof_twp/twp_tracer.ml
@@ -0,0 +1,52 @@
+(** Proof tracer that emits .twp proof files directly.
+
+    Implements Sidekick_smt_solver.Tracer.t:
+    - Proof.Tracer.t methods: capture proof steps and emit .twp lines
+    - Sidekick_sat.Tracer.t methods: no-ops (we don't trace SAT)
+    - emit_assert_term: no-op
+*)
+
+module Proof = Sidekick_proof
+module Sat_tracer = Sidekick_sat.Tracer
+module Smt_tracer = Sidekick_smt_solver.Tracer
+open Twp_state
+
+(** Create a Smt_tracer.t that emits .twp proof steps into [state]. *)
+let create (state : Twp_state.t) : Smt_tracer.t =
+  Twp_state.emit_preamble state;
+  let next_step_id = ref 1 in
+  object
+    val mutable enabled = true
+
+    (* Term.Tracer.t *)
+    method emit_term (_t : Term.t) : Term.Tracer.term_ref =
+      Sidekick_trace.Entry_id.dummy
+
+    (* Proof.Tracer.t *)
+    method proof_enabled = enabled
+    method proof_enable b = enabled <- b
+
+    method emit_proof_step (p : Proof.Pterm.delayed) : Proof.Step.id =
+      if not enabled then
+        Proof.Step.dummy
+      else (
+        let pt = p () in
+        let sid = !next_step_id in
+        next_step_id := sid + 1;
+        let step_id = Sidekick_trace.Entry_id.of_int_unsafe sid in
+        let p_idx = Twp_pterm.emit_pterm state pt in
+        Hashtbl.replace state.step_tbl sid p_idx;
+        step_id
+      )
+
+    method emit_proof_delete _id = ()
+
+    (* Sidekick_sat.Tracer.t — no-ops *)
+    method sat_assert_clause ~id:_ _ _ = Sidekick_trace.Entry_id.dummy
+    method sat_delete_clause ~id:_ _ = ()
+    method sat_unsat_clause ~id:_ = Sidekick_trace.Entry_id.dummy
+    method sat_encode_lit _ = Ser_value.null
+
+    (* Smt_tracer.t extra method *)
+    method emit_assert_term _ = Sidekick_trace.Entry_id.dummy
+  end