diff --git a/.github/workflows/build-debian-unstable.yml b/.github/workflows/build-debian-unstable.yml
index 34e2cad5d..61d921227 100644
--- a/.github/workflows/build-debian-unstable.yml
+++ b/.github/workflows/build-debian-unstable.yml
@@ -2,7 +2,7 @@ name: build-debian-unstable
 on:
   pull_request:
     branches:
-      - main
+      - none
   push:
     branches:
       - main
diff --git a/.github/workflows/build-fedora.yml b/.github/workflows/build-fedora.yml
index 8a098410e..0ebffe59a 100644
--- a/.github/workflows/build-fedora.yml
+++ b/.github/workflows/build-fedora.yml
@@ -2,7 +2,7 @@ name: build-fedora
 on:
   pull_request:
     branches:
-      - main
+      - none
   push:
     branches:
       - main
diff --git a/.github/workflows/build-nix.yml b/.github/workflows/build-nix.yml
index e2d028900..d1d0bdd53 100644
--- a/.github/workflows/build-nix.yml
+++ b/.github/workflows/build-nix.yml
@@ -2,7 +2,7 @@ name: build-nix
 on:
   pull_request:
     branches:
-      - main
+      - none
   push:
     branches:
       - main
diff --git a/.github/workflows/build-ubuntu.yml b/.github/workflows/build-ubuntu.yml
index 82056d647..1a8bfa7ce 100644
--- a/.github/workflows/build-ubuntu.yml
+++ b/.github/workflows/build-ubuntu.yml
@@ -2,7 +2,7 @@ name: build-ubuntu
 on:
   pull_request:
     branches:
-      - main
+      - none
   push:
     branches:
       - main
diff --git a/.github/workflows/changelog.yml b/.github/workflows/changelog.yml
index 309628919..33a8d33ca 100644
--- a/.github/workflows/changelog.yml
+++ b/.github/workflows/changelog.yml
@@ -3,7 +3,7 @@ on:
   pull_request:
     types: [assigned, opened, synchronize, reopened, labeled, unlabeled]
     branches:
-      - main
+      - none
 jobs:
   check-changelog:
     name: check-changelog
diff --git a/shell.nix b/shell.nix
index 38d970b08..7ae1c8000 100644
--- a/shell.nix
+++ b/shell.nix
@@ -36,6 +36,66 @@ let
   tinygo = pkgs.tinygo.overrideAttrs (old: {
     doCheck = false;
   });
