Writing pf2 Annotations

Proof annotations live in your documentation comments using the prove:pf2 marker. This page teaches the annotation format end to end: how the kernel uses an annotation for soundness, the block structure, where the annotation goes in each language, how to handle code the kernel cannot translate, and how caching keeps re-verification fast.

After this page you will be able to write a complete proof annotation on a real function, choose the right blocks for what you are proving, place the annotation correctly for your language, and know exactly what to do when a function touches something the kernel cannot reason about directly.

How the Kernel Uses an Annotation

An annotation is the mechanism that ties a formal proof to the code it describes. Verification works in three steps:

1. The code is translated to a formal representation. The language parser reads the annotated code and produces a representation of what it does in the kernel's term language, so the proof cannot claim behavior the code does not have.
2. The kernel reads the annotation. From the documentation comment it extracts the theorem name, the statement, and the proof script (structured steps that reduce to primitive inference rules).
3. The kernel checks the proof against the code. The proof must be consistent with the formal representation. A proof cannot lie about what the code does: if it claims a property that contradicts the code, the kernel rejects it.

This grounds every verified annotation in the actual implementation, not just the author's intent. Where a construct cannot be translated (foreign calls, inline assembly, hardware access, reflection), you record the boundary as an explicit cited assumption, described under Documenting External Dependencies below, so what is assumed versus proved is always visible.

The prove:pf2 Marker

Every proof annotation begins with the marker prove:pf2("theorem_name") inside a documentation comment. The theorem name uniquely identifies the proof within your project. The marker tells the scanner that the comment contains a pf2 proof to verify.

/* prove:pf2("my_theorem_name")
\[
  ... proof body ...
\]
*/

The \[ and \] delimiters wrap the LaTeX proof content. Everything between them is parsed as structured proof notation.

Annotation Shape

Every annotation contains these core elements:

• Theorem name: unique within the project, declared in the prove:pf2("name") marker
• Statement: expressed in the kernel’s term language, declaring what the proof establishes
• Proof script: structured steps that reduce to primitive rules the kernel can check

Optionally, annotations can also include:

• Domain and category: for organizing proofs in the dashboard
• Dependencies: references to other theorems this proof builds on
• Pre/post conditions: formal contracts the function must satisfy

LaTeX Sections

A range of structured block types can appear inside the \[ ... \] delimiters. Only the proof block is required; all others are optional or recommended. The kernel parses the proof block and skips over any other \begin{...} environment up to its matching \end{...}, so the section vocabulary is open-ended. The most common sections are listed below.

Section	Purpose	Required?
\begin{doc}	Human-readable narrative explaining the theorem	Optional
\begin{sig}	Type signature of the function	Recommended
\begin{params}	Function parameters and their types	Optional
\begin{returns}	Return type and description	Optional
\begin{pre}	Preconditions (HOL boolean expressions)	Optional
\begin{post}	Postconditions (HOL boolean expressions)	Optional
\begin{throws}	Exception and error conditions	Optional
\begin{fields}	Struct or class fields	Optional
\begin{columns}	SQL table columns	Optional
\begin{variants}	Enum variants or union cases	Optional
\begin{methods}	Trait or interface methods	Optional
\begin{laws}	Algebraic laws the type must satisfy	Optional
\begin{invariant}	Loop, struct, or module invariant	Optional
\begin{establishes}	Constructor guarantees	Optional
\begin{releases}	Destructor resource cleanup guarantees	Optional
\begin{sideeffects}	Observable state changes	Optional
\begin{proof}	Proof steps using pf2 syntax	REQUIRED

Comment Syntax by Language

The prove:pf2 marker goes inside your language's documentation comment syntax. Annotations always live in documentation comments, not regular comments.

