A Reversible Semantics for Janus

Ivan Lanese; Germán Vidal

cs.PLFeb 18, 2026

A Reversible Semantics for Janus

Authors: Ivan Lanese, Germán Vidal

Organizations: Olas Team, University of Bologna & Inria - Université Côte d’Azur, Bologna, Italy · VRAIN, Universitat Politècnica de València, Valencia, Spain

Abstract

Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions with concurrency primitives) is not reversible, since it loses information while computing forwards. E.g., it does not satisfy the Loop Lemma, stating that any reduction has an inverse, a main property of reversibility in process calculi, where a small-step semantics is commonly used. We present here a novel small-step semantics which is actually reversible, while remaining equivalent to the previous one. It involves the non-trivial challenge of defining a semantics based on a "program counter" for a high-level programming language.

Figures & tables

\frac{~}{\sigma\vdash c\Downarrow\llbracket c\rrbracket}\quad\textsc{left=Con}\frac{~}{\sigma\vdash x\Downarrow\sigma(x)}\quad\textsc{left=Var}\frac{\sigma\vdash e\Downarrow\sigma\vdash v}{\sigma\vdash x[e]\Downarrow x[v]}\quad\textsc{left=Arr}\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\llbracket\odot\rrbracket(v_{1},v_{2})=v}{\sigma\vdash e_{1}\odot e_{2}\Downarrow v}\quad\textsc{left=Bop}

Figure 2: Semantics of expressions

\frac{\sigma\vdash e\Downarrow v}{\sigma\vdash x~\oplus=e\Downarrow\sigma[x\mapsto\llbracket\oplus\rrbracket(\sigma(x),v)]}\quad\textsc{left=AssVar}\frac{\sigma\vdash e_{l}\Downarrow v_{l}\quad\sigma\vdash e\Downarrow v}{\sigma\vdash x[e_{l}]~\oplus=e\Downarrow\sigma[x[v_{l}]\mapsto\llbracket\oplus\rrbracket(\sigma(x[v_{l}]),v)]}\quad\textsc{left=AssArr}\frac{\sigma\vdash\Gamma(id)\Downarrow\sigma^{\prime}}{\sigma\vdash\mathsf{call}~id\Downarrow\sigma^{\prime}}\quad\textsc{left=Call}\frac{\sigma\vdash\mathcal{I}\llbracket\Gamma(id)\rrbracket\Downarrow\sigma^{\prime}}{\sigma\vdash\mathsf{uncall}~id\Downarrow\sigma^{\prime}}\quad\textsc{left=UnCall}\frac{\sigma\vdash s_{1}\Downarrow\sigma^{\prime}\quad\sigma^{\prime}\vdash s_{2}\Downarrow\sigma^{\prime\prime}}{\sigma\vdash s_{1}~s_{2}\Downarrow\sigma^{\prime\prime}}\quad\textsc{left=Seq}\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})\quad\sigma\vdash s_{1}\Downarrow\sigma^{\prime}\quad\sigma^{\prime}\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})}{\sigma\vdash\mathsf{if}~e_{1}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~e_{2}\Downarrow\sigma^{\prime}}\quad\textsc{left=IfTrue}\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})\quad\sigma\vdash s_{2}\Downarrow\sigma^{\prime}\quad\sigma^{\prime}\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})}{\sigma\vdash\mathsf{if}~e_{1}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~e_{2}\Downarrow\sigma^{\prime}}\quad\textsc{left=IfFalse}\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})\quad\sigma\vdash s_{1}\Downarrow\sigma^{\prime}\quad\sigma^{\prime}\vdash(e_{1},s_{1},e_{2},s_{2})\Downarrow\sigma^{\prime\prime}}{\sigma\vdash\mathsf{from}~e_{1}~\mathsf{do}~s_{1}~\mathsf{loop}~s_{2}~\mathsf{until}~e_{2}\Downarrow\sigma^{\prime\prime}}\quad\textsc{left=LoopMain}\frac{\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})}{\sigma\vdash(e_{1},s_{1},e_{2},s_{2})\Downarrow\sigma}\quad\textsc{left=LoopBase}\frac{\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})\quad\sigma\vdash s_{2}\Downarrow\sigma^{\prime}\quad\sigma^{\prime}\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})\quad\sigma^{\prime}\vdash s_{1}\Downarrow\sigma^{\prime\prime}\quad\sigma^{\prime\prime}\vdash(e_{1},s_{1},e_{2},s_{2})\Downarrow\sigma^{\prime\prime\prime}}{\sigma\vdash(e_{1},s_{1},e_{2},s_{2})\Downarrow\sigma^{\prime\prime\prime}}\quad\textsc{left=LoopRec}\frac{~}{\sigma\vdash\mathsf{skip}\Downarrow\sigma}\quad\textsc{left=Skip}

