From d79b4422b05654defb016fe0e43adf869238452a Mon Sep 17 00:00:00 2001
From: Jacco <4022046+basetunnel@users.noreply.github.com>
Date: Wed, 17 Jun 2026 11:47:19 +0200
Subject: [PATCH] Certifier: link to html agda docs from index.html
 (plutus-metatheory docs)

---
 plutus-metatheory/src/index.lagda.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/plutus-metatheory/src/index.lagda.md b/plutus-metatheory/src/index.lagda.md
index 936716b6436..e8ae637660a 100644
--- a/plutus-metatheory/src/index.lagda.md
+++ b/plutus-metatheory/src/index.lagda.md
@@ -32,6 +32,13 @@ untyped version of PLC which can also be executed directly.
 The final two pieces are a type checker which is guaranteed to be
 sound and an executable that is intended to be compiled into Haskell.
 
+A separate family of modules specify UPLC compiler optimizations as syntactic
+binary relations. The relations are (semi-)decidable, so for a given pair of
+input/output terms, we can produce a proof when the pass behaved according to
+specification. This is the basis of the `--certify` flag available in the Plinth
+compiler and UPLC CLI tool. The Plinth user guide contains more detail on how to
+use the certifier.
+
 1. [Types](#types)
 2. [Normalisation of types](#normal-types)
 3. [Builtin machinery](#builtins)
@@ -41,6 +48,7 @@ sound and an executable that is intended to be compiled into Haskell.
 7. [Untyped terms](#untyped-terms)
 8. [A typechecker](#type-checker)
 9. [An executable](#executable)
+10. [Certified compilation](#certified-compilation)
 
 ## Types
 
@@ -200,3 +208,13 @@ to produce an executable.
 import Main
 ```
 
+
+## Certified Compilation
+
+The top-level module that defines the `certify` function, imports all
+translation relations and their (semi-)decision procedures.
+
+```
+import VerifiedCompilation
+```
+