Language	Comment Syntax
Rust	/// prove:pf2("name") or /* prove:pf2("name") ... */
TypeScript, JavaScript	/** prove:pf2("name") ... */ (JSDoc)
Python	# prove:pf2("name") (line prefix)
Objective-C	/* prove:pf2("name") ... */ or // prove:pf2("name")
Dart	/// prove:pf2("name") or /* prove:pf2("name") ... */
Go	/* prove:pf2("name") ... */
Java	/** prove:pf2("name") ... */ (Javadoc)
C#	/* prove:pf2("name") ... */
C++	/* prove:pf2("name") ... */
C	/* prove:pf2("name") ... */
Swift	/* prove:pf2("name") ... */
Kotlin	/** prove:pf2("name") ... */ (KDoc)
Haskell	{- prove:pf2("name") ... -} or -- prove:pf2("name")
Ada	-- prove:pf2("name") (line prefix)
Lua	-- prove:pf2("name") (line prefix)
SQL	-- prove:pf2("name") (line prefix)
x86_64 Assembly (GAS, .s/.S)	# prove:pf2("name") (line prefix)
x86_64 Assembly (NASM, .asm)	; prove:pf2("name") (line prefix)
ARM64 Assembly	// prove:pf2("name") or /* prove:pf2("name") ... */
WebAssembly	;; prove:pf2("name") (line prefix)

Language Examples

Rust

/// prove:pf2("checked_add_safe")
/// \[
/// \begin{sig} fn checked_add(a: u64, b: u64) -> Option<u64> \end{sig}
/// \begin{pre} a : \mathbb{N} \land b : \mathbb{N} \end{pre}
/// \begin{post} \text{result} = \text{Some}(a + b) \lor \text{result} = \text{None} \end{post}
/// \begin{proof}
/// \step{1}{\text{checked\_add\_safe}
///   = (\lambda\, a\, b.\; a + b)}
///   \pf\ By DEFINE.
/// \step{2}{ a + b = b + a }
///   \pf\ By ADD\_SYM.
/// \qedstep
/// \begin{proof} \pf\ By \stepref{1} and \stepref{2}. \end{proof}
/// \end{proof}
/// \]
fn checked_add(a: u64, b: u64) -> Option<u64> {
    a.checked_add(b)
}

TypeScript / JavaScript

/** prove:pf2("array_sum_non_negative")
\[
\begin{sig} function sumArray(xs: number[]): number \end{sig}
\begin{pre}
  \forall\, i.\; 0 \leq i < \text{len}(xs)
    \Rightarrow xs[i] \geq 0
\end{pre}
\begin{post} \text{result} \geq 0 \end{post}
\begin{proof}
\step{1}{ \text{sum}([]) = 0 }
  \pf\ By definition of sum over empty list.
\step{2}{ \forall\, x \geq 0,\; s \geq 0.\;
  x + s \geq 0 }
  \pf\ By LE\_ADD.
\step{3}{ \text{sum}(xs) \geq 0 }
  \pf\ By induction on \text{len}(xs),
  \stepref{1}, and \stepref{2}.
\qedstep
  \begin{proof} \pf\ By \stepref{3}. \end{proof}
\end{proof}
\]
*/
function sumArray(xs: number[]): number {
  return xs.reduce((acc, x) => acc + x, 0);
}

Python

Python has no block comments, so annotations use consecutive # line comments directly above the function. (Docstrings are string literals, not comments, and are not scanned for annotations.)

# prove:pf2("binary_search_correct")
# \[
# \begin{pre}
#   \text{sorted}(arr) \land \text{len}(arr) > 0
# \end{pre}
# \begin{post}
#   \text{result} \neq \text{None}
#     \Rightarrow arr[\text{result}] = target
# \end{post}
# \begin{proof}
# \step{1}{ \text{lo} \leq \text{hi}
#   \Rightarrow \text{mid} \in [\text{lo}, \text{hi}] }
#   \pf\ By definition of integer division.
# \step{2}{ arr[\text{mid}] = target
#   \Rightarrow \text{result} = \text{mid} }
#   \pf\ By direct comparison.
# \step{3}{ \text{hi} - \text{lo}
#   \text{ decreases on each iteration} }
#   \pf\ By case split on arr[\text{mid}] vs target.
# \qedstep
#   \begin{proof} \pf\ By \stepref{1}, \stepref{2}, and \stepref{3}. \end{proof}
# \end{proof}
# \]
def binary_search(arr: list[int], target: int) -> int | None:
    lo, hi = 0, len(arr) - 1
    while lo <= hi:
        mid = (lo + hi) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            lo = mid + 1
        else:
            hi = mid - 1
    return None

Go