Figure 3: Big-step semantics of sequential Janus

\frac{\sigma\vdash e\Downarrow v}{\langle\sigma,x~\oplus=e,\pi\rangle\rightarrow\langle\sigma[x\mapsto\llbracket\oplus\rrbracket(\sigma(x),v)],\mathsf{skip},\pi\rangle}\quad\textsc{left=AssVarS}\frac{\sigma\vdash e_{l}\Downarrow v_{l}\quad\sigma\vdash e\Downarrow v}{\langle\sigma,x[e_{l}]~\oplus=e,\pi\rangle\rightarrow\langle\sigma[x[v_{l}]\mapsto\llbracket\oplus\rrbracket(\sigma(x[v_{l}]),v)],\mathsf{skip},\pi\rangle}\quad\textsc{left=AssArrS}\frac{~}{\langle\sigma,\mathsf{call}~id,\pi\rangle\rightarrow\langle\sigma,\Gamma(id),\pi\rangle}\quad\textsc{left=CallS}\frac{~}{\langle\sigma,\mathsf{uncall}~id,\pi\rangle\rightarrow\langle\sigma,\mathcal{I}\llbracket\Gamma(id)\rrbracket,\pi\rangle}\quad\textsc{left=UnCallS}\frac{~}{\langle\sigma,s_{1}~s_{2},\pi\rangle\rightarrow\langle\sigma,s_{1},\mathsf{seq}(s_{2})\!:\!\pi\rangle}\quad\textsc{left=Seq1}\frac{~}{\langle\sigma,\mathsf{skip},\mathsf{seq}(s_{2})\!:\!\pi\rangle\rightarrow\langle\sigma,s_{2},\pi\rangle}\quad\textsc{left=Seq2}

Figure 5: Small-step semantics: rules for basic constructs