+
+  codex = ocamlPackages.buildDunePackage (finalAttrs: {
+    pname = "codex";
+    version = "dev";
+    src = pkgs.fetchFromGitHub {
+      owner = "s41d";
+      repo = "codex";
+      rev = "05977de3acf12e18343a053be0f1fb936f8ec31c";
+      hash = "sha256-u/dD9ucNeY9j3czC9QtPPfNE3pZ1464gsWdJrsLT9hA=";
+    };
+
+    nativeBuildInputs = with pkgs.ocamlPackages; [
+      dune_3
+      findlib
+      js_of_ocaml
+      # tests
+      mdx
+      mdx.bin
+      qcheck-core
+    ];
+    buildInputs = with pkgs.ocamlPackages; [
+      js_of_ocaml
+      js_of_ocaml-ppx
+      ppx_deriving
+      ppx_inline_test
+    ];
+    propagatedBuildInputs = with pkgs.ocamlPackages; [
+      base64
+      bheap
+      camlp-streams
+      cudd
+      fmt
+      pacomb
+      patricia-tree
+      ppx_inline_test
+      vdom
+      zarith
+    ];
+
+
+    tailwindFile = pkgs.fetchurl {
+      url = "https://github.com/codex-semantics-library/codex/releases/download/1.0-rc4/tailwind4.1.5.css";
+      hash = "sha256-HgE6gWIf2+0W908sYIjhUDYkUnsIz0mJN2nHqXY3QD8=";
+    };
+    graphviz = pkgs.fetchurl {
+      url = "https://github.com/codex-semantics-library/codex/releases/download/1.0-rc4/graphviz.umd.js";
+      hash = "sha256-JeT1R2S8FhCSAcL0zsJjx7ai+bL1X3AjHcgEniwm33c=";
+    };
+    bundleOutput = pkgs.fetchurl {
+      url = "https://github.com/codex-semantics-library/codex/releases/download/1.0-rc4/bundle-output.js";
+      hash = "sha256-zYKJDdu5fkZ52eEzDBuk6mSyxzMDMWDatK/ynlpjU2o=";
+    };
+
+    postUnpack = ''
+      mkdir -p utils/gui/deps/js
+      cp ${finalAttrs.tailwindFile} $sourceRoot/utils/gui/deps/tailwind4.1.5.css
+      cp ${finalAttrs.graphviz} $sourceRoot/utils/gui/deps/graphviz.umd.js
+      cp ${finalAttrs.bundleOutput} $sourceRoot/utils/gui/deps/js/bundle-output.js
+    '';
+  });
 in
 
 pkgs.mkShell {
@@ -73,6 +133,7 @@ pkgs.mkShell {
   buildInputs = with ocamlPackages; [
     bos
     cmdliner
+    codex
     crowbar
     digestif
     dolmen_type
diff --git a/src/abs/abs_driver.ml b/src/abs/abs_driver.ml
new file mode 100644
index 000000000..970bdfe89
--- /dev/null
+++ b/src/abs/abs_driver.ml
@@ -0,0 +1,555 @@
+module D = Abs_value.ADomain
+module Size = Abs_value.Size
+
+module Int = struct
+  include Int
+
+  let to_int = Fun.id
+end
+
+module Locals = PatriciaTree.MakeMap (Int)
+
+type value = Abs_value.t
+
+(* type state = *)
+(*   { ctx : D.Context.t *)
+(*   ; stack : Stack.t *)
+(*   ; locals : value Locals.t *)
+(*   ; func_rt : Binary.val_type list *)
+(*   ; env : Abs_extern_func.extern_func Link_env.t *)
+(*   ; envs : Abs_extern_func.extern_func Link_env.t Dynarray.t *)
+(*   } *)
+
+let ( let* ) = Option.bind
+
+module Flags = Operator.Flags
+
+(*===========================================================================*)
+
+module DenotFixpoint (S : Abs_eval_intf.Base) = struct
+  type t = S.State.t
+  module D = S.State.ADom
+
+  module JumpKey = struct
+    (* TODO c'est mieux de définir le type nous même *)
+    type t =
+      | I of int
+      | Ret
+
+    let map : (int -> int) -> t -> t =
+     fun f key -> match key with I i -> I (f i) | Ret -> Ret
+
+    let decr = map Int.pred
+
+    let to_int = function I i -> i | Ret -> -1
+  end
+
+  module JumpTarget = struct
+    module Map = PatriciaTree.MakeMap (JumpKey)
+
+    type 'a t = 'a Map.t
+
+    let of_list = Map.of_list
+
+    let to_list = Map.to_list
+
+    let empty = Map.empty
+
+    let find_opt = Map.find_opt
+
+    let remove = Map.remove
+
+    let add m k state =
+      match Map.find_opt k m with
+      | Some state_list -> Map.add k (state :: state_list) m
+      | None -> Map.add k [ state ] m
+
+    let append (old : 'a list t) (neww : 'a list t) =
+      Map.mapi
+        (fun k el ->
+          match Map.find_opt k old with
+          | Some el' -> List.append el el'
+          | None -> el )
+        neww
+
+    let decr jt =
+      remove (I 0) jt |> to_list
+      |> List.map (fun (k, v) -> (JumpKey.decr k, v))
+      |> of_list
+  end
+
+  let ( let> ) (opt, mapp) f =
+    match opt with Some v -> f (v, mapp) | None -> (None, mapp)
+
+  let serialize ~widens :
+    S.State.t -> S.State.t -> (S.State.t, 'a) D.Context.result =
+   fun state_a state_b ->
+    let gen_new_value ~widens a b (state_a : S.State.t) (state_b : S.State.t)
+      (D.Context.Result (inc, intup, cont)) f =
+      if Abs_value.equal a b then None
+      else
+        let size = Abs_value.size_of a in
+        (* inc : whether the new value is included in the old one
+         * intup : symbolic repr of all variabls that will be created simultaneously
+         * cont : continuation function
+         *)
+        let (D.Context.Result (inc, in_tup, local_cont)) =
+          D.serialize_binary ~size ~widens state_a.ctx (Abs_value.to_binary a)
+            state_b.ctx (Abs_value.to_binary b) (inc, intup)
+        in
+        let cont ctx out_tuple =
+          let integer, out_tuple = local_cont ctx out_tuple in
+          let list, out_tuple = cont ctx out_tuple in
+          let b = Abs_value.of_binary size integer in
+          (f b list, out_tuple)
+        in
+        Some (D.Context.Result (inc, in_tup, cont))
+    in
+    let rec serialize_stack lhs rhs acc_res =
+      match (lhs, rhs) with
+      | [], [] -> acc_res
+      | [], _ :: _ | _ :: _, [] ->
+        Fmt.failwith "join on stacks of different sizes"
+      | v1 :: rest_a, v2 :: rest_b -> begin
+        let r = gen_new_value ~widens v1 v2 state_a state_b acc_res List.cons in
+        serialize_stack rest_a rest_b
+          (match r with Some res -> res | None -> acc_res)
+        end
+    in
+    let (D.Context.Result (included, in_tuple, locals_continue)) =
+      Locals.fold_on_nonequal_union
+        begin fun k v1 v2 res ->
+          let size =
+            (* v1 and v2 should have the same size *)
+            match v1 with
+            | Some v -> Abs_value.size_of v
+            | None -> assert false
+          in
+          let v1 = Option.value v1 ~default:(Abs_value.top size state_a.ctx) in
+          let v2 = Option.value v2 ~default:(Abs_value.top size state_b.ctx) in
+          let f = Locals.add k in
+          match gen_new_value ~widens v1 v2 state_a state_b res f with
+          | Some res -> res
+          | None -> res
+        end
+        state_a.locals state_b.locals
+        (D.Context.Result
+           ( true
+           , D.Context.empty_tuple ()
+           , fun _ctx out -> (state_a.locals, out) ) )
+    in
+    let (D.Context.Result (inc, in_tup, stack_continue)) =
+      serialize_stack
+        (Stack.to_list state_a.stack)
+        (Stack.to_list state_b.stack)
+        (D.Context.Result (included, in_tuple, fun _ctx out -> ([], out)))
+    in
+    let cont ctx out =
+      let stack, out = stack_continue ctx out in
+      let locals, out = locals_continue ctx out in
+      ( { state_a with ctx; stack = Stack.of_list @@ List.rev stack; locals }
+      , out )
+    in
+    D.Context.Result (inc, in_tup, cont)
+
+  let join state_a state_b =
+    let (D.Context.Result (_inc, in_tuple, continue)) =
+      serialize ~widens:false state_a state_b
+    in
+    let ctx, out = D.typed_nondet2 state_a.ctx state_b.ctx in_tuple in
+    fst @@ continue ctx out
+
+  let widen widening_id state_a state_b =
+    let (D.Context.Result (included, in_tuple, continue)) =
+      serialize ~widens:true state_a state_b
+    in
+    let ctx, included, out =
+      D.widened_fixpoint_step ~widening_id ~previous:state_a.ctx
+        ~next:state_b.ctx (included, in_tuple)
+    in
+    let state, _ = continue ctx out in
+    ({ state with ctx }, included)
+
+  let rec eval_expr :
+    t -> Binary.instr Annotated.t list -> t option * t list JumpTarget.t =
+   fun state expr ->
+    let rec loop (state, jt) (expr : Binary.instr Annotated.t list) =
+      match expr with
+      | [] -> (Some state, jt)
+      | instr :: instrs -> (
+        let new_state, new_jt = eval_instr state instr.raw in
+        let new_jt = JumpTarget.append jt new_jt in
+        match new_state with
+        | None -> (None, new_jt)
+        | Some s -> loop (s, new_jt) instrs )
+    in
+    loop (state, JumpTarget.empty) expr
+
+  and eval_func (state : S.State.t) (func : Binary.Func.t) =
+    Log.info (fun m ->
+      m "calling func  : func %s" (Option.value func.id ~default:"anonymous") );
+    let (Bt_raw ((None | Some _), (param_type, result_type))) = func.type_f in
+    let args, caller_popped_stack =
+      Stack.pop_n state.stack (List.length param_type)
+    in
+    let init_value (vt : Binary.val_type) =
+      let size =
+        match vt with
+        | Num_type t -> (
+          match t with I32 -> Size.b32 | I64 -> Size.b64 | _ -> assert false )
+        | Ref_type _ -> assert false
+      in
+      let zero = D.Binary_Forward.biconst ~size Z.zero state.ctx in
+      match vt with
+      | Num_type I32 -> Abs_value.I32 zero
+      | Num_type I64 -> I64 zero
+      | _ -> assert false
+    in
+    let locals =
+      List.map (fun (_str_opt, vt) -> init_value vt) func.locals
+      |> List.mapi (fun i v -> (i, v))
+      |> Locals.of_list
+    in
+    let fn_state : S.State.t =
+      { state with
+        stack = args
+      ; ctx = state.ctx
+      ; func_rt = result_type
+      ; locals
+      }
+    in
+    Log.info (fun m -> m "Func start state : %a" pp_state fn_state);
+    (* TODO: handle mapping *)
+    let func_end_state, _ = eval_expr fn_state func.body.raw in
+    Log.info (fun m ->
+      m "Func end state : %a@."
+        (Fmt.option ~none:(Fmt.any "None") pp_state)
+        func_end_state );
+    (* We should probably copy state and join back the return values in the context here *)
+    let* func_end_state in
+    let stack =
+      Stack.append caller_popped_stack
+      @@ Stack.take (List.length result_type) func_end_state.stack
+    in
+    Some { state with stack }
+
+  and eval_instr : t -> Binary.instr -> t option * t list JumpTarget.t =
+   fun state instr ->
+    Log.debug (fun m ->
+      m "#%a\t\t%a@." (pp_instr ~short:true) instr pp_state state );
+    match instr with
+    | Call idx ->
+      let func = Link_env.get_func state.env idx in
+      begin match func with
+      | Wasm { func; idx } ->
+        let env = Dynarray.get state.envs idx in
+        let r = eval_func { state with env } func in
+        (r, JumpTarget.empty)
+      | Extern { idx } -> (
+        match idx with
+        | 0 ->
+          (* assume that it's correctly typed to returning an i32 *)
+          let v = D.binary_unknown ~size:Size.b32 state.ctx in
+          let stack = Stack.push state.stack (I32 v) in
+          (Some { state with stack }, JumpTarget.empty)
+        | 1 ->
+          (* assume that it's correctly typed to returning an i64 *)
+          let v = D.binary_unknown ~size:Size.b64 state.ctx in
+          let stack = Stack.push state.stack (I64 v) in
+          (Some { state with stack }, JumpTarget.empty)
+        | _ ->
+          Fmt.failwith "Some day we will have proper external function support"
+        )
+      end
+    | Block (_str_opt, _bt, expr) ->
+      (* TODO il faut gérer le mapping pour le cas de None *)
+      let> res, mapping = eval_expr state expr.raw in
+      let state = { state with stack = res.stack; locals = res.locals } in
+      let new_state =
+        match JumpTarget.find_opt (I 0) mapping with
+        | Some br_states -> List.fold_left join state br_states
+        | None -> state
+      in
+      let mapping =
+        (* TODO on peut avoir une paire de (int * map) pour ne pas avoir à decr la liste immédiatement *)
+        JumpTarget.decr mapping
+      in
+      (Some new_state, mapping)
+    | If_else (_, bt, expr_true, expr_false) ->
+      let b, stack = Stack.pop state.stack in
+      let cond = Abs_value.to_boolean state.ctx b in
+      let state_true, jt_true =
+        let> ctx, _ = (D.assume state.ctx cond, JumpTarget.empty) in
+        eval_instr { state with stack; ctx } (Block (None, bt, expr_true))
+      in
+      let state_false, jt_false =
+        let not_cond = D.Boolean_Forward.not state.ctx cond in
+        let> ctx, _ = (D.assume state.ctx not_cond, JumpTarget.empty) in
+        eval_instr { state with stack; ctx } (Block (None, bt, expr_false))
+      in
+      let jt = JumpTarget.append jt_true jt_false in
+      begin match (state_true, state_false) with
+      | Some state_true, Some state_false ->
+        (Some (join state_true state_false), jt)
+      | Some state, None | None, Some state -> (Some state, jt)
+      | None, None ->
+        (* TODO should this be assert false ? *)
+        (None, jt)
+      end
+    | Loop (_str_opt, bt, body) ->
+      let widening_id = Domains.Sig.Widening_Id.fresh () in
+      (* TODO tester si on a besoin de copie *)
+      let initial_state = { state with ctx = D.Context.copy state.ctx } in
+      let rec fixpoint state =
+        let next_state, jt = eval_expr state body.raw in
+        let to_take =
+          match bt with
+          | Some (Bt_raw (_i, (params, _res))) -> List.length params
+          | None -> 0
+        in
+        let shorten_stack stack = Stack.take to_take stack in
+        let next_head =
+          match JumpTarget.find_opt (I 0) jt with
+          | Some jts ->
+            let fp_stack = shorten_stack initial_state.stack in
+            List.fold_left
+              (fun acc state ->
+                let stack = shorten_stack state.stack in
+                join acc { state with stack } )
+              { initial_state with stack = fp_stack }
+              jts
+          | None -> assert false
+        in
+        let widened, included = widen widening_id state next_head in
+        if not included then fixpoint widened
+        else
+          (* fixpoint reached: exit loop, assume condition is false *)
+          let jt = JumpTarget.decr jt in
+          let next_state =
+            Option.bind next_state @@ fun next_state ->
+            let stack = Stack.append next_state.stack initial_state.stack in
+            Some { next_state with stack }
+          in
+          (next_state, jt)
+      in
+      fixpoint state
+    | Br i -> (None, JumpTarget.of_list [ (I i, [ state ]) ])
+    | instr -> (
+      let res = S.eval_instr state instr in
+      match res with
+      | Some s, None -> (Some s, JumpTarget.empty)
+      | None, Some instr -> eval_instr state instr
+      | Some _, Some _ -> (* should not happen *) assert false
+      | None, None -> (* unreachable *) (None, JumpTarget.empty) )
+end
+
+(*===========================================================================*)
+
+module DataState : Abs_eval_intf.Base = struct
+  (*TODO on peut utiliser une exception*)
+  module State = struct
+    module Value = Abs_value
+    module ADom = Abs_value.ADomain
+    module Locals = Locals
+    module Stack = Abs_stack.Make (Value)
+
+    type t =
+      { stack : Stack.t
+      ; ctx : ADom.Context.t
+      ; func_rt : Binary.val_type list
+      ; locals : Value.t Locals.t
+      }
+
+    let pp : Format.formatter -> t -> unit =
+     fun fmt state ->
+      Fmt.pf fmt "{@\n@[<hov 2>  ctx : %a,@;stack : %a,@;locals : %a@]@\n}"
+        D.context_pretty state.ctx
+        (Stack.pp @@ Abs_value.pp state.ctx)
+        state.stack
+        (Fmt.list ~sep:Fmt.semi (Abs_value.pp state.ctx))
+        (Locals.to_list state.locals |> List.map snd)
+  end
+
+  open State
+
+  type t = State.t option * Binary.instr option
+
+  module Binop = struct
+    (* TODO vérifier les overflows *)
+    let binop stack size op =
+      let e1, e2, stack = Stack.pop_2 stack in
+      let lhs, rhs = (Abs_value.to_binary e1, Abs_value.to_binary e2) in
+      let bin_res = op lhs rhs in
+      let r = Abs_value.of_binary size bin_res in
+      let stack = Stack.push stack r in
+      stack
+
+    let add state size =
+      let flags = Flags.Biadd.no_overflow in
+      let op = D.Binary_Forward.biadd ~flags ~size state.ctx in
+      let stack = binop state.stack size op in
+      { state with stack }
+
+    let sub state size =
+      let flags = Operator.Flags.Bisub.no_overflow in
+      let op = D.Binary_Forward.bisub ~flags ~size state.ctx in
+      let stack = binop state.stack size op in
+      { state with stack }
+
+    let mul state size =
+      let flags = Flags.Bimul.pack ~nsw:true ~nuw:true in
+      let op = D.Binary_Forward.bimul ~flags ~size state.ctx in
+      let stack = binop state.stack size op in
+      { state with stack }
+
+    let div state (sx : Text.sx) size =
+      let op =
+        match sx with
+        | S -> D.Binary_Forward.bisdiv ~size state.ctx
+        | U -> D.Binary_Forward.biudiv ~size state.ctx
+      in
+      let stack = binop state.stack size op in
+      { state with stack }
+  end
+
+  module Relop = struct
+    let relop ?(not = None) state size op =
+      let e1, e2, stack = Stack.pop_2 state.stack in
+      let lhs, rhs = (Abs_value.to_binary e1, Abs_value.to_binary e2) in
+      let bool_res = op lhs rhs in
+      let bool_res =
+        match not with
+        | Some v ->
+          D.Boolean_Forward.( && ) state.ctx
+            (D.Boolean_Forward.not state.ctx v)
+            bool_res
+        | None -> bool_res
+      in
+      let r = Abs_value.of_boolean state.ctx size bool_res in
+      let stack = Stack.push stack r in
+      stack
+
+    let _and state size =
+      let op = D.Binary_Forward.band ~size state.ctx in
+      let stack = Binop.binop state.stack size op in
+      { state with stack }
+
+    let _or state size =
+      let op = D.Binary_Forward.bor ~size state.ctx in
+      let stack = Binop.binop state.stack size op in
+      { state with stack }
+
+    let le state (sx : Text.sx) size =
+      let op =
+        match sx with
+        | S -> D.Binary_Forward.bisle ~size state.ctx
+        | U -> D.Binary_Forward.biule ~size state.ctx
+      in
+      let stack = relop state size op in
+      { state with stack }
+
+    let lt state (sx : Text.sx) size =
+      let op =
+        match sx with
+        | S -> D.Binary_Forward.bisle ~size state.ctx
+        | U -> D.Binary_Forward.biule ~size state.ctx
+      in
+      let stack = relop state size op in
+      { state with stack }
+  end
+
+  let eval_i32 state (instr : Binary.i32_instr) =
+    let size = Size.b32 in
+    match instr with
+    | Const i ->
+      let abs_i = D.Binary_Forward.biconst ~size (Z.of_int32 i) state.ctx in
+      let stack = Stack.push state.stack (Abs_value.I32 abs_i) in
+      { state with stack }
+    | Add -> Binop.add state size
+    | Sub -> Binop.sub state size
+    | Mul -> Binop.mul state size
+    | Div sx -> Binop.div state sx size
+    | And -> Relop._and state size
+    | Or -> Relop._or state size
+    | Lt sx -> Relop.lt state sx size
+    | Le sx -> Relop.le state sx size
+    | _ -> Fmt.failwith "not implemented yet"
+
+  let eval_i64 state (instr : Binary.i64_instr) =
+    let size = Size.b64 in
+    match instr with
+    | Const i ->
+      let abs_i =
+        D.Binary_Forward.biconst ~size:Size.b64 (Z.of_int64 i) state.ctx
+      in
+      let stack = Stack.push state.stack (Abs_value.I32 abs_i) in
+      { state with stack }
+    | Add -> Binop.add state size
+    | Sub -> Binop.sub state size
+    | Mul -> Binop.mul state size
+    | Div sx -> Binop.div state sx size
+    | _ -> assert false
+
+  let eval_local state : Binary.local_instr -> _ = function
+    | Get i ->
+      let v = Locals.find i state.locals in
+      let stack = Stack.push state.stack v in
+      { state with stack }
+    | Set i ->
+      let e, stack = Stack.pop state.stack in
+      let locals = Locals.add i e state.locals in
+      { state with stack; locals }
+    | Tee i ->
+      let e, stack = Stack.pop state.stack in
+      let stack = Stack.push stack e in
+      let locals = Locals.add i e state.locals in
+      { state with stack; locals }
+
+  let eval_instr : State.t -> Binary.instr -> t =
+   fun state instr ->
+    match instr with
+    | I32 instr ->
+      let r = eval_i32 state instr in
+      (Some r, None)
+    | I64 instr ->
+      let r = eval_i64 state instr in
+      (Some r, None)
+    | Unreachable ->
+      (*TODO à gèrer proprement*)
+      (None, None)
+    | Local instr ->
+      let state = eval_local state instr in
+      (Some state, None)
+    | Drop ->
+      let _, stack = Stack.pop state.stack in
+      (Some { state with stack }, None)
+    | Nop -> (Some state, None)
+    | ( If_else _ | Call _ | Block _ | Loop _ | Br _ | Br_if _ | Br_table _
+      | Br_on_non_null _ | Br_on_null _ ) as instr ->
+      (Some state, Some instr)
+    | instr ->
+      Fmt.failwith "DataState.eval_instr not implemented for %a"
+        (Binary.pp_instr ~short:true)
+        instr
+end
+
+module ConcreteFixpoint = DenotFixpoint (DataState)
+
+let expr (link_state : Abs_extern_func.extern_func Link.State.t)
+  (m : Abs_extern_func.extern_func Linked.Module.t) =
+  let envs = Link.State.get_envs link_state in
+  let ctx = D.root_context () in
+  let initial_state =
+    { ctx
+    ; stack = Stack.empty
+    ; locals = Locals.empty
+    ; env = m.env
+    ; func_rt = []
+    ; envs
+    }
+  in
+
+  List.iter
+    (fun (e : Binary.expr Annotated.t) ->
+      ConcreteFixpoint.eval_expr initial_state e.raw )
+    m.to_run
diff --git a/src/abs/abs_extern_func.ml b/src/abs/abs_extern_func.ml
new file mode 100644
index 000000000..48114aea3
--- /dev/null
+++ b/src/abs/abs_extern_func.ml
@@ -0,0 +1,13 @@
+module SVA = struct
+  type i32 = Abs_value.ADomain.binary
+
+  type i64 = Abs_value.ADomain.binary
+
+  type f32 = Abs_value.ADomain.binary
+
+  type f64 = Abs_value.ADomain.binary
+
+  type v128 = Abs_value.ADomain.binary
+end
+
+include Extern.Func.Make (SVA) (Result) (Concrete_memory)
diff --git a/src/abs/abs_stack.ml b/src/abs/abs_stack.ml
new file mode 100644
index 000000000..68e706f3c
--- /dev/null
+++ b/src/abs/abs_stack.ml
@@ -0,0 +1,38 @@
+module Make (M : sig type t end) =
+struct
+  type elt = M.t
+
+  type t = elt list
+
+  let empty : M.t list = []
+
+  let pop : t -> M.t * t = function h :: t -> (h, t) | [] -> assert false
+
+  let push : t -> M.t -> t = fun stack v -> v :: stack
+
+  let pop_n : t -> int -> t * t =
+   fun stack n -> (List.take n stack, List.drop n stack)
+
+  let pop_2 : t -> M.t * M.t * t = function
+    | v1 :: v2 :: stack' -> (v1, v2, stack')
+    | _ -> assert false
+
+  let pp : M.t Fmt.t -> Format.formatter -> t -> unit =
+   fun el_fmt fmt t -> Fmt.pf fmt "[%a]" (Fmt.list ~sep:(Fmt.any ", ") el_fmt) t
+
+  let is_empty : t -> bool = fun t -> List.is_empty t
+
+  let to_list : t -> M.t list = fun t -> t
+
+  let of_list : M.t list -> t = fun t -> t
+
+  let append : t -> t -> t = fun x y -> List.append x y
+
+  let take : int -> t -> t = List.take
+
+  let drop : int -> t -> t = List.drop
+
+  let rev : t -> t = List.rev
+
+  let length : t -> int = List.length
+end
diff --git a/src/abs/abs_stack.mli b/src/abs/abs_stack.mli
new file mode 100644
index 000000000..7cba3d376
--- /dev/null
+++ b/src/abs/abs_stack.mli
@@ -0,0 +1,3 @@
+module Make (M : sig
+  type t
+end) : Abs_eval_intf.STACK with type elt = M.t
diff --git a/src/abs/abs_value.ml b/src/abs/abs_value.ml
new file mode 100644
index 000000000..773b2eac1
--- /dev/null
+++ b/src/abs/abs_value.ml
@@ -0,0 +1,66 @@
+module Terms =
+  Terms.Builder.Make (Terms.Condition.ConditionCudd) (Terms.Relations.Equality)
+    ()
+
+module SVA : Single_value_abstraction.Sig.NUMERIC_ENUM = struct
+  include Single_value_abstraction.Ival
+  include Single_value_abstraction.Bitfield
+end
+
+module NonRelationalDomain = Domains.Term_based.Nonrelational.Make (Terms) (SVA)
+
+module ADomain : Codex.Domains.Sig.BASE_WITH_INTEGER =
+  Domains.Term_domain.Make (Terms) (NonRelationalDomain)
+
+module Size = struct
+  let b32 = Units.In_bits.s32
+
+  let b64 = Units.In_bits.of_int 64
+
+  let equal s1 s2 = Units.In_bits.compare s1 s2 = 0
+end
+
+type t =
+  | I32 of ADomain.binary
+  | I64 of ADomain.binary
+
+let pp ctx fmt = function
+  | I32 b -> Fmt.pf fmt "i32 %a" (ADomain.binary_pretty ctx ~size:Size.b32) b
+  | I64 b -> Fmt.pf fmt "i64 %a" (ADomain.binary_pretty ctx ~size:Size.b64) b
+
+let equal v1 v2 =
+  match (v1, v2) with
+  | I32 v1, I32 v2 -> ADomain.Binary.equal v1 v2
+  | I64 v1, I64 v2 -> ADomain.Binary.equal v1 v2
+  | _ -> false
+
+let to_binary = function I32 b -> b | I64 b -> b
+
+let of_binary size binary =
+  match Units.In_bits.to_int size with
+  | 32 -> I32 binary
+  | 64 -> I64 binary
+  | _ -> assert false
+
+let of_boolean ctx size boolean =
+  let true_ = ADomain.Boolean_Forward.true_ ctx in
+  if ADomain.Boolean.equal boolean true_ then
+    (match Units.In_bits.to_int size with
+    | 32 -> I32(ADomain.Binary_Forward.biconst ~size (Z.of_int32 1l) ctx)
+    | 64 -> I64(ADomain.Binary_Forward.biconst ~size (Z.of_int64 1L) ctx)
+    | _ -> assert false)
+  else
+    (match Units.In_bits.to_int size with
+    | 32 -> I32(ADomain.Binary_Forward.biconst ~size (Z.of_int32 1l) ctx)
+    | 64 -> I64(ADomain.Binary_Forward.biconst ~size (Z.of_int64 1L) ctx)
+    | _ -> assert false)
+
+let size_of = function I32 _ -> Size.b32 | I64 _ -> Size.b64
+
+let to_boolean ctx x =
+  let size = Size.b32 in
+  let zero = ADomain.Binary_Forward.biconst ~size Z.zero ctx in
+  ADomain.Binary_Forward.beq ~size ctx (to_binary x) zero
+
+let top size ctx = of_binary size @@ ADomain.binary_empty ~size ctx
+
diff --git a/src/abs/abs_value.mli b/src/abs/abs_value.mli
new file mode 100644
index 000000000..3c4450db1
--- /dev/null
+++ b/src/abs/abs_value.mli
@@ -0,0 +1,29 @@
+module Size : sig
+  val b32 : Units.In_bits.t
+
+  val b64 : Units.In_bits.t
+
+  val equal : Units.In_bits.t -> Units.In_bits.t -> bool
+end
+
+module ADomain : Codex.Domains.Sig.BASE_WITH_INTEGER
+
+type t =
+  | I32 of ADomain.binary
+  | I64 of ADomain.binary
+
+val pp : ADomain.Context.t -> Format.formatter -> t -> unit
+
+val to_binary : t -> ADomain.binary
+
+val of_binary : Units.In_bits.t -> ADomain.binary -> t
+
+val equal : t -> t -> bool
+
+val size_of : t -> Units.In_bits.t
+
+val to_boolean : ADomain.Context.t -> t -> ADomain.boolean
+
+val top : Units.In_bits.t -> ADomain.Context.t -> t
+
+val of_boolean : ADomain.Context.t -> Units.In_bits.t -> ADomain.boolean -> t
diff --git a/src/abs/abs_wasm_ffi.ml b/src/abs/abs_wasm_ffi.ml
new file mode 100644
index 000000000..a9655cac7
--- /dev/null
+++ b/src/abs/abs_wasm_ffi.ml
@@ -0,0 +1,28 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2026 OCamlPro *)
+(* Written by the Owi programmers *)
+
+(* The constraint is used here to make sure we don't forget to define one of
+   the expected FFI functions, this whole file is further constrained such that
+   if one function of M is unused in the FFI module below, an error will be
+   displayed *)
+module M = struct
+  (* let symbol_i32 () = *)
+  (*   Ok *)
+  (*     (Abs_value.ADomain.binary_unknown ~size:Units.In_bits.s32 *)
+  (*        (Abs_value.ADomain.root_context ()) ) *)
+end
+
+(* open M *)
+(* open Abs_extern_func *)
+(* open Abs_extern_func.Syntax *)
+
+let symbolic_extern_module =
+  let functions =
+    [ (* ("i32_symbol", Extern_func (unit ^->. i32, symbol_i32)) *)
+      (* ; ("assume", Extern_func (i32 ^->. unit, assume)) *)
+      (* ; ("assert", Extern_func (i32 ^->. unit, assert')) *)
+      (* ; ("exit", Extern_func (i32 ^->. unit, exit)) *)
+    ]
+  in
+  { Extern.Module.functions; func_type = Abs_extern_func.extern_type }
diff --git a/src/abs/denot_concrete.ml b/src/abs/denot_concrete.ml
new file mode 100644
index 000000000..358306aad
--- /dev/null
+++ b/src/abs/denot_concrete.ml
@@ -0,0 +1,358 @@
+open Syntax
+
+type t =
+  | I32
+  | I64
+
+type bf =
+  | Block
+  | Loop
+  | Func
+
+type bt =
+  { arg : t list
+  ; result : t list
+  }
+
+type l =
+  { form : bf
+  ; ty : bt
+  ; code : Binary.expr
+  }
+
+module Map = PatriciaTree.MakeMap (struct
+  include Int
+
+  let to_int = Fun.id
+end)
+
+type state = l list * sigma * e
+
+(*=========================================================================*)
+
+let pp_t fmt : t -> unit = function
+  | I32 -> Fmt.pf fmt "i32"
+  | I64 -> Fmt.pf fmt "i64"
+
+let pp_l fmt { form; ty; code } =
+  Fmt.pf fmt "(%s (%a)->(%a) %s)"
+    (match form with Block -> "b" | Loop -> "l" | Func -> "f")
+    (Fmt.list ~sep:(Fmt.any ", ") pp_t)
+    ty.arg
+    (Fmt.list ~sep:(Fmt.any ", ") pp_t)
+    ty.result
+    (if List.length code > 0 then "I" else "[]")
+
+let pp_v fmt = function
+  | I32 i -> Fmt.pf fmt "(i32 %ld)" i
+  | I64 i -> Fmt.pf fmt "(i64 %Ld)" i
+
+let print_state ((labels, stack, locals) : state) =
+  Fmt.pr "(%a,,@; %a,,@; %a)@."
+    (Fmt.list ~sep:Fmt.comma pp_l)
+    labels (Stack.pp pp_v) stack
+    (Map.pretty (fun fmt k v -> Fmt.pf fmt "%i -> %a" k pp_v v))
+    locals
+
+let rec input_loop state =
+  match In_channel.input_line In_channel.stdin with
+  | None | Some "n" | Some "" -> ()
+  | Some "p" ->
+    print_state state;
+    input_loop state
+  | Some "q" -> exit 0
+  | _ ->
+    Fmt.pr "Input should be <cr>|n|p@.";
+    input_loop state
+
+let option_get = function Some x -> x | None -> assert false
+
+let func_type_to_bt ((params, results) : Binary.func_type) =
+  let val_type_to_bt : Binary.val_type -> t = function
+    | Num_type Text.I32 -> I32
+    | Num_type Text.I64 -> I64
+    | Ref_type _ -> Fmt.failwith "we don't handle refs for now"
+    | _ -> Fmt.failwith "not handled yet"
+  in
+  let params = List.map snd params in
+  { arg = List.map val_type_to_bt params
+  ; result = List.map val_type_to_bt results
+  }
+
+(*=========================================================================*)
+
+module Binop = struct
+  (* let run_op op e1 e2 = *)
+  (*   match op with *)
+  (*   | `Plus -> *)
+  (*       match e1 with *)
+  (*       | I32  -> Int32.add *)
+  (*       | I64 -> Int64.add *)
+
+  (* let binop stack op = *)
+  (*   let e1, e2, stack = Stack.pop_2 stack in *)
+  (*   match e1, e2 with *)
+  (*   | I64 e1, I64 e2 -> *)
+  (*   | I32 e1, I32 e2 -> *)
+
+  (* let add state size = *)
+  (*   assert false *)
+end
+
+(* let eval_ibinop (state : states) (size : Text.nn) (op : Text.ibinop) : *)
+(*   states Result.t = *)
+(*   match state with *)
+(*   | (l, sigma, rho) :: state' -> begin *)
+(*     match size with *)
+(*     | S32 -> begin *)
+(*       let int32_op = *)
+(*         match op with *)
+(*         | Text.Add -> Int32.add *)
+(*         | Text.Sub -> Int32.sub *)
+(*         | Text.Mul -> Int32.mul *)
+(*         | Text.Div _sx -> Int32.div *)
+(*         | _ -> Fmt.failwith "TODO" *)
+(*       in *)
+(*       match sigma with *)
+(*       | I32 n1 :: I32 n2 :: sigma -> *)
+(*         let n = I32 (int32_op n1 n2) in *)
+(*         Ok ((l, n :: sigma, rho) :: state') *)
+(*       | _ -> Fmt.error_msg "ibinop: (s32) malformed stack" *)
+(*     end *)
+(*     | S64 -> begin *)
+(*       let int64_op = *)
+(*         match op with *)
+(*         | Text.Add -> Int64.add *)
+(*         | Text.Sub -> Int64.sub *)
+(*         | Text.Mul -> Int64.mul *)
+(*         | Text.Div _sx -> Int64.div *)
+(*         | _ -> Fmt.failwith "TODO" *)
+(*       in *)
+(*       match sigma with *)
+(*       | I64 n1 :: I64 n2 :: sigma -> *)
+(*         let n = I64 (int64_op n1 n2) in *)
+(*         Ok ((l, n :: sigma, rho) :: state') *)
+(*       | _ -> Fmt.error_msg "ibinop: (s64) malformed stack" *)
+(*     end *)
+(*   end *)
+(*   | [] -> Fmt.error_msg "empty state" *)
+
+(* let eval_irelop (state : states) (size : Text.nn) (op : Text.irelop) = *)
+(*   match state with *)
+(*   | (l, sigma, rho) :: state' -> begin *)
+(*     match size with *)
+(*     | Text.S32 -> ( *)
+(*       let op = *)
+(*         match op with *)
+(*         | Text.Eq -> Int32.eq *)
+(*         | Ne -> Int32.ne *)
+(*         | Lt s -> ( match s with U -> Int32.lt_u | S -> Int32.lt ) *)
+(*         | Gt s -> ( *)
+(*           fun x y -> *)
+(*             match s with U -> not @@ Int32.le_u x y | S -> not @@ Int32.le x y ) *)
+(*         | Le s -> ( match s with U -> Int32.le_u | S -> Int32.le ) *)
+(*         | Ge s -> ( *)
+(*           fun x y -> *)
+(*             match s with U -> not @@ Int32.lt_u x y | S -> not @@ Int32.lt x y ) *)
+(*       in *)
+(*       match sigma with *)
+(*       | I32 n1 :: I32 n2 :: sigma' -> *)
+(*         let to_int32 x = match x with false -> 0l | true -> 1l in *)
+(*         Ok ((l, I32 (op n1 n2 |> to_int32) :: sigma', rho) :: state') *)
+(*       | _ -> assert false ) *)
+(*     | S64 -> ( *)
+(*       let op = *)
+(*         match op with *)
+(*         | Text.Eq -> Int64.eq *)
+(*         | Ne -> Int64.ne *)
+(*         | Lt s -> ( match s with U -> Int64.lt_u | S -> Int64.lt ) *)
+(*         | Gt s -> ( *)
+(*           fun x y -> *)
+(*             match s with U -> not @@ Int64.le_u x y | S -> not @@ Int64.le x y ) *)
+(*         | Le s -> ( match s with U -> Int64.le_u | S -> Int64.le ) *)
+(*         | Ge s -> ( *)
+(*           fun x y -> *)
+(*             match s with U -> not @@ Int64.lt_u x y | S -> not @@ Int64.lt x y ) *)
+(*       in *)
+(*       match sigma with *)
+(*       | I64 n1 :: I64 n2 :: sigma' -> *)
+(*         let to_int64 x = match x with false -> 0L | true -> 1L in *)
+(*         Ok ((l, I64 (op n1 n2 |> to_int64) :: sigma', rho) :: state') *)
+(*       | _ -> assert false ) *)
+(*   end *)
+(*   | [] -> assert false *)
+
+let i32_binop stack op =
+  let v1, v2, stack = Stack.pop_2 stack in
+  match (v1, v2) with
+  | I32 i1, I32 i2 -> Stack.push stack (I32 (op i1 i2))
+  | _ -> assert false
+
+let eval_i32 (l, sigma, rho) : Binary.i32_instr -> _ = function
+  | Binary.Const i ->
+    let sigma = Stack.push sigma (I32 i) in
+    (l, sigma, rho)
+  | Add ->
+    let sigma = i32_binop sigma Int32.add in
+    (l, sigma, rho)
+  | Sub ->
+    let sigma = i32_binop sigma Int32.sub in
+    (l, sigma, rho)
+  | Mul ->
+    let sigma = i32_binop sigma Int32.mul in
+    (l, sigma, rho)
+  | _ -> assert false
+
+let eval_i64 (l, sigma, rho) : Binary.i64_instr -> _ = function
+  | _ -> assert false
+
+
+module Base : Abs_eval_intf.Base = struct
+  module State = struct
+    module ADom = struct
+      module Context = struct
+        type t = unit
+      end
+    end
+
+    module Value = struct
+      type t =
+        | I32 of int32
+        | I64 of int64
+    end
+  end
+end
+
+let eval_instr ~no_input (instrs : Binary.instr Annotated.t list)
+  ((labels, stack, locals) as state : state) : state Result.t =
+  match instrs with
+  | i :: instrs -> begin
+    if no_input then (
+      let instr_str = Fmt.str "%a" (Binary.pp_instr ~short:false) i.raw in
+      Fmt.pr "# %-40s" instr_str;
+      print_state state )
+    else Fmt.pr "# %a@." (Binary.pp_instr ~short:false) i.raw;
+    let* res, res_instrs =
+      begin match i.raw with
+      | Binary.I32 instr -> Ok (eval_i32 state instr, instrs)
+      | I64 instr -> Ok (eval_i64 state instr, instrs)
+      | Local (Get i) -> (
+        match Map.find_opt i locals with
+        | None -> Fmt.error_msg "local.get: local %i is not set" i
+        | Some v ->
+          let stack = Stack.push stack v in
+          Ok ((labels, stack, locals), instrs) )
+      | Local (Set i) ->
+        let v, stack = Stack.pop stack in
+        let locals = Map.add i v locals in
+        Ok ((labels, stack, locals), instrs)
+      | Local (Tee i) ->
+        let v, stack = Stack.pop stack in
+        let locals = Map.add i v locals in
+        let stack = Stack.push stack v in
+        Ok ((labels, stack, locals), instrs)
+      | Drop ->
+        let _, stack = Stack.pop stack in
+        Ok ((labels, stack, locals), instrs)
+      | Unreachable -> Fmt.error_msg "unreachable"
+      | Block (_str_opt, bt, block_instrs) -> (
+        let ty =
+          match bt with
+          | None -> { arg = []; result = [] }
+          | Some (Bt_raw (_, ft)) -> func_type_to_bt ft
+        in
+        let l' = Some { form = Block; ty; code = [] } in
+        let args = List.take (List.length ty.arg) sigma in
+        let+ res =
+          eval_instr ~no_input block_instrs.raw ((l', args, rho) :: states)
+        in
+        match res with
+        | (_, sigma', rho') :: _ ->
+          ((l, sigma' @ sigma, rho') :: states', instrs)
+        | [] -> assert false )
+      | Loop (_str_opt, bt, block_instrs) -> (
+        let ty =
+          match bt with
+          | None -> { arg = []; result = [] }
+          | Some (Bt_raw (_, ft)) -> func_type_to_bt ft
+        in
+        let l' = Some { form = Loop; ty; code = block_instrs.raw } in
+        let args = List.take (List.length ty.arg) sigma in
+        let+ res =
+          eval_instr ~no_input block_instrs.raw ((l', args, rho) :: states)
+        in
+        match res with
+        | (_, sigma', rho') :: _ ->
+          ((l, sigma' @ sigma, rho') :: states', instrs)
+        | [] -> assert false )
+      | If_else (_str_opt, bt, then_instrs, else_instrs) ->
+        let+ res =
+          match sigma with
+          | I32 0l :: sigma | I64 0L :: sigma ->
+            eval_instr ~no_input
+              [ Binary.Block (_str_opt, bt, then_instrs) |> Annotated.dummy ]
+              ((l, sigma, rho) :: states')
+          | _ ->
+            eval_instr ~no_input
+              [ Binary.Block (_str_opt, bt, else_instrs) |> Annotated.dummy ]
+              ((l, sigma, rho) :: states')
+        in
+        (res, instrs)
+      | Br id -> (
+        match l with
+        | None -> Fmt.error_msg "br: on root (should be typechecked)"
+        | Some lbl when id = 0 -> (
+          match lbl.form with
+          | Block ->
+            let results = List.take (List.length lbl.ty.result) sigma in
+            Ok ((Some lbl, results, rho) :: states', instrs)
+          | Loop ->
+            let args = List.take (List.length lbl.ty.arg) sigma in
+            Ok ((Some lbl, args, rho) :: states', instrs)
+          | Func -> Fmt.error_msg "TODO: br func" )
+        | Some lbl -> (
+          match lbl.form with
+          | Func ->
+            Fmt.error_msg
+              "br: trying to go higher than func (should be typechecked)"
+          | _ -> (
+            match states with
+            | _ :: f -> Ok (f, i :: instrs)
+            | [] -> Fmt.error_msg "br: reached the top (should be typechecked)"
+            ) ) )
+      | Br_if id -> (
+        match sigma with
+        | I32 0l :: sigma | I64 0L :: sigma ->
+          let br = Annotated.dummy (Binary.Br id) in
+          Ok ((l, sigma, rho) :: states', br :: instrs)
+        | _ :: sigma -> Ok ((l, sigma, rho) :: states', instrs)
+        | [] -> Fmt.error_msg "br_if: empty stack" )
+      | Return -> (
+        match states' with
+        | (l', sigma', rho') :: state' ->
+          Ok ((l', sigma @ sigma', rho') :: state', instrs)
+        | [] ->
+          assert (List.length instrs = 0);
+          Ok ([], []) )
+      | instr ->
+        Fmt.error_msg "TODO implement instr %a@\n"
+          (Binary.pp_instr ~short:false)
+          instr
+      end
+    in
+    if not no_input then input_loop res;
+    eval_instr ~no_input res_instrs res
+    end
+  | [] ->
+    print_state states;
+    Ok states
+
+let run ~no_input (m : Binary.Module.t Result.t) =
+  let+ m in
+  let start = m.func.(option_get m.start) in
+  let start = match start with Local a -> a | _ -> assert false in
+  let state = (None, [], Map.empty) :: [] in
+  let res = eval_instr start.body.raw state ~no_input in
+  match res with
+  | Ok _state -> Fmt.pr "Ok@."
+  | Error e -> Fmt.epr "%s@." (Result.err_to_string e)
diff --git a/src/abs/eval/abs_eval_base.ml b/src/abs/eval/abs_eval_base.ml
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/abs/eval/abs_eval_intf.ml b/src/abs/eval/abs_eval_intf.ml
new file mode 100644
index 000000000..a2983dddf
--- /dev/null
+++ b/src/abs/eval/abs_eval_intf.ml
@@ -0,0 +1,60 @@
+module type STACK = sig
+  type elt
+
+  type t
+
+  val empty : t
+
+  val pop : t -> elt * t
+
+  val push : t -> elt -> t
+
+  val pop_n : t -> int -> t * t
+
+  val pop_2 : t -> elt * elt * t
+
+  val pp : elt Fmt.t -> Format.formatter -> t -> unit
+
+  val is_empty : t -> bool
+
+  val to_list : t -> elt list
+
+  val of_list : elt list -> t
+
+  val append : t -> t -> t
+
+  val take : int -> t -> t
+
+  val drop : int -> t -> t
+
+  val rev : t -> t
+
+  val length : t -> int
+end
+
+module type Base = sig
+  module State : sig
+    module ADom : Codex.Domains.Sig.BASE
+
+    module Value : sig
+      type t
+    end
+
+    module Locals : PatriciaTree.MAP with type key = Value.t
+
+    module Stack : STACK
+
+    type t =
+      { stack : Stack.t
+      ; ctx : ADom.Context.t
+      ; func_rt : Binary.val_type list
+      ; locals : Value.t Locals.t
+      }
+  end
+
+  type t = State.t option * Binary.instr option
+
+  val eval_instr : State.t -> Binary.instr -> t
+end
+
+module type Fixpoint = sig end
diff --git a/src/bin/owi.ml b/src/bin/owi.ml
index 9423b9d9c..148cc4be0 100644
--- a/src/bin/owi.ml
+++ b/src/bin/owi.ml
@@ -301,6 +301,34 @@ let symbolic_parameters default_entry_point =
   ; workspace
   }
 
+(* owi drun *)
+
+(* let drun_info = *)
+(*   let doc = "Run the denotational interpreter" in *)
+(*   let man = [] @ shared_man in *)
+(*   Cmd.info "drun" ~version ~doc ~sdocs ~man *)
+(**)
+(* let drun_cmd = *)
+(*   let+ source_file *)
+(*   and+ no_input = *)
+(*     let doc = "disable interactive mode" in *)
+(*     Arg.(value & flag & info [ "no-input" ] ~doc) *)
+(*   and+ () = setup_log in *)
+(*   let compiled = Compile.File.until_binary ~unsafe:false source_file in *)
+(*   Denot_concrete.run ~no_input compiled *)
+
+(* owi ai *)
+
+let abs_info =
+  let doc = "Run the abstract interpreter" in
+  let man = [] @ shared_man in
+  Cmd.info "abs" ~version ~doc ~sdocs ~man
+
+let abs_cmd =
+  let+ source_file
+  and+ () = setup_log in
+  Cmd_abs.cmd ~source_file
+
 (* owi analyze *)
 
 let analyze_info =
@@ -677,6 +705,8 @@ let cli =
   in
   Cmd.group info ~default
     [ Cmd.group analyze_info [ Cmd.v cg_info cg_cmd; Cmd.v cfg_info cfg_cmd ]
+    (* ; Cmd.v drun_info drun_cmd *)
+    ; Cmd.v abs_info abs_cmd
     ; Cmd.v c_info c_cmd
     ; Cmd.v cpp_info cpp_cmd
     ; Cmd.v fmt_info fmt_cmd
diff --git a/src/cmd/cmd_abs.ml b/src/cmd/cmd_abs.ml
new file mode 100644
index 000000000..325fcdcb1
--- /dev/null
+++ b/src/cmd/cmd_abs.ml
@@ -0,0 +1,18 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2026 OCamlPro *)
+(* Written by the Owi programmers *)
+
+open Syntax
+
+let cmd ~source_file =
+  let link_state =
+    Link.State.empty ()
+    |> Link.Extern.modul ~name:"owi" Abs_wasm_ffi.symbolic_extern_module
+  in
+  let+ m, link_state =
+    Compile.File.until_link ~unsafe:true ~name:None link_state source_file
+  in
+  (* let start = match m.start with Some i -> i | None -> assert false in *)
+  (* let f = m.func.(start) in *)
+  (* let expr = match f with Origin.Local f -> f.body | _ -> assert false in *)
+  Abs_driver.expr link_state m
diff --git a/src/dune b/src/dune
index d61cf8ae2..76350acc8 100644
--- a/src/dune
+++ b/src/dune
@@ -3,6 +3,14 @@
 (library
  (public_name owi)
  (modules
+  abs_stack
+  abs_driver
+  abs_eval_base
+  abs_eval_intf
+  abs_extern_func
+  abs_value
+  abs_wasm_ffi
+  denot_concrete
   annotated
   assigned
   benchmark
@@ -15,6 +23,7 @@
   bug
   choice_intf
   call_graph
+  cmd_abs
   cmd_utils
   cmd_c
   cmd_call_graph
@@ -140,6 +149,7 @@
   domainpc
   dune-build-info
   dune-site
+  codex
   fmt
   fmt.cli
   fmt.tty
diff --git a/src/owi.ml b/src/owi.ml
index 6a526748f..3989d0c5a 100644
--- a/src/owi.ml
+++ b/src/owi.ml
@@ -1,7 +1,9 @@
+module Abs_driver = Abs_driver
 module Annotated = Annotated
 module Binary = Binary
 module Binary_validate = Binary_validate
 module Binary_to_text = Binary_to_text
+module Cmd_abs = Cmd_abs
 module Cmd_sym = Cmd_sym
 module Cmd_c = Cmd_c
 module Cmd_call_graph = Cmd_call_graph
@@ -30,6 +32,7 @@ module Concrete_i32 = Concrete_i32
 module Concrete_i64 = Concrete_i64
 module Concrete_f32 = Concrete_f32
 module Concrete_f64 = Concrete_f64
+(* module Denot_concrete =Denot_concrete *)
 module Extern = Extern
 module Init = Init
 module Interpret = Interpret
diff --git a/src/owi.mli b/src/owi.mli
index a7b07217a..225c3877f 100644
--- a/src/owi.mli
+++ b/src/owi.mli
@@ -1265,6 +1265,10 @@ module Link : sig
 end
 
 module Compile : sig
+  module File : sig
+    val until_binary : unsafe:bool -> Fpath.t -> Binary.Module.t Result.t
+  end
+
   module Text : sig
     val until_binary : unsafe:bool -> Text.Module.t -> Binary.Module.t Result.t
 
@@ -1411,6 +1415,17 @@ module Symbolic_extern_func : sig
   end
 end
 
+module Abs_driver : sig
+  val expr :
+       Abs_extern_func.extern_func Link.State.t
+    -> Abs_extern_func.extern_func Linked.Module.t
+    -> unit
+end
+
+(* module Denot_concrete : sig
+  val run : no_input:bool -> Binary.Module.t Result.t -> unit Result.t
+end *)
+
 module Interpret : sig
   module type Parameters = sig
     val use_ite_for_select : bool
@@ -1514,6 +1529,10 @@ module Symbolic_driver : sig
     -> unit Result.t
 end
 
+module Cmd_abs : sig
+  val cmd : source_file:Fpath.t -> unit Result.t
+end
+
 module Cmd_sym : sig
   val cmd :
     parameters:Symbolic_parameters.t -> source_file:Fpath.t -> unit Result.t
diff --git a/test/abs/add.wat b/test/abs/add.wat
new file mode 100644
index 000000000..8e674f4b3
--- /dev/null
+++ b/test/abs/add.wat
@@ -0,0 +1,10 @@
+(module
+  (func $start
+    i32.const 42
+    i32.const 28
+    i32.sub
+    return
+  )
+
+  (start $start)
+)
diff --git a/test/abs/fact.wat b/test/abs/fact.wat
new file mode 100644
index 000000000..f680efa55
--- /dev/null
+++ b/test/abs/fact.wat
@@ -0,0 +1,40 @@
+(module
+  (func $start (result i32)
+    (local $n i32)
+    (local $result i32)
+    
+    i32.const 5
+    local.set $n
+    
+    i32.const 1
+    local.set $result
+    
+    (block $done
+      (loop $continue
+        ;; if n <= 1, exit
+        local.get $n
+        i32.const 1
+        i32.le_s
+        br_if $done
+        
+        ;; result *= n
+        local.get $result
+        local.get $n
+        i32.mul
+        local.set $result
+        
+        ;; n--
+        local.get $n
+        i32.const 1
+        i32.sub
+        local.set $n
+        
+        br $continue
+      )
+    )
+    
+    local.get $result
+  )
+  
+  (start $start)
+)
diff --git a/test/abs/if.wat b/test/abs/if.wat
new file mode 100644
index 000000000..38f546ce3
--- /dev/null
+++ b/test/abs/if.wat
@@ -0,0 +1,15 @@
+(module
+  (func $start
+    i32.const 42
+    i32.const 28
+
+    i32.const 0
+    (if (param i32) (param i32) (result i32)
+      (then i32.add)
+      (else i32.sub))
+
+    drop
+  )
+
+  (start $start)
+)
diff --git a/test/abs/local_func.wat b/test/abs/local_func.wat
new file mode 100644
index 000000000..eff1f23b8
--- /dev/null
+++ b/test/abs/local_func.wat
@@ -0,0 +1,16 @@
+(module
+  (func $add (param $i i32) (result i32)
+    local.get $i
+    nop (; should be top ;)
+    i32.add
+    return
+  )
+
+  (func $start
+    i32.const 42
+    call $add
+    return
+  )
+
+  (start $start)
+)
diff --git a/test/abs/loop.wat b/test/abs/loop.wat
new file mode 100644
index 000000000..3976d4791
--- /dev/null
+++ b/test/abs/loop.wat
@@ -0,0 +1,15 @@
+(module
+  (func $start
+    (local $res i32)
+    i32.const 0
+    (loop (param i32) (result i32)
+      (local.get $res)
+      i32.const 2
+      i32.add
+      (local.tee $res)
+      br 0)
+    drop
+  )
+
+  (start $start)
+)
diff --git a/test/abs/return.wat b/test/abs/return.wat
new file mode 100644
index 000000000..880c9c23c
--- /dev/null
+++ b/test/abs/return.wat
@@ -0,0 +1,8 @@
+(module
+  (func $start
+    i32.const 2
+    return
+  )
+
+  (start $start)
+)