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

Sep 29, 2026

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

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.

Mustafa Arslan

Independent Researcher Istanbul, Türkiye

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

Ask PDF

May 29, 2026

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

Formal methods provide rigorous accounts of program behavior, but practical software engineering often works through executable libraries, tests, and incremental design. This paper presents SEMBridge, a small tagless-final framework for generating weakest-precondition and bounded-checking interpretations from the same executable object programs. Instead of committing a program semantics to one abstract syntax tree and then writing separate traversals, object programs are written once against a semantic interface and interpreted into multiple meanings: readable code, concrete execution, predicate transformers, bounded counterexample search, and future proof-assistant or SMT back ends. The Python prototype implements a loop-free imperative core with assignments, conditionals, assumptions, and assertions. Across five example programs, the same tagless-final definitions generated executable state transformers and verification conditions that passed bounded checking over domains up to 729 states. The contribution is not a Scala code-generation system or a new verifier, but a compact architecture for keeping executable semantics, weakest-precondition artifacts, and bounded validation synchronized.

Eric Liang

Oracle

Bounded Model Checking Formal Verification

Ask PDF

Oct 23, 2026

SemantEq: Faithful Bidirectional Equivalence of Formal Statements

Statement autoformalization translates mathematics from natural language into a proof assistant such as Lean 4, and models now do it at scale. As provers get stronger, the burden of correctness shifts from the proof to the statement, that is, to whether the formal statement faithfully translates its source. Given a trusted reference formalization, the natural test is logical equivalence, and it proves too much.

P \leftrightarrow Q

holds trivially for any two statements

P

and

Q

that the library proves, because a prover can prove each separately and pass through

P \leftrightarrow \mathrm{True} \leftrightarrow Q

. The stronger the prover, the more unrelated pairs pass. Earlier methods restrict the prover and check that each proof names the other statement. We introduce SemantEq, a more principled relation that instead requires each statement to turn into the other only through a chain of allowed steps, such as logical rearrangement and rewriting with the library's own equations. Our programs judge a proof by the proof term Lean checks, not by its tactic script. SemantEq-Eval, a search without a model, reaches 100% precision and 65.6% recall on the ProofNetVerif test split under our adjudicated labels, against 95.8% and 61.8% for BEq+, and an 8.9-fold increase in its CPU time adds at most three pairs. A language model finds more proofs, but under two of four prompts it proves both directions of about two in five of the non-equivalent pairs. SemantEq-ProofAudit audits each model-written proof under a policy derived from the relation and accepts none of the 104 non-equivalent pairs, and it raises recall on 407 equivalent pairs from 65.4% to 81.1% under the best prompt. Separating the generation of equivalence proofs from their acceptance lets a stronger prover raise recall without changing what an acceptance means. We release code and data at: https://github.com/hlxr89/SemantEq

Xinrui Li, Pawan Sasanka Ammanamanchi, Siddharth Bhat +3

EleutherAI · Carnegie Mellon University · University of Cambridge +1

Formal Verification Lean Theorem Proving Autoformalization Large Language Model-Guided Theorem Proving

Ask PDF

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