\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})\quad}{\langle\sigma,\mathsf{if}~e_{1}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~e_{2},\pi\rangle\rightarrow\langle\sigma,s_{1},\mathsf{if\_true}(e_{2})\!:\!\pi\rangle}\quad\textsc{left=IfTrue1}\frac{\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})\quad}{\langle\sigma,\mathsf{skip},\mathsf{if\_true}(e_{2})\!:\!\pi\rangle\rightarrow\langle\sigma,\mathsf{skip},\pi\rangle}\quad\textsc{left=IfTrue2}\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})\quad}{\langle\sigma,\mathsf{if}~e_{1}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~e_{2},\pi\rangle\rightarrow\langle\sigma,s_{2},\mathsf{if\_false}(e_{2})\!:\!\pi\rangle}\quad\textsc{left=IfFalse1}\frac{\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})\quad}{\langle\sigma,\mathsf{skip},\mathsf{if\_false}(e_{2})\!:\!\pi\rangle\rightarrow\langle\sigma,\mathsf{skip},\pi\rangle}\quad\textsc{left=IfFalse2}\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})}{\langle\sigma,\mathsf{from}~e_{1}~\mathsf{do}~s_{1}~\mathsf{loop}~s_{2}~\mathsf{until}~e_{2},\pi\rangle\rightarrow\langle\sigma,s_{1},\mathsf{loop1}(e_{1},s_{1},e_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{left=LoopMainS}\frac{\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})}{\langle\sigma,\mathsf{skip},\mathsf{loop1}(e_{1},s_{1},e_{2},s_{2})\!:\!\pi\rangle\rightarrow\langle\sigma,\mathsf{skip},\pi\rangle}\quad\textsc{left=LoopBaseS}\frac{\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})}{\langle\sigma,\mathsf{skip},\mathsf{loop1}(e_{1},s_{1},e_{2},s_{2})\!:\!\pi\rangle\rightarrow\langle\sigma,s_{2},\mathsf{loop2}(e_{1},s_{1},e_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{left=Loop1}\frac{\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})}{\langle\sigma,\mathsf{skip},\mathsf{loop2}(e_{1},s_{1},e_{2},s_{2})\!:\!\pi\rangle\rightarrow\langle\sigma,s_{1},\mathsf{loop1}(e_{1},s_{1},e_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{left=Loop2}

Figure 6: Small-step semantics: rules for if and for loop

Panel of Figure 11 — Figure 11: CFGs for program Sum3

\frac{\mathit{block}(\ell^{\prime})=(x~\oplus=e)\quad\sigma\vdash e\Downarrow v\quad\ell^{\prime}\longrightarrow\ell^{\prime\prime}}{\langle\sigma,\ell,\ell^{\prime},\pi\rangle\rightharpoonup\langle\sigma[x\mapsto\llbracket\oplus\rrbracket(\sigma(x),v)],\ell^{\prime},\ell^{\prime\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{AssVar}}

}\frac{\mathit{block}(\ell^{\prime})=(x[e_{l}]~\oplus=e)\quad\sigma\vdash e_{l}\Downarrow v_{l}\quad\sigma\vdash e\Downarrow v\quad\ell^{\prime}\longrightarrow\ell^{\prime\prime}}{\langle\sigma,\ell,\ell^{\prime},\pi\rangle\rightharpoonup\langle\sigma[x[v_{l}]\mapsto\llbracket\oplus\rrbracket(\sigma(x[v_{l}]),v)],\ell^{\prime},\ell^{\prime\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{AssArr}}

}\frac{\mathit{block}(\ell^{\prime})=(\mathsf{call}~id)\quad\mathit{entry}(\Gamma(id))\longrightarrow\ell^{\prime\prime}}{\langle\sigma,\ell,\ell^{\prime},\pi\rangle\rightharpoonup\langle\sigma,\mathit{entry}(\Gamma(id)),\ell^{\prime\prime},\mathsf{call}(\ell^{\prime})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{Call}}

}\frac{\mathit{block}(\ell^{\prime})=\mathsf{stop}\quad\ell^{\prime\prime}\longrightarrow\ell^{\prime\prime\prime}}{\langle\sigma,\ell,\ell^{\prime},\mathsf{call}(\ell^{\prime\prime})\!:\!\pi\rangle\rightharpoonup\langle\sigma,\ell^{\prime\prime},\ell^{\prime\prime\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{Return1}}

}\frac{\mathit{block}(\ell^{\prime})=(\mathsf{uncall}~id)\quad\mathit{entry}(\Gamma(id^{-1}))\longrightarrow\ell^{\prime\prime}}{\langle\sigma,\ell,\ell^{\prime},\pi\rangle\rightharpoonup\langle\sigma,\mathit{entry}(\Gamma(id^{-1})),\ell^{\prime\prime},\mathsf{uncall}(\ell^{\prime})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{UnCall}}

}\frac{\mathit{block}(\ell^{\prime})=\mathsf{stop}\quad\ell^{\prime\prime}\longrightarrow\ell^{\prime\prime\prime}}{\langle\sigma,\ell,\ell^{\prime},\mathsf{uncall}(\ell^{\prime\prime})\!:\!\pi\rangle\rightharpoonup\langle\sigma,\ell^{\prime\prime},\ell^{\prime\prime\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{Return2}}

}\frac{\mathit{block}(\ell^{\prime})=\mathsf{skip}\quad\ell^{\prime}\longrightarrow\ell^{\prime\prime}}{\langle\sigma,\ell,\ell^{\prime},\pi\rangle\rightharpoonup\langle\sigma,\ell^{\prime},\ell^{\prime\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{Skip}}

}

