diff --git a/ivette/src/frama-c/plugins/wp/api/tac/index.ts b/ivette/src/frama-c/plugins/wp/api/tac/index.ts
index b39fef289e3cf56bf3093f04bd01f0da82030c82..ee290243ed1d4610fe4ce2b696a50a7522296b46 100644
--- a/ivette/src/frama-c/plugins/wp/api/tac/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tac/index.ts
@@ -37,6 +37,14 @@ import * as Server from 'frama-c/server';
 //@ts-ignore
 import * as State from 'frama-c/states';
 
+//@ts-ignore
+import { byNode } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
+import { jNode } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
+import { node } from 'frama-c/plugins/wp/api/tip';
+//@ts-ignore
+import { nodeDefault } from 'frama-c/plugins/wp/api/tip';
 
 /** Parameter kind */
 export type kind =
@@ -256,31 +264,25 @@ export const tacticalDataDefault: tacticalData =
   { id: Json.jKey<'#tactic'>('#tactic')(''), label: '', title: '',
     error: undefined, status: statusDefault, params: [] };
 
-const configureTactics_internal: Server.ExecRequest<
-  { node: Json.index<'#node'> },
-  null
-  > = {
+const configureTactics_internal: Server.ExecRequest<{ node: node },null> = {
   kind: Server.RqKind.EXEC,
   name: 'plugins.wp.tac.configureTactics',
-  input: Json.jObject({ node: Json.jIndex<'#node'>('#node'),}),
+  input: Json.jObject({ node: jNode,}),
   output: Json.jNull,
   signals: [ { name: 'plugins.wp.tip.printStatus' } ],
 };
 /** Configure all tactics */
-export const configureTactics: Server.ExecRequest<
-  { node: Json.index<'#node'> },
-  null
-  >= configureTactics_internal;
+export const configureTactics: Server.ExecRequest<{ node: node },null>= configureTactics_internal;
 
 const setParameter_internal: Server.ExecRequest<
-  { node: Json.index<'#node'>, tactic: Json.key<'#tactic'>,
-    param: Json.key<'#param'>, value: Json.json },
+  { node: node, tactic: Json.key<'#tactic'>, param: Json.key<'#param'>,
+    value: Json.json },
   null
   > = {
   kind: Server.RqKind.EXEC,
   name: 'plugins.wp.tac.setParameter',
   input: Json.jObject({
-           node: Json.jIndex<'#node'>('#node'),
+           node: jNode,
            tactic: Json.jKey<'#tactic'>('#tactic'),
            param: Json.jKey<'#param'>('#param'),
            value: Json.jAny,
@@ -290,25 +292,19 @@ const setParameter_internal: Server.ExecRequest<
 };
 /** Configure tactical parameter */
 export const setParameter: Server.ExecRequest<
-  { node: Json.index<'#node'>, tactic: Json.key<'#tactic'>,
-    param: Json.key<'#param'>, value: Json.json },
+  { node: node, tactic: Json.key<'#tactic'>, param: Json.key<'#param'>,
+    value: Json.json },
   null
   >= setParameter_internal;
 
-const applyTactic_internal: Server.ExecRequest<
-  Json.key<'#tactic'>,
-  Json.index<'#node'>[]
-  > = {
+const applyTactic_internal: Server.ExecRequest<Json.key<'#tactic'>,node[]> = {
   kind: Server.RqKind.EXEC,
   name: 'plugins.wp.tac.applyTactic',
   input: Json.jKey<'#tactic'>('#tactic'),
-  output: Json.jArray(Json.jIndex<'#node'>('#node')),
+  output: Json.jArray(jNode),
   signals: [],
 };
 /** Applies the (configured) tactic */
-export const applyTactic: Server.ExecRequest<
-  Json.key<'#tactic'>,
-  Json.index<'#node'>[]
-  >= applyTactic_internal;
+export const applyTactic: Server.ExecRequest<Json.key<'#tactic'>,node[]>= applyTactic_internal;
 
 /* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/wp/api/tip/index.ts b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
index 5d4df9da28b041d11a689d297032d62d14255dcd..4e60c09639b549869a59530c4588c5454aeafe28 100644
--- a/ivette/src/frama-c/plugins/wp/api/tip/index.ts
+++ b/ivette/src/frama-c/plugins/wp/api/tip/index.ts
@@ -75,15 +75,27 @@ export const proofStatus: Server.Signal = {
   name: 'plugins.wp.tip.proofStatus',
 };
 
+/** Proof Node index */
+export type node = Json.index<'#node'>;
+
+/** Decoder for `node` */
+export const jNode: Json.Decoder<node> = Json.jIndex<'#node'>('#node');
+
+/** Natural order for `node` */
+export const byNode: Compare.Order<node> = Compare.number;
+
+/** Default value for `node` */
+export const nodeDefault: node = Json.jIndex<'#node'>('#node')(-1);
+
 const getNodeInfos_internal: Server.GetRequest<
-  Json.index<'#node'>,
+  node,
   { result: string, proved: boolean, pending: number, size: number,
     stats: string, results: [ prover, result ][], tactic: string,
-    children: [ string, Json.index<'#node'> ][] }
+    children: [ string, node ][] }
   > = {
   kind: Server.RqKind.GET,
   name: 'plugins.wp.tip.getNodeInfos',
-  input: Json.jIndex<'#node'>('#node'),
+  input: jNode,
   output: Json.jObject({
             result: Json.jString,
             proved: Json.jBoolean,
@@ -92,33 +104,28 @@ const getNodeInfos_internal: Server.GetRequest<
             stats: Json.jString,
             results: Json.jArray(Json.jPair( jProver, jResult,)),
             tactic: Json.jString,
-            children: Json.jArray(
-                        Json.jPair(
-                          Json.jString,
-                          Json.jIndex<'#node'>('#node'),
-                        )),
+            children: Json.jArray(Json.jPair( Json.jString, jNode,)),
           }),
   signals: [ { name: 'plugins.wp.tip.proofStatus' } ],
 };
 /** Proof node information */
 export const getNodeInfos: Server.GetRequest<
-  Json.index<'#node'>,
+  node,
   { result: string, proved: boolean, pending: number, size: number,
     stats: string, results: [ prover, result ][], tactic: string,
-    children: [ string, Json.index<'#node'> ][] }
+    children: [ string, node ][] }
   >= getNodeInfos_internal;
 
 const getProofState_internal: Server.GetRequest<
   goal,
-  { current: Json.index<'#node'>, path: Json.index<'#node'>[], index: number,
-    pending: number }
+  { current: node, path: node[], index: number, pending: number }
   > = {
   kind: Server.RqKind.GET,
   name: 'plugins.wp.tip.getProofState',
   input: jGoal,
   output: Json.jObject({
-            current: Json.jIndex<'#node'>('#node'),
-            path: Json.jArray(Json.jIndex<'#node'>('#node')),
+            current: jNode,
+            path: Json.jArray(jNode),
             index: Json.jNumber,
             pending: Json.jNumber,
           }),
@@ -127,8 +134,7 @@ const getProofState_internal: Server.GetRequest<
 /** Current Proof Status of a Goal */
 export const getProofState: Server.GetRequest<
   goal,
-  { current: Json.index<'#node'>, path: Json.index<'#node'>[], index: number,
-    pending: number }
+  { current: node, path: node[], index: number, pending: number }
   >= getProofState_internal;
 
 const goForward_internal: Server.SetRequest<goal,null> = {
@@ -161,25 +167,25 @@ const goToIndex_internal: Server.SetRequest<[ goal, number ],null> = {
 /** Go to k-th pending node of proof tree */
 export const goToIndex: Server.SetRequest<[ goal, number ],null>= goToIndex_internal;
 
-const goToNode_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+const goToNode_internal: Server.SetRequest<node,null> = {
   kind: Server.RqKind.SET,
   name: 'plugins.wp.tip.goToNode',
-  input: Json.jIndex<'#node'>('#node'),
+  input: jNode,
   output: Json.jNull,
   signals: [],
 };
 /** Set current node of associated proof tree */
-export const goToNode: Server.SetRequest<Json.index<'#node'>,null>= goToNode_internal;
+export const goToNode: Server.SetRequest<node,null>= goToNode_internal;
 
-const removeNode_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+const removeNode_internal: Server.SetRequest<node,null> = {
   kind: Server.RqKind.SET,
   name: 'plugins.wp.tip.removeNode',
-  input: Json.jIndex<'#node'>('#node'),
+  input: jNode,
   output: Json.jNull,
   signals: [],
 };
 /** Remove node from tree and go to parent */
-export const removeNode: Server.SetRequest<Json.index<'#node'>,null>= removeNode_internal;
+export const removeNode: Server.SetRequest<node,null>= removeNode_internal;
 
 /** Updated TIP printer */
 export const printStatus: Server.Signal = {
@@ -221,15 +227,14 @@ export const byRformat: Compare.Order<rformat> = Compare.structural;
 export const rformatDefault: rformat = "ratio";
 
 const printSequent_internal: Server.ExecRequest<
-  { node: Json.index<'#node'>, indent?: number, margin?: number,
-    iformat?: iformat, rformat?: rformat, autofocus?: boolean,
-    unmangled?: boolean },
+  { node: node, indent?: number, margin?: number, iformat?: iformat,
+    rformat?: rformat, autofocus?: boolean, unmangled?: boolean },
   text
   > = {
   kind: Server.RqKind.EXEC,
   name: 'plugins.wp.tip.printSequent',
   input: Json.jObject({
-           node: Json.jIndex<'#node'>('#node'),
+           node: jNode,
            indent: Json.jOption(Json.jNumber),
            margin: Json.jOption(Json.jNumber),
            iformat: Json.jOption(jIformat),
@@ -242,31 +247,30 @@ const printSequent_internal: Server.ExecRequest<
 };
 /** Pretty-print the associated node */
 export const printSequent: Server.ExecRequest<
-  { node: Json.index<'#node'>, indent?: number, margin?: number,
-    iformat?: iformat, rformat?: rformat, autofocus?: boolean,
-    unmangled?: boolean },
+  { node: node, indent?: number, margin?: number, iformat?: iformat,
+    rformat?: rformat, autofocus?: boolean, unmangled?: boolean },
   text
   >= printSequent_internal;
 
-const clearSelection_internal: Server.SetRequest<Json.index<'#node'>,null> = {
+const clearSelection_internal: Server.SetRequest<node,null> = {
   kind: Server.RqKind.SET,
   name: 'plugins.wp.tip.clearSelection',
-  input: Json.jIndex<'#node'>('#node'),
+  input: jNode,
   output: Json.jNull,
   signals: [],
 };
 /** Reset node selection */
-export const clearSelection: Server.SetRequest<Json.index<'#node'>,null>= clearSelection_internal;
+export const clearSelection: Server.SetRequest<node,null>= clearSelection_internal;
 
 const setSelection_internal: Server.SetRequest<
-  { node: Json.index<'#node'>, part?: Json.key<'#part'>,
-    term?: Json.key<'#term'>, extend?: boolean },
+  { node: node, part?: Json.key<'#part'>, term?: Json.key<'#term'>,
+    extend?: boolean },
   null
   > = {
   kind: Server.RqKind.SET,
   name: 'plugins.wp.tip.setSelection',
   input: Json.jObject({
-           node: Json.jIndex<'#node'>('#node'),
+           node: jNode,
            part: Json.jOption(Json.jKey<'#part'>('#part')),
            term: Json.jOption(Json.jKey<'#term'>('#term')),
            extend: Json.jOption(Json.jBoolean),
@@ -276,8 +280,8 @@ const setSelection_internal: Server.SetRequest<
 };
 /** Set node selection */
 export const setSelection: Server.SetRequest<
-  { node: Json.index<'#node'>, part?: Json.key<'#part'>,
-    term?: Json.key<'#term'>, extend?: boolean },
+  { node: node, part?: Json.key<'#part'>, term?: Json.key<'#term'>,
+    extend?: boolean },
   null
   >= setSelection_internal;
 
diff --git a/ivette/src/frama-c/plugins/wp/goals.tsx b/ivette/src/frama-c/plugins/wp/goals.tsx
index 535c7713344ee09f22cfebeb8fb9928cae23b46e..349d1f2c2f144105788669a60323f107f3e731c9 100644
--- a/ivette/src/frama-c/plugins/wp/goals.tsx
+++ b/ivette/src/frama-c/plugins/wp/goals.tsx
@@ -98,9 +98,9 @@ function filterGoal(
 
 export interface GoalTableProps {
   display: boolean;
-  scope: Ast.decl | undefined;
   failed: boolean;
-  current: WP.goal;
+  scope: Ast.decl | undefined;
+  current: WP.goal | undefined;
   setCurrent: (goal: WP.goal) => void;
   setTIP: (goal: WP.goal) => void;
   setGoals: (goals: number) => void;
diff --git a/ivette/src/frama-c/plugins/wp/index.tsx b/ivette/src/frama-c/plugins/wp/index.tsx
index 872aa980024d662ba40c46660e940093193f6932..5e7967660147b419b1eb8b3a2dc7cd7203cf3d6d 100644
--- a/ivette/src/frama-c/plugins/wp/index.tsx
+++ b/ivette/src/frama-c/plugins/wp/index.tsx
@@ -42,15 +42,14 @@ import './style.css';
 /* --- Goal Component                                                     --- */
 /* -------------------------------------------------------------------------- */
 
+type Goal = WP.goal | undefined;
+
 function WPGoals(): JSX.Element {
   const [scoped, flipScoped] = Dome.useFlipSettings('frama-c.wp.goals.scoped');
   const [failed, flipFailed] = Dome.useFlipSettings('frama-c.wp.goals.failed');
   const [displayTip, setTip] = React.useState(false);
-  const [current, setCurrent] = React.useState(WP.goalDefault);
-  Server.useShutdown(() => {
-    setTip(false);
-    setCurrent(WP.goalDefault);
-  });
+  const [current, setCurrent] = React.useState<Goal>(undefined);
+  Server.useShutdown(() => { setTip(false); setCurrent(undefined); });
   const scope = States.useCurrentScope();
   const [goals, setGoals] = React.useState(0);
   const [total, setTotal] = React.useState(0);
diff --git a/ivette/src/frama-c/plugins/wp/tip.tsx b/ivette/src/frama-c/plugins/wp/tip.tsx
index 1ed009f33136bd58c1e6c6caf5cc27a44ef45b59..fe686b4f6f0af24d7aedc9c194e53c22565d3243 100644
--- a/ivette/src/frama-c/plugins/wp/tip.tsx
+++ b/ivette/src/frama-c/plugins/wp/tip.tsx
@@ -28,27 +28,57 @@ import * as WP from 'frama-c/plugins/wp/api';
 import * as TIP from 'frama-c/plugins/wp/api/tip';
 import { getStatus } from './goals';
 
+/* -------------------------------------------------------------------------- */
+/* --- Goal View                                                          --- */
+/* -------------------------------------------------------------------------- */
+
+type Node = TIP.node | undefined;
+
+const nodeToString = (node: Node): string =>
+  node === undefined ? '-' : `#${node}`;
+
+interface GoalViewProps {
+  node: Node;
+}
+
+function GoalView(props: GoalViewProps): JSX.Element {
+  return <Cell label={`Node ${nodeToString(props.node)}`}/>;
+}
+
 /* -------------------------------------------------------------------------- */
 /* --- TIP View                                                           --- */
 /* -------------------------------------------------------------------------- */
 
-export interface TIPProps {
-  display: boolean;
-  goal: WP.goal;
+interface ProofState {
+  current: Node;
+  index: number;
+  pending: number;
+}
+
+function useProofState(target: WP.goal | undefined): ProofState {
+  const DefaultProofState: ProofState = {
+    current: undefined, index: 0, pending: 0
+  };
+  return States.useRequest(
+    TIP.getProofState,
+    target,
+    { onError: DefaultProofState }
+  ) ?? DefaultProofState;
 }
 
 function useTarget(target: WP.goal | undefined) : WP.goalsData {
-  const data = States.useSyncArrayElt( WP.goals, target );
-  return data ?? WP.goalsDataDefault;
+  return States.useSyncArrayElt( WP.goals, target ) ?? WP.goalsDataDefault;
+}
+
+export interface TIPProps {
+  display: boolean;
+  goal: WP.goal | undefined;
 }
 
 export function TIPView(props: TIPProps): JSX.Element {
   const { display, goal } = props;
-  const target = goal !== WP.goalDefault ? goal : undefined;
-  const infos: WP.goalsData = useTarget(goal);
-  const status = getStatus(infos);
-  const { index=0, pending=0 } =
-    States.useRequest( TIP.getProofState, target ) ?? {};
+  const infos = useTarget(goal);
+  const { current, index, pending } = useProofState(goal);
   return (
     <Vfill display={display}>
       <Hbox>
@@ -57,10 +87,11 @@ export function TIPView(props: TIPProps): JSX.Element {
           label={infos.wpo} title='Goal identifier' />
         <Cell
           icon='CODE'
-          display={pending > 0}
-          label={`${index+1}/${pending}`} title='Pending proof nodes'/>
-        <Cell {...status}/>
+          display={0 <= index && index < pending}
+          label={`${index}/${pending}`} title='Pending proof nodes'/>
+        <Cell {...getStatus(infos)}/>
       </Hbox>
+      <GoalView node={current} />
     </Vfill>
   );
 }
diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml
index 5263a3a674a41ae62b193917edb04d00b538d47d..e6eca6e75142063b6da985731af53b6a1c5f0a3b 100644
--- a/src/plugins/wp/wpTipApi.ml
+++ b/src/plugins/wp/wpTipApi.ml
@@ -42,7 +42,12 @@ let package = P.package ~plugin:"wp" ~name:"tip"
 let proofStatus = R.signal ~package ~name:"proofStatus"
     ~descr:(Md.plain "Proof Status has changed")
 
-module Node = D.Index(Map.Make(ProofEngine.Node))(struct let name = "node" end)
+module Node =
+struct
+  include D.Index(Map.Make(ProofEngine.Node))(struct let name = "node" end)
+  let jtype =
+    D.declare ~package ~name:"node" ~descr:(Md.plain "Proof Node index") jtype
+end
 
 let () =
   let inode = R.signature ~input:(module Node) () in