/* prove:pf2("clamp_in_range")
\[
\begin{pre}
  \text{lo} \leq \text{hi}
\end{pre}
\begin{post}
  \text{lo} \leq \text{result} \leq \text{hi}
\end{post}
\begin{proof}
\step{1}{ x < \text{lo}
  \Rightarrow \text{result} = \text{lo} }
  \pf\ By first branch.
\step{2}{ x > \text{hi}
  \Rightarrow \text{result} = \text{hi} }
  \pf\ By second branch.
\step{3}{ \text{lo} \leq x \leq \text{hi}
  \Rightarrow \text{result} = x }
  \pf\ By default branch.
\qedstep
  \begin{proof} \pf\ By \stepref{1}, \stepref{2}, and \stepref{3},
  \text{result} \in [\text{lo}, \text{hi}]. \end{proof}
\end{proof}
\]
*/
func Clamp(x, lo, hi int) int {
    if x < lo {
        return lo
    }
    if x > hi {
        return hi
    }
    return x
}

Java

/** prove:pf2("abs_non_negative")
\[
\begin{pre} x \neq \text{Integer.MIN\_VALUE} \end{pre}
\begin{post} \text{result} \geq 0 \end{post}
\begin{proof}
\step{1}{ x \geq 0 \Rightarrow \text{result} = x \geq 0 }
  \pf\ By first branch.
\step{2}{ x < 0 \Rightarrow \text{result} = -x > 0 }
  \pf\ By second branch and precondition.
\qedstep
  \begin{proof} \pf\ By \stepref{1} and \stepref{2}. \end{proof}
\end{proof}
\]
*/
public static int abs(int x) {
    return x >= 0 ? x : -x;
}

C#

/* prove:pf2("max_returns_larger")
\[
\begin{proof}
\step{1}{ a \geq b \Rightarrow \text{result} = a }
  \pf\ By ternary true branch.
\step{2}{ a < b \Rightarrow \text{result} = b }
  \pf\ By ternary false branch.
\qedstep
  \begin{proof} \pf\ By \stepref{1} and \stepref{2}. \end{proof}
\end{proof}
\]
*/
public static int Max(int a, int b) => a >= b ? a : b;

C++

/* prove:pf2("swap_values")
\[
\begin{post} a' = b \land b' = a \end{post}
\begin{proof}
\step{1}{ \text{temp} = a }
  \pf\ By assignment.
\step{2}{ a' = b }
  \pf\ By second assignment.
\step{3}{ b' = \text{temp} = a }
  \pf\ By \stepref{1} and third assignment.
\qedstep
  \begin{proof} \pf\ By \stepref{2} and \stepref{3}. \end{proof}
\end{proof}
\]
*/
void swap(int& a, int& b) {
    int temp = a;
    a = b;
    b = temp;
}

Swift

/* prove:pf2("is_even_correct")
\[
\begin{proof}
\step{1}{ n \mod 2 = 0 \Rightarrow \text{result} = \text{true} }
  \pf\ By definition of even.
\step{2}{ n \mod 2 \neq 0 \Rightarrow \text{result} = \text{false} }
  \pf\ By negation.
\qedstep
  \begin{proof} \pf\ By \stepref{1} and \stepref{2}. \end{proof}
\end{proof}
\]
*/
func isEven(_ n: Int) -> Bool {
    return n % 2 == 0
}

Kotlin

/** prove:pf2("safe_divide")
\[
\begin{pre} b \neq 0 \end{pre}
\begin{proof}
\step{1}{ b \neq 0 \Rightarrow a / b \text{ is defined} }
  \pf\ By precondition.
\qedstep
  \begin{proof} \pf\ By \stepref{1}. \end{proof}
\end{proof}
\]
*/
fun divide(a: Int, b: Int): Int = a / b

Haskell

{- prove:pf2("reverse_involutive")
\[
\begin{proof}
\step{1}{ \text{reverse}(\text{reverse}([])) = [] }
  \pf\ By base case.
\step{2}{ \text{reverse}(\text{reverse}(x:xs))
  = x : \text{reverse}(\text{reverse}(xs)) }
  \pf\ By inductive step and reverse definition.
\qedstep
  \begin{proof} \pf\ By induction, \stepref{1} and \stepref{2}. \end{proof}
\end{proof}
\]
-}
myReverse :: [a] -> [a]
myReverse [] = []
myReverse (x:xs) = myReverse xs ++ [x]

Lua

-- prove:pf2("table_count_positive")
-- \[
-- \begin{proof}
-- \step{1}{ \text{count}(\{}) = 0 }
--   \pf\ By empty table.
-- \qedstep
-- \begin{proof} \pf\ By \stepref{1}. \end{proof}
-- \end{proof}
-- \]
function count(t)
  local n = 0
  for _ in pairs(t) do n = n + 1 end
  return n