Figure 12: Reversible forward semantics: rules for basic constructs

\frac{\mathit{block}(\ell_{1})=e_{1}\quad\mathsf{ctx}(\ell_{1})=(\mathsf{if}~[e_{1}]^{\ell_{1}}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~[e_{2}]^{\ell_{2}})\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})}{\langle\sigma,\ell,\ell_{1},\pi\rangle\rightharpoonup\langle\sigma,\ell_{1},\mathit{entry}(s_{1}),\mathsf{if\_true}(\ell_{1},\ell_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{IfTrue1}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})\quad\ell_{2}\longrightarrow\ell^{\prime}_{2}}{\langle\sigma,\ell,\ell_{2},\mathsf{if\_true}(\ell_{1},\ell_{2})\!:\!\pi\rangle\rightharpoonup\langle\sigma,\ell_{2},\ell^{\prime}_{2},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{IfTrue2}}

}\frac{\mathit{block}(\ell_{1})=e_{1}\quad\mathsf{ctx}(\ell_{1})=(\mathsf{if}~[e_{1}]^{\ell_{1}}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~[e_{2}]^{\ell_{2}})\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})}{\langle\sigma,\ell,\ell_{1},\pi\rangle\rightharpoonup\langle\sigma,\ell_{1},\mathit{entry}(s_{2}),\mathsf{if\_false}(\ell_{1},\ell_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{IfFalse1}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})\quad\ell_{2}\longrightarrow\ell^{\prime}_{2}}{\langle\sigma,\ell,\ell_{2},\mathsf{if\_false}(\ell_{1},\ell_{2})\!:\!\pi\rangle\rightharpoonup\langle\sigma,\ell_{2},\ell^{\prime}_{2},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{IfFalse2}}

}\frac{\mathit{block}(\ell_{1})=e_{1}\quad\mathsf{ctx}(\ell_{1})=(\mathsf{from}~[e_{1}]^{\ell_{1}}~\mathsf{do}~s_{1}~\mathsf{loop}~s_{2}~\mathsf{until}~[e_{2}]^{\ell_{2}})\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})}{\langle\sigma,\ell,\ell_{1},\pi\rangle\rightharpoonup\langle\sigma,\ell_{1},\mathit{entry}(s_{1}),\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{LoopMain}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})\quad\ell_{2}\longrightarrow\ell^{\prime}_{2}\quad\ell^{\prime}_{2}\neq\mathit{entry}(s_{1})}{\langle\sigma,\ell,\ell_{2},\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle\rightharpoonup\langle\sigma,\ell_{2},\ell^{\prime}_{2},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{LoopBase}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})}{\langle\sigma,\ell,\ell_{2},\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle\rightharpoonup\langle\sigma,\ell_{2},\mathit{entry}(s_{2}),\mathsf{loop2}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{Loop1}}

}\frac{\mathit{block}(\ell_{1})=e_{1}\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})}{\langle\sigma,\ell,\ell_{1},\mathsf{loop2}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle\rightharpoonup\langle\sigma,\ell_{1},\mathit{entry}(s_{1}),\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overrightarrow{\mathit{Loop2}}

}

Figure 13: Reversible forward semantics: rules for if and for loop

