AVOC

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

1 \usepackage[a4paper,margin=23mm,headheight=15pt]{geometry}
2 \usepackage[T1]{fontenc}
3 \usepackage{lmodern,microtype}
4 \usepackage{amsmath,amssymb,amsthm,mathtools}
5 \usepackage{graphicx,xcolor,booktabs,longtable,array,tabularx}
6 \usepackage{enumitem,fancyhdr,lastpage,listings,float}
7 \usepackage{xurl}
8 \usepackage[hidelinks]{hyperref}
9 \definecolor{navy}{HTML}{16354A}
10 \definecolor{teal}{HTML}{007D80}
11 \definecolor{amber}{HTML}{B57524}
12 \definecolor{light}{HTML}{F0F5F7}
13 \definecolor{ink}{HTML}{263846}
14 \color{ink}
15 \setlength{\emergencystretch}{3em}
16 \setlength{\parindent}{0pt}
17 \setlength{\parskip}{0.5em}
18 \setlist{itemsep=0.2em,topsep=0.3em}
19 \newtheorem{theorem}{Theorem}[section]
20 \newtheorem{proposition}[theorem]{Proposition}
21 \newtheorem{lemma}[theorem]{Lemma}
22 \newtheorem{corollary}[theorem]{Corollary}
23 \theoremstyle{definition}
24 \newtheorem{definition}[theorem]{Definition}
25 \newtheorem{example}[theorem]{Example}
26 \theoremstyle{remark}
27 \newtheorem{remark}[theorem]{Remark}
28 \newcommand{\Q}{\mathbb Q}
29 \newcommand{\R}{\mathbb R}
30 \newcommand{\N}{\mathbb N}
31 \newcommand{\E}{\mathbb E}
32 \newcommand{\Prob}{\mathbb P}
33 \newcommand{\avocdate}{7 October 2026}
34 \newcommand{\avocsubtitle}{Certified Artifact Planning, Calibration, and Recoverable Execution}
35 \providecommand{\paperkind}{Publication edition}
36 \newcommand{\note}[2]{\begin{quote}\textcolor{teal}{\textbf{#1}}\par #2\end{quote}}
37 \newcommand{\fig}[3]{\begin{figure}[H]\centering\includegraphics[width=\linewidth]{#1}\caption{#2}\label{#3}\end{figure}}
38 \graphicspath{{../figures/}{figures/}}
39 \pagestyle{fancy}\fancyhf{}
40 \fancyhead[L]{\small\textcolor{navy}{AVOC / Certified artifact planning}}
41 \fancyhead[R]{\small\paperkind}
42 \fancyfoot[L]{\small Komorebi P.\quad $\cdot$\quad \avocdate}
43 \fancyfoot[R]{\small\thepage\,/\,\pageref{LastPage}}
44 \renewcommand{\headrulewidth}{0.3pt}
45 \hypersetup{pdfauthor={Komorebi P.},pdftitle={AVOC: Certified Artifact Planning, Calibration, and Recoverable Execution},pdfsubject={Publication edition based on AVOC Formal v0.41.0}}
46 \lstdefinelanguage{Lean}{keywords={import,namespace,end,open,def,theorem,lemma,structure,inductive,where,by,exact,apply,intro,have,show,match,with,if,then,else,fun,let,in,private,noncomputable,instance,variable,abbrev,example,deriving},sensitive=true,morecomment=[l]{--},morecomment=[s]{/-}{-/},morestring=[b]"}
47 \lstdefinestyle{LeanCode}{language=Lean,basicstyle=\ttfamily\footnotesize,breaklines=true,columns=fullflexible,keepspaces=true,showstringspaces=false,backgroundcolor=\color{light},frame=single,rulecolor=\color{light},keywordstyle=\color{navy},commentstyle=\color{teal},aboveskip=0.7em,belowskip=0.7em,
48  literate={∀}{{$\forall$}}1 {∃}{{$\exists$}}1 {→}{{$\to$}}1 {↔}{{$\leftrightarrow$}}1 {⇒}{{$\Rightarrow$}}1 {←}{{$\leftarrow$}}1 {∈}{{$\in$}}1 {∉}{{$\notin$}}1 {≤}{{$\le$}}1 {≥}{{$\ge$}}1 {≠}{{$\ne$}}1 {ℕ}{{$\mathbb N$}}1 {ℚ}{{$\mathbb Q$}}1 {ℝ}{{$\mathbb R$}}1 {ℤ}{{$\mathbb Z$}}1 {Ω}{{$\Omega$}}1 {α}{{$\alpha$}}1 {β}{{$\beta$}}1 {κ}{{$\kappa$}}1 {δ}{{$\delta$}}1 {ε}{{$\varepsilon$}}1 {π}{{$\pi$}}1 {ω}{{$\omega$}}1 {σ}{{$\sigma$}}1 {τ}{{$\tau$}}1 {μ}{{$\mu$}}1 {λ}{{$\lambda$}}1 {Θ}{{$\Theta$}}1 {ξ}{{$\xi$}}1 {η}{{$\eta$}}1 {ν}{{$\nu$}}1 {χ}{{$\chi$}}1 {θ}{{$\theta$}}1 {ρ}{{$\rho$}}1 {Γ}{{$\Gamma$}}1 {Σ}{{$\Sigma$}}1 {∧}{{$\land$}}1 {∨}{{$\lor$}}1 {¬}{{$\neg$}}1 {×}{{$\times$}}1 {⊆}{{$\subseteq$}}1 {⊂}{{$\subset$}}1 {⟨}{{$\langle$}}1 {⟩}{{$\rangle$}}1 {∑}{{$\sum$}}1 {∏}{{$\prod$}}1 {∣}{{$\mid$}}1 {∘}{{$\circ$}}1 {↑}{{$\uparrow$}}1 {↓}{{$\downarrow$}}1 {▸}{{$\triangleright$}}1 {₀}{{$_0$}}1 {₁}{{$_1$}}1 {₂}{{$_2$}}1 {₃}{{$_3$}}1 {₄}{{$_4$}}1 {₅}{{$_5$}}1 {₆}{{$_6$}}1 {₇}{{$_7$}}1 {₈}{{$_8$}}1 {₉}{{$_9$}}1}
49 \lstset{style=LeanCode}
50 \newcommand{\avoccover}[2]{\hypersetup{pageanchor=false}\begin{titlepage}\color{navy}
51  \vspace*{16mm}{\large KOMOREBI\quad /\quad REALIZATION CALCULUS\par}
52  \vspace{17mm}{\Huge\bfseries AVOC\par}
53  \vspace{9mm}{\LARGE\bfseries Certified Artifact Planning,\\[2mm]Calibration, and\\[2mm]Recoverable Execution\par}
54  \vspace{14mm}{\Large #1\par}\vspace{10mm}\rule{\linewidth}{0.6pt}
55  \vspace{8mm}{\normalsize #2\par}
56  \vfill{\large Komorebi P.\par}\vspace{3mm}{\avocdate\quad /\quad Publication edition 1.0\par}
57  \end{titlepage}\hypersetup{pageanchor=true}}

Back to source controls

Back to AVOC