end

SQL

-- prove:pf2("tenant_isolation")
-- \[
-- \begin{pre} \text{tenant\_id} \neq \text{NULL} \end{pre}
-- \begin{post}
--   \forall\, r \in \text{result}.\;
--     r.\text{tenant\_id} = \text{p\_tenant\_id}
-- \end{post}
-- \begin{proof}
-- \step{1}{ \text{WHERE tenant\_id = p\_tenant\_id}
--   \text{ filters all rows} }
--   \pf\ By SQL WHERE semantics.
-- \qedstep
-- \begin{proof} \pf\ By \stepref{1}. \end{proof}
-- \end{proof}
-- \]
CREATE FUNCTION get_orders(p_tenant_id UUID)
RETURNS SETOF orders AS $$
  SELECT * FROM orders WHERE tenant_id = p_tenant_id;
$$ LANGUAGE sql;

Pre/Post Contracts

Preconditions and postconditions define a function’s formal contract. The kernel verifies that the proof is consistent with both the contract and the parser’s translation of the code.

/* prove:pf2("divide_safe")
\[
\begin{pre}
  \forall\, a : \text{Int}, b : \text{Int}.\; b \neq 0
\end{pre}
\begin{post}
  \text{divide}(a, b) \cdot b + (a \mod b) = a
\end{post}
\begin{proof}
\step{1}{ \text{divide}(a, b) \cdot b + (a \mod b) = a }
  \pf\ By definition of integer division (Euclidean property).
\qedstep
  \begin{proof} \pf\ By \stepref{1}. \end{proof}
\end{proof}
\]
*/

The \begin{pre} block declares what must hold before the function executes. The \begin{post} block declares what the function guarantees when it returns. The proof must show that the postcondition follows from the precondition and the code’s behavior.

Documenting External Dependencies

When a proof reasons about external code that Backbuild Prove cannot translate directly (for example a third-party library, native FFI, or system call), document the dependency in the human-readable \begin{doc} section and cite it in your proof steps. This keeps the assumption explicit and auditable while the kernel verifies the steps that build on it.

/* prove:pf2("encrypt_data")
\[
\begin{doc}
  Assumes OpenSSL AES-256-GCM provides IND-CPA security.
\end{doc}
\begin{proof}
\step{1}{ \text{AES-256-GCM} \text{ provides authenticated encryption} }
  \pf\ By the documented OpenSSL AES-256-GCM assumption.
\step{2}{ \text{result} \text{ is ciphertext} }
  \pf\ By \stepref{1} and function implementation.
\qedstep
  \begin{proof} \pf\ By \stepref{2}. \end{proof}
\end{proof}
\]
*/

Content Hash Caching

Backbuild Prove computes a content hash for each annotation. When you re-run verification, annotations whose content has not changed since their last successful verification are returned immediately with a Cached status. Only modified or new annotations are sent to the HOL kernel for re-verification.

This means that large projects with hundreds of annotations can re-verify in seconds when only a few files have changed. Any change to the annotation content, including whitespace changes inside the proof, invalidates the cache and triggers re-verification.

When the Parser Cannot Translate Code

Some code constructs cannot be translated into the kernel’s term language. Common cases include:

• Inline assembly
• FFI (Foreign Function Interface) calls
• Macros and code generation
• Reflective or metaprogramming code
• Dynamic dispatch through runtime type information

For functions that contain untranslatable constructs, document the untranslatable portion as an explicit assumption in the \begin{doc} section and reason about it in your proof steps. This preserves soundness while making the dependency explicit and auditable.

AI Agents and pf2

AI coding agents do not need special training to write pf2 annotations. The Backbuild system teaches agents through three mechanisms:

• Examples: the system provides annotated code samples that agents can follow.
• Documentation: agents receive references to the pf2 syntax guide and the available theorem library.
• Instructive error messages: when verification fails, the error message explains exactly what went wrong and what the kernel expected. The agent reads the error, understands the issue, and self-corrects.

This teach-by-feedback approach means any AI coding agent can learn to write correct pf2 annotations through normal tool use.

Next Steps

• Pre/Post Contracts: detailed guide to precondition and postcondition verification
• Supported Languages: full list of languages with file extensions and tier limits
• Governance Proofs: project-wide properties verified across every call site
• CLI and CI: commands for running verification