\frac{}{[\>]\sim_{\mathit{stack}}[\>]}\frac{\pi\sim_{\mathit{stack}}\pi^{\prime}}{\mathsf{seq}(s)\!:\!\pi\sim_{\mathit{stack}}\pi^{\prime}}\frac{\pi\sim_{\mathit{stack}}\pi^{\prime}}{\pi\sim_{\mathit{stack}}\mathsf{call}(\ell)\!:\!\pi^{\prime}}\frac{\pi\sim_{\mathit{stack}}\pi^{\prime}}{\pi\sim_{\mathit{stack}}\mathsf{uncall}(\ell)\!:\!\pi^{\prime}}\frac{\mathsf{ctx}(\ell_{2})=(\mathsf{if}~[e_{1}]^{\ell_{1}}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~[e_{2}]^{\ell_{2}})\quad\pi\sim_{\mathit{stack}}\pi^{\prime}}{\mathsf{if\_true}([e_{2}]^{\ell_{2}})\!:\!\pi\sim_{\mathit{stack}}\mathsf{if\_true}(\ell_{1},\ell_{2})\!:\!\pi^{\prime}}\frac{\mathsf{ctx}(\ell_{2})=(\mathsf{if}~[e_{1}]^{\ell_{1}}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~[e_{2}]^{\ell_{2}})\quad\pi\sim_{\mathit{stack}}\pi^{\prime}}{\mathsf{if\_false}([e_{2}]^{\ell_{2}})\!:\!\pi\sim_{\mathit{stack}}\mathsf{if\_false}(\ell_{1},\ell_{2})\!:\!\pi^{\prime}}\frac{\pi\sim_{\mathit{stack}}\pi^{\prime}}{\mathsf{loop1}([e_{1}]^{\ell_{1}},s_{1},[e_{2}]^{\ell_{2}},s_{2})\!:\!\pi\sim_{\mathit{stack}}\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi^{\prime}}\frac{\pi\sim_{\mathit{stack}}\pi^{\prime}}{\mathsf{loop2}([e_{1}]^{\ell_{1}},s_{1},[e_{2}]^{\ell_{2}},s_{2})\!:\!\pi\sim_{\mathit{stack}}\mathsf{loop2}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi^{\prime}}

Figure 14: Equivalence relation on stacks “

\sim_{\mathit{stack}}

”

\frac{\mathit{block}(\ell^{\prime})=(x~\oplus=e)\quad\sigma\vdash e\Downarrow v\quad\ell^{\prime\prime}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell^{\prime}}{\langle\sigma,\ell^{\prime},\ell^{\prime\prime},\pi\rangle\leftharpoondown\langle\sigma[x\mapsto\mathcal{I}_{op}\llbracket\oplus\rrbracket(\sigma(x),v)],\ell,\ell^{\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{AssVar}}

}\frac{\mathit{block}(\ell^{\prime})=(x[e_{l}]~\oplus=e)\quad\sigma\vdash e_{l}\Downarrow v_{l}\quad\sigma\vdash e\Downarrow v\quad\ell^{\prime\prime}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell^{\prime}}{\langle\sigma,\ell^{\prime},\ell^{\prime\prime},\pi\rangle\leftharpoondown\langle\sigma[x[v_{l}]\mapsto\mathcal{I}_{op}\llbracket\oplus\rrbracket(\sigma(x[v_{l}]),v)],\ell,\ell^{\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{AssArr}}

}\frac{\mathit{block}(\ell_{s})=\mathsf{start}\quad\ell^{\prime}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell}{\langle\sigma,\ell_{s},\ell^{\prime\prime},\mathsf{call}(\ell^{\prime})\!:\!\pi\rangle\leftharpoondown\langle\sigma,\ell,\ell^{\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{Call}}

}\frac{\mathit{block}(\ell^{\prime\prime})=(\mathsf{call}~id)\quad\mathit{exit}(\Gamma(\mathit{id}))\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell}{\langle\sigma,\ell^{\prime\prime},\ell^{\prime\prime\prime},\pi\rangle\leftharpoondown\langle\sigma,\ell,\mathit{exit}(\Gamma(\mathit{id})),\mathsf{call}(\ell^{\prime\prime})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{Return1}}

}\frac{\mathit{block}(\ell_{s})=\mathsf{start}\quad\ell^{\prime}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell}{\langle\sigma,\ell_{s},\ell^{\prime\prime},\mathsf{uncall}(\ell^{\prime})\!:\!\pi\rangle\leftharpoondown\langle\sigma,\ell,\ell^{\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{UnCall}}

}\frac{\mathit{block}(\ell^{\prime\prime})=(\mathsf{uncall}~id)\quad\mathit{exit}(\Gamma(\mathit{id}^{-1}))\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell}{\langle\sigma,\ell^{\prime\prime},\ell^{\prime\prime\prime},\pi\rangle\leftharpoondown\langle\sigma,\ell,\mathit{exit}(\Gamma(\mathit{id}^{-1})),\mathsf{uncall}(\ell^{\prime\prime})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{Return2}}

}\frac{\mathit{block}(\ell^{\prime})=\mathsf{skip}\quad\ell^{\prime\prime}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell^{\prime}\quad}{\langle\sigma,\ell^{\prime},\ell^{\prime\prime},\pi\rangle\leftharpoondown\langle\sigma,\ell,\ell^{\prime},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{Skip}}

}

Figure 16: Reversible backward semantics: rules for basic constructs

\frac{\mathit{block}(\ell_{1})=e_{1}\quad\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})\quad\ell_{1}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell\quad}{\langle\sigma,\ell_{1},\ell^{\prime}_{1},\mathsf{if\_true}(\ell_{1},\ell_{2})\!:\!\pi\rangle\leftharpoondown\langle\sigma,\ell,\ell_{1},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{IfTrue1}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\mathsf{ctx}(\ell_{2})=(\mathsf{if}~[e_{1}]^{\ell_{1}}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~[e_{2}]^{\ell_{2}})\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})\quad}{\langle\sigma,\ell_{2},\ell^{\prime}_{2},\pi\rangle\leftharpoondown\langle\sigma,\mathit{exit}(s_{1}),\ell_{2},\mathsf{if\_true}(\ell_{1},\ell_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{IfTrue2}}

}\frac{\mathit{block}(\ell_{1})=e_{1}\quad\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})\quad\ell_{1}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell\quad}{\langle\sigma,\ell_{1},\ell^{\prime}_{1},\mathsf{if\_false}(\ell_{1},\ell_{2})\!:\!\pi\rangle\leftharpoondown\langle\sigma,\ell,\ell_{1},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{IfFalse1}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\mathsf{ctx}(\ell_{2})=(\mathsf{if}~[e_{1}]^{\ell_{1}}~\mathsf{then}~s_{1}~\mathsf{else}~s_{2}~\mathsf{fi}~[e_{2}]^{\ell_{2}})\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})\quad}{\langle\sigma,\ell_{2},\ell^{\prime}_{2},\pi\rangle\leftharpoondown\langle\sigma,\mathit{exit}(s_{2}),\ell_{2},\mathsf{if\_false}(\ell_{1},\ell_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{IfFalse2}}

}\frac{\mathit{block}(\ell_{1})=e_{1}\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_true?}(v_{1})\quad\ell_{1}\stackrel{{\scriptstyle\mbox{\tiny-1}}}{{\longrightarrow}}\ell\quad\ell\neq\mathit{exit}(s_{2})}{\langle\sigma,\ell_{1},\ell^{\prime},\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle\leftharpoondown\langle\sigma,\ell,\ell_{1},\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{LoopMain}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\mathsf{ctx}(\ell_{2})=(\mathsf{from}~[e_{1}]^{\ell_{1}}~\mathsf{do}~s_{1}~\mathsf{loop}~s_{2}~\mathsf{until}~[e_{2}]^{\ell_{2}})\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_true?}(v_{2})\quad}{\langle\sigma,\ell_{2},\ell^{\prime}_{2},\pi\rangle\leftharpoondown\langle\sigma,\mathit{exit}(s_{1}),\ell_{2},\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{LoopBase}}

}\frac{\mathit{block}(\ell_{2})=e_{2}\quad\sigma\vdash e_{2}\Downarrow v_{2}\quad\mathsf{is\_false?}(v_{2})}{\langle\sigma,\ell_{2},\ell^{\prime},\mathsf{loop2}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle\leftharpoondown\langle\sigma,\mathit{exit}(s_{1}),\ell_{2},\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{Loop1}}

}\frac{\mathit{block}(\ell_{1})=e_{1}\quad\sigma\vdash e_{1}\Downarrow v_{1}\quad\mathsf{is\_false?}(v_{1})}{\langle\sigma,\ell_{1},\ell^{\prime},\mathsf{loop1}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle\leftharpoondown\langle\sigma,\mathit{exit}(s_{2}),\ell_{1},\mathsf{loop2}(\ell_{1},s_{1},\ell_{2},s_{2})\!:\!\pi\rangle}\quad\textsc{leftstyle=\rm,left=

\overleftarrow{\mathit{Loop2}}

}

Figure 17: Reversible backward semantics: rules for if and for loop

Janus: Evidence-Before-Effect Sagas and Offline-Verifiable Provenance for Agentic LLMs
Sep 29, 2026Mustafa ArslanLLM Auditing AI Agent Governance
Independent Researcher Istanbul, Türkiye
SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
May 29, 2026Eric LiangBounded Model Checking Formal Verification
Oracle
SemantEq: Faithful Bidirectional Equivalence of Formal Statements
Oct 23, 2026Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat +3Formal Verification Lean Theorem Proving
EleutherAI · Carnegie Mellon University · University of Cambridge +1

Sep 29, 2026J/K move · Enter open · S save

Janus: Evidence-Before-Effect Sagas and Offline-Verifiable Provenance for Agentic LLMs

Mustafa Arslan

Independent Researcher Istanbul, Türkiye

LLM Auditing AI Agent Governance LLM Agent Safety Tool Access Control for LLM Agents

Open paper AskPDF arXiv

Agentic large language models (LLMs) now move money through tools, yet the record of what they did is usually a trace their own process emits beside the effect. Janus puts the record on the effect path. A step's proposal, the verdict on it and any answer from a validator or a person are durable in a signed, hash-chained log before the step may run or its effect be released; with keys declared, each answer is signed by whoever gave or relayed it. Gates are pure functions of that log, and an auditor re-derives every verdict offline from the log and one public key. At the MCP edge the effect is held until then; through the SDK, which our model experiment uses, a cooperating client runs it only afterwards. We evaluate Janus under crash injection (144 kills in-process, 81 through the daemon), by verifying a 100-million-event log offline (254.5 s), and with a real model behind a lending workflow, run governed and plain on the same recorded model outputs. With the lending mandate in the model's prompt, the comparison was 0 against 0. With it only in the policy and the amount's unit stated, the model approved six loans declared over the mandate, three with no injection (a run that also dropped the unit approved three); the plain agent paid all six and Janus none, each refused by a deterministic validator and re-derivable offline. An always-approve oracle over the recorded intakes gave 20 and 21 declared over the mandate against 0, though Janus paid four and three whose declared amount understated the request. Designing the experiment exposed, in a system that passed its own audit, an instance of post-approval substitution: an approval keyed to an attempt was counted for a different proposal, moving a person's approval from 100 to 1,000,000. We report it, a first fix and the five routes around it, and what Janus does not guarantee.

Abstract

Explore similar work

Janus: Evidence-Before-Effect Sagas and Offline-Verifiable Provenance for Agentic LLMs

SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations

SemantEq: Faithful Bidirectional Equivalence of Formal Statements