diff --git a/docs-site/app/layout.tsx b/docs-site/app/layout.tsx
index 32a7e4ec8..708e71fc7 100644
--- a/docs-site/app/layout.tsx
+++ b/docs-site/app/layout.tsx
@@ -2,6 +2,7 @@ import { Layout, Navbar } from 'nextra-theme-docs'
 import { Head } from 'nextra/components'
 import { getPageMap } from 'nextra/page-map'
 import 'nextra-theme-docs/style.css'
+import './verity-code.css'
 
 export const metadata = {
   title: {
diff --git a/docs-site/app/verity-code.css b/docs-site/app/verity-code.css
new file mode 100644
index 000000000..8dafde66a
--- /dev/null
+++ b/docs-site/app/verity-code.css
@@ -0,0 +1,41 @@
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] {
+  background:
+    linear-gradient(90deg, rgba(123, 63, 50, 0.06), transparent 22rem),
+    #fffaf1 !important;
+  border: 1px solid #eadcca;
+  box-shadow: 0 1px 0 rgba(255, 255, 255, 0.72) inset;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code {
+  line-height: 1.62;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span {
+  position: relative;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span::before {
+  content: "";
+  position: absolute;
+  inset-block: 0;
+  left: 1.35rem;
+  border-left: 1px solid rgba(139, 118, 99, 0.13);
+  pointer-events: none;
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#7b3f32" i]:first-child),
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#875c24" i]) {
+  background: linear-gradient(90deg, rgba(234, 220, 202, 0.7), rgba(234, 220, 202, 0));
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#a34537" i]) {
+  background: linear-gradient(90deg, rgba(163, 69, 55, 0.08), rgba(163, 69, 55, 0));
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#285f91" i]) {
+  background: linear-gradient(90deg, rgba(40, 95, 145, 0.07), rgba(40, 95, 145, 0));
+}
+
+figure[data-rehype-pretty-code-figure] pre[data-language="verity"] code > span:has(> span[style*="#3f7456" i]) {
+  background: linear-gradient(90deg, rgba(63, 116, 86, 0.08), rgba(63, 116, 86, 0));
+}
diff --git a/docs-site/content/compiler.mdx b/docs-site/content/compiler.mdx
index 4efa69898..ffcff85f3 100644
--- a/docs-site/content/compiler.mdx
+++ b/docs-site/content/compiler.mdx
@@ -55,7 +55,7 @@ Roadmap, milestones, and progress updates live in `docs-site/content/research.md
 ## Example: SimpleStorage
 
 ### EDSL Implementation
-```lean
+```verity
 -- Verity/Examples/SimpleStorage.lean
 def storedData : StorageSlot Uint256 := ⟨0⟩
 
@@ -67,7 +67,7 @@ def retrieve : Contract Uint256 := do
 ```
 
 ### Declarative Specification
-```lean
+```verity
 -- Compiler/Specs.lean
 def simpleStorageSpec : CompilationModel := {
   name := "SimpleStorage"
@@ -217,7 +217,7 @@ forge create SimpleStorage --from 0x... --private-key ...
 ## Features
 
 ### Automatic Storage Slot Inference ✅
-```lean
+```verity
 fields := [
   { name := "owner", ty := FieldType.address },     -- slot 0
   { name := "balances", ty := FieldType.mappingTyped (.simple .address) },  -- slot 1
@@ -228,7 +228,7 @@ fields := [
 No manual slot management needed. Compiler assigns slots based on field order.
 
 ### Constructor Parameters ✅
-```lean
+```verity
 constructor := some {
   params := [{ name := "initialOwner", ty := ParamType.address }]
   body := [
@@ -363,7 +363,7 @@ Members can carry packed bit metadata, so common `uint128`-style packed subfield
 | `internalCall "f" args` | Call internal function (statement) | `internal_f(args...)` |
 
 **Example**, combining multiple features:
-```lean
+```verity
 -- Balance check with require
 Stmt.require (Expr.ge (Expr.mapping "balances" Expr.caller) (Expr.param "amount")) "Insufficient",
 Stmt.setMapping "balances" Expr.caller
@@ -371,14 +371,14 @@ Stmt.setMapping "balances" Expr.caller
 Stmt.stop
 ```
 
-```lean
+```verity
 -- If/else branching
 Stmt.ite (Expr.eq Expr.caller (Expr.storage "owner"))
   [Stmt.setStorage "paused" (Expr.literal 1), Stmt.stop]
   [Stmt.stop]  -- non-owner: no-op
 ```
 
-```lean
+```verity
 -- Bounded loop over array
 Stmt.forEach "i" (Expr.arrayLength "recipients")
   [Stmt.setMapping "balances" (Expr.arrayElement "recipients" (Expr.localVar "i"))
@@ -441,7 +441,7 @@ lake exe verity-compiler-patched --backend-profile solidity-parity
 
 Conditional logic for contract functions:
 
-```lean
+```verity
 -- Simple if (no else)
 Stmt.ite (Expr.eq Expr.caller (Expr.storage "owner"))
   [Stmt.setStorage "paused" (Expr.literal 1)]
@@ -468,7 +468,7 @@ Compiles to a block-scoped condition variable to avoid re-evaluation after state
 
 Iterate over array parameters or fixed counts:
 
-```lean
+```verity
 -- Iterate over a dynamic array
 Stmt.forEach "i" (Expr.arrayLength "recipients")
   [Stmt.setMapping "balances"
@@ -500,7 +500,7 @@ let (lhs, rhs) ← helperPair arg
 
 Those source forms lower to `Stmt.internalCall`, `Stmt.internalCallAssign`, or `Expr.internalCall` in the compilation model.
 
-```lean
+```verity
 def mySpec : CompilationModel := {
   name := "MyContract"
   fields := [{ name := "balances", ty := FieldType.mappingTyped (.simple .address) }]
@@ -531,7 +531,7 @@ def mySpec : CompilationModel := {
 ```
 
 Internal functions that return values use `__ret` assignment instead of EVM `RETURN`:
-```lean
+```verity
 -- Internal function returning a value
 { name := "getBalance"
   params := [{ name := "addr", ty := ParamType.address }]
@@ -548,7 +548,7 @@ Stmt.letVar "bal" (Expr.internalCall "getBalance" [Expr.caller])
 
 Emit EVM events for standards compliance (ERC20 Transfer/Approval, etc.):
 
-```lean
+```verity
 def tokenSpec : CompilationModel := {
   name := "Token"
   fields := [{ name := "balances", ty := FieldType.mappingTyped (.simple .address) }]
@@ -582,7 +582,7 @@ Event topic0 is computed from the event signature (e.g., `keccak256("Transfer(ad
 
 For ERC20 allowances and similar patterns requiring `mapping(address => mapping(address => uint256))`:
 
-```lean
+```verity
 fields := [
   { name := "allowances", ty := FieldType.mappingTyped (MappingType.nested .address .address) }
 ]
@@ -600,7 +600,7 @@ Storage layout: `keccak256(spender . keccak256(owner . slot))`; matches Solidity
 
 For mappings keyed by numeric values instead of addresses:
 
-```lean
+```verity
 fields := [
   { name := "data", ty := FieldType.mappingTyped (MappingType.simple .uint256) }
 ]
@@ -616,7 +616,7 @@ Stmt.setMappingUint "data" (Expr.param "tokenId") (Expr.param "value")
 
 Dynamic arrays, fixed arrays, and bytes parameters for batch operations:
 
-```lean
+```verity
 -- Dynamic array parameter
 { name := "recipients", ty := ParamType.array ParamType.address }
 
@@ -660,7 +660,7 @@ FOUNDRY_PROFILE=difftest forge test
 ### Add New Contract
 
 1. **Add a macro contract declaration** in `Contracts/<Name>/<Name>.lean`:
-```lean
+```verity
 verity_contract MyContract where
   storage
     value : Uint256 := slot 0
@@ -765,7 +765,7 @@ private def ownedContract : IRContract :=
 ```
 
 **After** (declarative spec):
-```lean
+```verity
 def ownedSpec : CompilationModel := {
   name := "Owned"
   fields := [
diff --git a/docs-site/content/core.mdx b/docs-site/content/core.mdx
index a77753484..96b5979e6 100644
--- a/docs-site/content/core.mdx
+++ b/docs-site/content/core.mdx
@@ -9,7 +9,7 @@ The core is intentionally small. It provides types for contract state, storage o
 
 ## Types
 
-```lean
+```verity
 abbrev Address := String
 abbrev Uint256 := Verity.Core.Uint256
 
@@ -25,7 +25,7 @@ structure StorageSlot (α : Type) where
 
 ## ContractState
 
-```lean
+```verity
 structure ContractState where
   storage : Nat → Uint256                         -- Uint256 storage
   storageAddr : Nat → Address                      -- Address storage
@@ -64,7 +64,7 @@ abbrev Contract (α : Type) := ContractState → ContractResult α
 
 A contract is a function from state to result. The custom `bind` short-circuits on revert:
 
-```lean
+```verity
 def bind (ma : Contract α) (f : α → Contract β) : Contract β :=
   fun s => match ma s with
   | ContractResult.success a s' => f a s'
@@ -87,7 +87,7 @@ Five pairs of get/set functions, one per storage type:
 
 All follow the same pattern — read from or write to the corresponding `ContractState` field:
 
-```lean
+```verity
 def getStorage (s : StorageSlot Uint256) : Contract Uint256 :=
   fun state => ContractResult.success (state.storage s.slot) state
 
@@ -99,7 +99,7 @@ def setStorage (s : StorageSlot Uint256) (value : Uint256) : Contract Unit :=
 
 Mapping operations take key arguments:
 
-```lean
+```verity
 -- Address-keyed mapping (e.g., balances[owner])
 let bal ← getMapping balances owner
 setMapping balances owner newBal
@@ -119,7 +119,7 @@ setMapping2 allowances owner spender newAllow
 
 Read-only functions for accessing transaction context:
 
-```lean
+```verity
 let sender ← msgSender           -- Transaction sender address
 let self ← contractAddress        -- This contract's address
 let value ← msgValue             -- ETH value sent with call
@@ -130,7 +130,7 @@ These return values from `ContractState` without modifying state.
 
 ## Event emission
 
-```lean
+```verity
 emitEvent "Transfer" [amount] [senderBal, recipientBal]
 ```
 
@@ -138,7 +138,7 @@ emitEvent "Transfer" [amount] [senderBal, recipientBal]
 
 ## Require guard
 
-```lean
+```verity
 def require (condition : Bool) (message : String) : Contract Unit :=
   fun s => if condition
            then ContractResult.success () s
@@ -151,7 +151,7 @@ Returns `success` when the condition holds, `revert` with the message when it do
 
 Every storage operation, context accessor, and event function has a full-result `@[simp]` lemma:
 
-```lean
+```verity
 -- Full-result form (preferred for new proofs):
 @[simp] theorem getStorage_run (s : StorageSlot Uint256) (state : ContractState) :
   (getStorage s).run state = ContractResult.success (state.storage s.slot) state := rfl
@@ -173,7 +173,7 @@ A plain `StateM ContractState α` monad cannot model `require` failures — proo
 
 The `StorageSlot α` type parameter prevents mixing storage types:
 
-```lean
+```verity
 def owner : StorageSlot Address := ⟨0⟩
 def count : StorageSlot Uint256 := ⟨1⟩
 def balances : StorageSlot (Address → Uint256) := ⟨2⟩
diff --git a/docs-site/content/edsl-api-reference.mdx b/docs-site/content/edsl-api-reference.mdx
index a9783ee7f..27df1d87c 100644
--- a/docs-site/content/edsl-api-reference.mdx
+++ b/docs-site/content/edsl-api-reference.mdx
@@ -20,7 +20,7 @@ open Verity.Stdlib.Math
 
 Use `local_obligations [...]` on constructors or functions when a small unsafe or refinement-shaped boundary must stay explicit in the generated trust report. Direct assembly-shaped primitives such as raw low-level calls, returndata forwarding, and manual memory/calldata operations are expected to carry at least one local obligation at that exact usage site.
 
-```lean
+```verity
 function unsafeEdge ()
   local_obligations [manual_delegatecall_refinement := assumed "Caller must separately prove the handwritten assembly path."]
   : Unit := do
@@ -35,7 +35,7 @@ Each entry lowers into `spec.constructor.localObligations` or `FunctionSpec.loca
 
 **Signature**
 
-```lean
+```verity
 def getStorage (s : StorageSlot Uint256) : Contract Uint256
 def setStorage (s : StorageSlot Uint256) (value : Uint256) : Contract Unit
 ```
@@ -46,7 +46,7 @@ Read/write a `Uint256` storage slot.
 
 **Example**
 
-```lean
+```verity
 let x <- getStorage counterSlot
 setStorage counterSlot (x + 1)
 ```
@@ -60,7 +60,7 @@ setStorage counterSlot (x + 1)
 
 **Signature**
 
-```lean
+```verity
 def getStorageAddr (s : StorageSlot Address) : Contract Address
 def setStorageAddr (s : StorageSlot Address) (value : Address) : Contract Unit
 ```
@@ -71,7 +71,7 @@ Read/write an `Address` storage slot.
 
 **Example**
 
-```lean
+```verity
 let owner <- getStorageAddr ownerSlot
 setStorageAddr ownerSlot newOwner
 ```
@@ -85,7 +85,7 @@ setStorageAddr ownerSlot newOwner
 
 **Signature**
 
-```lean
+```verity
 def getMapping (s : StorageSlot (Address -> Uint256)) (key : Address) : Contract Uint256
 def setMapping (s : StorageSlot (Address -> Uint256)) (key : Address) (value : Uint256) : Contract Unit
 ```
@@ -96,7 +96,7 @@ Read/write address-keyed mappings.
 
 **Example**
 
-```lean
+```verity
 let bal <- getMapping balances msgSenderAddr
 setMapping balances msgSenderAddr (bal - amount)
 ```
@@ -110,7 +110,7 @@ setMapping balances msgSenderAddr (bal - amount)
 
 **Signature**
 
-```lean
+```verity
 def getMappingUint (s : StorageSlot (Uint256 -> Uint256)) (key : Uint256) : Contract Uint256
 def setMappingUint (s : StorageSlot (Uint256 -> Uint256)) (key : Uint256) (value : Uint256) : Contract Unit
 ```
@@ -121,7 +121,7 @@ Read/write uint256-keyed mappings.
 
 **Example**
 
-```lean
+```verity
 let price <- getMappingUint oraclePrices tokenId
 setMappingUint oraclePrices tokenId newPrice
 ```
@@ -135,7 +135,7 @@ setMappingUint oraclePrices tokenId newPrice
 
 **Signature**
 
-```lean
+```verity
 def getMapping2 (s : StorageSlot (Address -> Address -> Uint256)) (key1 key2 : Address) : Contract Uint256
 def setMapping2 (s : StorageSlot (Address -> Address -> Uint256)) (key1 key2 : Address) (value : Uint256) : Contract Unit
 ```
@@ -146,7 +146,7 @@ Read/write double mappings (for example, allowances).
 
 **Example**
 
-```lean
+```verity
 let allow <- getMapping2 allowances owner spender
 setMapping2 allowances owner spender (allow - amount)
 ```
@@ -162,7 +162,7 @@ setMapping2 allowances owner spender (allow - amount)
 
 **Signature**
 
-```lean
+```verity
 def require (condition : Bool) (message : String) : Contract Unit
 ```
 
@@ -203,7 +203,7 @@ Monadic sequencing with short-circuit on revert.
 
 **Example**
 
-```lean
+```verity
 let x <- getStorage counterSlot
 setStorage counterSlot (x + 1)
 ```
@@ -241,7 +241,7 @@ Reference points:
 
 **Signature**
 
-```lean
+```verity
 def emitEvent (name : String) (args : List Uint256) (indexedArgs : List Uint256 := []) : Contract Unit
 ```
 
@@ -251,7 +251,7 @@ Append an event entry to the execution state's event log.
 
 **Example**
 
-```lean
+```verity
 emitEvent "Transfer" [amount] [fromAddr, toAddr]
 ```
 
@@ -292,7 +292,7 @@ let scale : Uint256 := pow 10 decimals
 
 **Signatures**
 
-```lean
+```verity
 def safeAdd (a b : Uint256) : Option Uint256
 def safeSub (a b : Uint256) : Option Uint256
 def safeMul (a b : Uint256) : Option Uint256
@@ -303,7 +303,7 @@ def requireSomeUint (opt : Option Uint256) (message : String) : Contract Uint256
 
 **Example**
 
-```lean
+```verity
 let sum <- requireSomeUint (safeAdd a b) "overflow"
 let product <- requireSomeUint (safeMul a b) "overflow"
 let quotient <- requireSomeUint (safeDiv a b) "division by zero"
@@ -374,7 +374,7 @@ only when the divisor is zero or the final floor/ceil quotient does not fit in
 
 Inside `verity_contract`, call reusable same-contract helpers with ordinary function-call syntax. Do not write `internalCall` or `internalCallAssign` in source contracts; those names are compilation-model IR constructors used after macro lowering.
 
-```lean
+```verity
 verity_contract HelperExample where
   storage
     total : Uint256 := slot 0
@@ -425,7 +425,7 @@ For executable Lean definitions generated by `verity_contract`, tuple-typed para
 
 `verity_contract` now accepts an empty `storage` block when a contract is purely functional or only depends on ambient values such as `msg.sender`:
 
-```lean
+```verity
 verity_contract Stateless where
   storage
 
@@ -441,7 +441,7 @@ This keeps the macro surface usable for helper-style and interface-shaped contra
 
 Constructors can also be marked payable directly in the macro surface:
 
-```lean
+```verity
 verity_contract PayableInit where
   storage
     owner : Address := slot 0
@@ -458,7 +458,7 @@ This sets `spec.constructor.isPayable := true`, emits constructor ABI `stateMuta
 
 Upgradeable-style initialization can also be guarded directly from the macro surface using an explicit version slot:
 
-```lean
+```verity
 verity_contract UpgradeableConfig where
   storage
     initializedVersion : Uint256 := slot 0
@@ -478,7 +478,7 @@ verity_contract UpgradeableConfig where
 
 `verity_contract` also supports contract-scoped compile-time constants that are shared between the executable fallback and the generated compilation model:
 
-```lean
+```verity
 verity_contract FeeConfig where
   storage
 
@@ -505,7 +505,7 @@ Storage fields, constants, and functions also share the generated Lean namespace
 
 `verity_contract` also supports contract-scoped immutables for deployment-time values that should become read-only at runtime:
 
-```lean
+```verity
 verity_contract ImmutableConfig where
   storage
     owner : Address := slot 0
@@ -545,7 +545,7 @@ The current surface supports `Uint256`, `Uint8`, `Address`, `Bytes32`, and `Bool
 
 `verity_contract` can now declare linked external functions directly and use them from `externalCall` expressions:
 
-```lean
+```verity
 verity_contract LinkedOracle where
   storage
     lastQuote : Uint256 := slot 0
@@ -603,7 +603,7 @@ String and bytes values remain intentionally bounded. ABI transport is supported
 
 `verity_contract` now accepts custom error declarations and threads them into the generated `CompilationModel`/ABI surface:
 
-```lean
+```verity
 errors
   error NonPositive(Uint256)
   error AmountTooLarge(Uint256, Uint256)
@@ -706,7 +706,7 @@ If the contract already defines a same-named function with the matching arity, t
 
 `verity_contract` also accepts a low-level `tryCatch` do-element for call-style expressions that return a success word:
 
-```lean
+```verity
 tryCatch (call gas target value inOffset inSize outOffset outSize) (do
   setStorage lastFailure 1)
 ```
@@ -738,7 +738,7 @@ This elaborates to `Compiler.CompilationModel.Expr.keccak256` and lowers to the
 For packed preimages where each item is already a full 32-byte word, use the
 standard hashing ECMs instead of open-coded offset arithmetic:
 
-```lean
+```verity
 Compiler.Modules.Hashing.abiEncodePackedWords
   "digest"
   [Expr.param "root", Expr.param "contextHash", Expr.param "nullifier"]
@@ -756,7 +756,7 @@ reverts on precompile failure, and binds the digest word.
 
 For static mixed-width preimages, use explicit byte-width segment helpers:
 
-```lean
+```verity
 Compiler.Modules.Hashing.abiEncodePackedStaticSegments
   "digest"
   [(Expr.param "who", 20), (Expr.param "amount", 32)]
@@ -840,7 +840,7 @@ First-class linear-memory forms (`Expr.mload`, `Stmt.mstore`, `Stmt.calldatacopy
 
 **Signatures**
 
-```lean
+```verity
 def msgSender : Contract Address
 def contractAddress : Contract Address
 def msgValue : Contract Uint256
@@ -851,7 +851,7 @@ def blobbasefee : Contract Uint256
 
 **Example**
 
-```lean
+```verity
 let from <- msgSender
 let value <- msgValue
 ```
diff --git a/docs-site/content/examples.mdx b/docs-site/content/examples.mdx
index bc9ea8f2e..826109f8d 100644
--- a/docs-site/content/examples.mdx
+++ b/docs-site/content/examples.mdx
@@ -34,7 +34,7 @@ Example (SimpleStorage):
 
 Single storage slot with get/set.
 
-```lean
+```verity
 def storedData : StorageSlot Uint256 := ⟨0⟩
 
 def store (value : Uint256) : Contract Unit := do
@@ -50,7 +50,7 @@ Proofs cover store/retrieve roundtrip and state isolation.
 
 Read-modify-write with increment and decrement.
 
-```lean
+```verity
 def count : StorageSlot Uint256 := ⟨0⟩
 
 def increment : Contract Unit := do
@@ -68,7 +68,7 @@ Proofs cover arithmetic, composition (two increments add 2), and decrement-at-ze
 
 Same as Counter but uses checked arithmetic from `Stdlib/Math`.
 
-```lean
+```verity
 def increment : Contract Unit := do
   let current ← getStorage count
   let newCount ← requireSomeUint (safeAdd current 1) "Overflow"
@@ -81,7 +81,7 @@ Proofs cover overflow/underflow revert and bounds preservation.
 
 Access control with an owner address and a `require` guard.
 
-```lean
+```verity
 def owner : StorageSlot Address := ⟨0⟩
 
 def isOwner : Contract Bool := do
@@ -100,7 +100,7 @@ Proofs cover access control enforcement and ownership transfer.
 
 Composes Owned and Counter. Increment/decrement require ownership.
 
-```lean
+```verity
 def owner : StorageSlot Address := ⟨0⟩
 def count : StorageSlot Uint256 := ⟨1⟩
 
@@ -116,7 +116,7 @@ Proofs cover cross-pattern composition, ownership transfer locking out old owner
 
 Mapping storage for per-address balances with deposit, withdraw, and transfer.
 
-```lean
+```verity
 def balances : StorageSlot (Address → Uint256) := ⟨0⟩
 
 def deposit (amount : Uint256) : Contract Unit := do
@@ -143,7 +143,7 @@ Proofs cover balance guards, deposit/withdraw/transfer sum equations, and deposi
 
 Composes Owned and Ledger. Adds owner-controlled minting and supply tracking.
 
-```lean
+```verity
 def owner : StorageSlot Address := ⟨0⟩
 def balances : StorageSlot (Address → Uint256) := ⟨1⟩
 def totalSupply : StorageSlot Uint256 := ⟨2⟩
@@ -202,7 +202,7 @@ Proofs cover: existential attack witness (vulnerability is provably exploitable)
 
 Unverified example demonstrating external library linking via the [Linker](/compiler#linker). Has no specs or proofs; it exists to show how external Yul helper functions integrate with compiled output. See the [Linking Libraries](/guides/linking-libraries) guide for a walkthrough.
 
-```lean
+```verity
 -- Placeholder hash for proofs (replaced with real Poseidon at compile time)
 def hashTwo (a b : Uint256) : Contract Uint256 := do
   return add a b
diff --git a/docs-site/content/getting-started.mdx b/docs-site/content/getting-started.mdx
index 62e0db712..1a358b283 100644
--- a/docs-site/content/getting-started.mdx
+++ b/docs-site/content/getting-started.mdx
@@ -68,7 +68,7 @@ Before reading files, keep this map:
 3. `Compiler/Specs.lean`: `CompilationModel` compiler models that generate IR/Yul.
 
 **1. Open an example contract** — [`Verity/Examples/SimpleStorage.lean`](https://github.com/Th0rgal/verity/blob/main/Verity/Examples/SimpleStorage.lean):
-```lean
+```verity
 -- A contract with a single uint256 storage slot
 def store (value : Uint256) : Contract Unit := setStorage storedData value
 def retrieve : Contract Uint256 := getStorage storedData
diff --git a/docs-site/content/guides/_meta.js b/docs-site/content/guides/_meta.js
index 42cd0cb39..9ef2dbdd3 100644
--- a/docs-site/content/guides/_meta.js
+++ b/docs-site/content/guides/_meta.js
@@ -1,6 +1,7 @@
 export default {
   'first-contract': 'Adding Your First Contract',
   'solidity-to-verity': 'Solidity to Verity Translation',
+  'verity-syntax-highlighting': 'Verity Syntax Highlighting',
   'linking-libraries': 'Linking External Libraries',
   'debugging-proofs': 'Proof Debugging Handbook',
 };
diff --git a/docs-site/content/guides/debugging-proofs.mdx b/docs-site/content/guides/debugging-proofs.mdx
index 4c3ac7070..a96905bed 100644
--- a/docs-site/content/guides/debugging-proofs.mdx
+++ b/docs-site/content/guides/debugging-proofs.mdx
@@ -77,7 +77,7 @@ example : expr1 = expr2 := rfl  -- Definitional equality
 **Cause**: Definition not unfolded, or no simp lemmas apply.
 
 **Solution 1**: Unfold before simping
-```lean
+```verity
 -- ❌ DOESN'T WORK
 theorem getValue_correct : ... := by
   simp [getStorage]  -- Error: simp made no progress
@@ -228,7 +228,7 @@ exact my_proof
 ### SafeAdd/SafeSub Failures
 
 **Pattern 1**: Proving safeAdd returns Some
-```lean
+```verity
 -- Goal: safeAdd a b = some c
 theorem safeAdd_proof (h : a.val + b.val ≤ MAX_UINT256) :
     safeAdd a b = some ⟨a.val + b.val, by omega⟩ := by
@@ -249,7 +249,7 @@ theorem increment_no_overflow (h : count.val < MAX_UINT256) :
 ```
 
 **Pattern 3**: Bounded arithmetic
-```lean
+```verity
 -- Prove result stays in bounds
 theorem bounded_add (h1 : a.val ≤ bound) (h2 : b.val ≤ bound) :
     (safeAdd a b).isSome → (safeAdd a b).get!.val ≤ 2 * bound := by
@@ -307,7 +307,7 @@ Avoid `Contract.runState` and `Contract.runValue` in new proofs — use `((op).r
 **Problem**: Prove two storage functions are equal.
 
 **Pattern**: Use `ext` tactic
-```lean
+```verity
 -- Goal: state1.storage = state2.storage
 theorem storage_equal : state1.storage = state2.storage := by
   ext slot  -- For all slots
@@ -319,7 +319,7 @@ theorem storage_equal : state1.storage = state2.storage := by
 ### Storage Unchanged Except
 
 **Pattern**: Common in contract proofs
-```lean
+```verity
 -- Goal: Only slot k changed
 theorem only_slot_k_changed :
     ∀ slot, slot ≠ k → state'.storage slot = state.storage slot := by
@@ -346,7 +346,7 @@ theorem increment_twice_adds_two (s : ContractState) :
 ```
 
 For low-level multi-update proofs, unfold bind directly:
-```lean
+```verity
 theorem two_updates (s : ContractState) :
   let s' := ((do setStorage slot1 val1; setStorage slot2 val2).run s).snd
   s'.storage slot2.slot = val2 := by
@@ -437,7 +437,7 @@ theorem retrieve_meets_spec (s : ContractState) :
 ```
 
 **Alternative when simp can't unfold**:
-```lean
+```verity
 -- ✅ OK: unfold first, then simp
 theorem good_order : getValue state = value := by
   unfold getValue     -- Expose the definition
@@ -591,7 +591,7 @@ theorem retrieve_meets_spec (s : ContractState) :
 
 **Goal**: Prove `increment` updates count and preserves everything else.
 
-```lean
+```verity
 -- The spec is a conjunction: correct value ∧ other slots preserved ∧ context preserved
 theorem increment_meets_spec (s : ContractState) :
   let s' := ((increment).run s).snd
@@ -616,7 +616,7 @@ theorem increment_meets_spec (s : ContractState) :
 
 **Goal**: Prove ownership transfer works when the caller is the current owner.
 
-```lean
+```verity
 theorem transferOwnership_meets_spec_when_owner (s : ContractState) (newOwner : Address)
   (h_is_owner : s.sender = s.storageAddr 0) :
   let s' := ((transferOwnership newOwner).run s).snd
diff --git a/docs-site/content/guides/first-contract.mdx b/docs-site/content/guides/first-contract.mdx
index 940c85c8b..a5a010d28 100644
--- a/docs-site/content/guides/first-contract.mdx
+++ b/docs-site/content/guides/first-contract.mdx
@@ -90,7 +90,7 @@ Specifications describe **what** the contract should do, not **how** it does it.
 
 Open `Contracts/TipJar/Spec.lean`:
 
-```lean
+```verity
 /-
   TipJar: Formal Specification
 
@@ -133,7 +133,7 @@ end Contracts.TipJar.Spec
 
 Open `Contracts/TipJar/Invariants.lean`:
 
-```lean
+```verity
 /-
   TipJar: State Invariants
 
@@ -167,7 +167,7 @@ Now we implement the contract using the EDSL. Every function in the EDSL is a `C
 
 Open `Contracts/TipJar/TipJar.lean`:
 
-```lean
+```verity
 /-
   TipJar: Deposit tips and check balances
 
@@ -252,7 +252,7 @@ This is where formal verification happens. We prove that our implementation matc
 
 Open `Contracts/TipJar/Proofs/Basic.lean`:
 
-```lean
+```verity
 /-
   TipJar: Basic Correctness Proofs
 
@@ -357,7 +357,7 @@ grep -r "sorry" Contracts/TipJar/
 Add your contract in `Contracts/<Name>/<Name>.lean` with `verity_contract`.
 Then register `Contracts.<Name>.spec` in `Compiler/Specs.lean` under `allSpecs`:
 
-```lean
+```verity
 verity_contract TipJar where
   storage
     tips : Address -> Uint256 := slot 0
@@ -650,7 +650,7 @@ open Verity.EVM.Uint256
 **Problem**: Wrong return type.
 
 **Solution**: Check the function signature matches what you return:
-```lean
+```verity
 def tip (amount : Uint256) : Contract Unit := do  -- Returns nothing
   ...
 
@@ -663,7 +663,7 @@ def getBalance (addr : Address) : Contract Uint256 := do  -- Returns Uint256
 **Problem**: `simp` can't solve the goal.
 
 **Solution**: Try `unfold` first to expose definitions, then `simp`:
-```lean
+```verity
 theorem my_thm : ... := by
   unfold myFunction bind
   simp [getMapping, setMapping, msgSender, tips]
diff --git a/docs-site/content/guides/linking-libraries.mdx b/docs-site/content/guides/linking-libraries.mdx
index 223796041..3915d4e33 100644
--- a/docs-site/content/guides/linking-libraries.mdx
+++ b/docs-site/content/guides/linking-libraries.mdx
@@ -17,12 +17,12 @@ echo 'function myHash(a, b) -> result { result := add(xor(a, b), 0x42) }' > exam
 ```
 
 **Step 2** — Use a placeholder in your Lean EDSL (for proofs):
-```lean
+```verity
 def myHash (a b : Uint256) : Contract Uint256 := return add a b
 ```
 
 **Step 3** — Declare the external function and reference it in your CompilationModel:
-```lean
+```verity
 -- In your CompilationModel definition:
 externals := [
   { name := "myHash"
@@ -68,7 +68,7 @@ function myHash(a, b) -> result {
 
 In your EDSL contract, define a placeholder that models the same interface:
 
-```lean
+```verity
 -- Placeholder for proofs: models the hash as addition
 -- At compile time, replaced by the real myHash from MyHash.yul
 def myHash (a b : Uint256) : Contract Uint256 := do
@@ -79,7 +79,7 @@ def myHash (a b : Uint256) : Contract Uint256 := do
 
 In `Compiler/Specs.lean`, first declare the external function in the `externals` field of your CompilationModel, then use `Expr.externalCall` in the function body:
 
-```lean
+```verity
 def myCompilationModel : CompilationModel := {
   name := "MyContract"
   fields := [...]
@@ -136,7 +136,7 @@ This means you forgot to pass `--link examples/external-libs/MyHash.yul`.
 Verity includes a working example in [`Verity/Examples/CryptoHash.lean`](https://github.com/Th0rgal/verity/blob/main/Verity/Examples/CryptoHash.lean) with libraries in [`examples/external-libs/`](https://github.com/Th0rgal/verity/tree/main/examples/external-libs).
 
 **EDSL placeholder** (`Verity/Examples/CryptoHash.lean`):
-```lean
+```verity
 -- Placeholder: just adds the inputs (for proving logic)
 def hashTwo (a b : Uint256) : Contract Uint256 := do
   return add a b
diff --git a/docs-site/content/guides/solidity-to-verity.mdx b/docs-site/content/guides/solidity-to-verity.mdx
index 64700ae64..c188b0002 100644
--- a/docs-site/content/guides/solidity-to-verity.mdx
+++ b/docs-site/content/guides/solidity-to-verity.mdx
@@ -51,7 +51,7 @@ modifier onlyOwner() {
 
 Verity pattern:
 
-```lean
+```verity
 verity_contract OwnedExample where
   storage
     owner : Address := slot 0
@@ -72,7 +72,7 @@ Call helpers directly by name. `internalCall` and `internalCallAssign` are the l
 
 Partial support exists today via low-level `tryCatch` sugar in `verity_contract`:
 
-```lean
+```verity
 tryCatch (call gas target value inOffset inSize outOffset outSize) (do
   setStorage lastFailure 1)
 ```
@@ -123,14 +123,14 @@ function transfer(address to, uint256 amount) external returns (bool) {
 
 ### Step A: Define slots
 
-```lean
+```verity
 def balances : StorageSlot (Address → Uint256) := ⟨0⟩
 def totalSupply : StorageSlot Uint256 := ⟨1⟩
 ```
 
 ### Step B: Translate the function body
 
-```lean
+```verity
 def transfer (to : Address) (amount : Uint256) : Contract Bool := do
   let sender <- msgSender
   let current <- getStorage balances
diff --git a/docs-site/content/guides/verity-syntax-highlighting.mdx b/docs-site/content/guides/verity-syntax-highlighting.mdx
new file mode 100644
index 000000000..e0de5f546
--- /dev/null
+++ b/docs-site/content/guides/verity-syntax-highlighting.mdx
@@ -0,0 +1,48 @@
+# Verity Syntax Highlighting
+
+The docs site uses a Verity-specific TextMate grammar and the LFGLabs Cream theme for `verity` code fences.
+
+## Definition of Done
+
+- Verity snippets are rendered with `verity`, not generic `lean`, when they show contract DSL code.
+- Contract structure is visually explicit: `verity_contract`, section headers, `linked_externals`, typed `external` declarations, `modifier`, and `function` headers each receive distinct scopes.
+- Solidity-like control surfaces are easy to scan: `with onlyRelayer`, `nonreentrant(...)`, `forEach`, `requireError`, `tryExternalCall`, `abiEncode`, and `emit` are all highlighted by semantic role.
+- Domain-level signals stand out without changing source text: field access such as `txn.proof`, typed external returns such as `Circuit`, event names, and custom errors such as `PoolCircuitNotRegistered()` receive dedicated scopes.
+- Code blocks use a warm light theme with subtle scope bands for guards, external calls, events, and declaration lines.
+- The scope contract is checked by `npm run check:highlighting`.
+
+## Unlink-Style Example
+
+```verity
+linked_externals
+  external getCircuit(Address, Uint256) -> (Circuit)
+  external getCircuit_try(Address, Uint256) -> (Bool, Circuit)
+
+modifier onlyRelayer := do
+  let sender ← msgSender
+  let isR ← getMapping relayersSlot sender
+  requireError (isR != 0) PoolUnauthorizedRelayer()
+
+function nonreentrant(reentrancyLockSlot) transfer
+    (transactions : Array Transaction) with onlyRelayer : Unit := do
+  let txLen := arrayLength transactions
+  requireError (txLen != 0) PoolEmptyTransactions()
+  forEach "i" txLen (do
+    let txn := arrayElement transactions i
+    let verifierRouter ← getStorageAddr stateVerifierRouter
+    let (success, circuit) ← tryExternalCall "getCircuit"
+      [verifierRouter, txn.circuitId]
+    requireError success PoolCircuitNotRegistered()
+    requireError (circuit.verifier != 0) PoolCircuitNotRegistered()
+    let (proofOk, ok) ← tryExternalCall "verifySpend"
+      [circuit.verifier, abiEncode txn.proof, txn.merkleRoot,
+       txn.contextHash, txn.nullifierHashes, txn.newCommitments]
+    requireError proofOk PoolProofVerificationFailed()
+    requireError ok PoolProofVerificationFailed()
+    let leaves ← realCommitments txn.newCommitments maxUint
+    let startIndex ← nextLeafIndex
+    let newRoot ← insertLeaves leaves
+    emit "Transferred"
+      [newRoot, startIndex, leaves,
+       realNullifiers txn.nullifierHashes, txn.ciphertexts])
+```
diff --git a/docs-site/content/index.mdx b/docs-site/content/index.mdx
index f541c47ec..0b282f67f 100644
--- a/docs-site/content/index.mdx
+++ b/docs-site/content/index.mdx
@@ -41,7 +41,7 @@ This project uses Lean to:
 Each contract has three files:
 
 **1. Specification** (`Contracts/SimpleToken/Spec.lean`)
-```lean
+```verity
 -- What should mint do?
 def mint_spec (to : Address) (amount : Uint256) (s s' : ContractState) : Prop :=
   s'.storageMap 1 to = add (s.storageMap 1 to) amount ∧  -- balance increases
@@ -51,7 +51,7 @@ def mint_spec (to : Address) (amount : Uint256) (s s' : ContractState) : Prop :=
 ```
 
 **2. Implementation** (`Contracts/SimpleToken/SimpleToken.lean`)
-```lean
+```verity
 -- How to implement mint (with overflow protection)
 def mint (to : Address) (amount : Uint256) : Contract Unit := do
   onlyOwner
@@ -64,7 +64,7 @@ def mint (to : Address) (amount : Uint256) : Contract Unit := do
 ```
 
 **3. Proof** (`Contracts/SimpleToken/Proofs/Basic.lean`)
-```lean
+```verity
 -- Proof that implementation satisfies specification
 theorem mint_meets_spec (s : ContractState) (to : Address) (amount : Uint256)
   (h_owner : s.sender = s.storageAddr 0) :
diff --git a/docs-site/content/research.mdx b/docs-site/content/research.mdx
index 2973b2444..1c30bd8c3 100644
--- a/docs-site/content/research.mdx
+++ b/docs-site/content/research.mdx
@@ -56,7 +56,7 @@ Two approaches coexist for overflow safety:
 ## Proof Techniques
 
 **Full unfolding** is the main approach:
-```lean
+```verity
 simp only [operation, onlyOwner, isOwner, owner,
   msgSender, getStorageAddr, setStorage,
   Verity.bind, Bind.bind, Pure.pure,
diff --git a/docs-site/content/verification.mdx b/docs-site/content/verification.mdx
index 0970bf036..f41753eef 100644
--- a/docs-site/content/verification.mdx
+++ b/docs-site/content/verification.mdx
@@ -45,7 +45,7 @@ Verity/Proofs/Stdlib/     # Reusable proof infrastructure (Math, Automation, etc
 
 The `ContractResult` type models Solidity's `require` explicitly:
 
-```lean
+```verity
 inductive ContractResult (α : Type) where
   | success : α → ContractState → ContractResult α
   | revert : String → ContractState → ContractResult α
diff --git a/docs-site/next.config.mjs b/docs-site/next.config.mjs
index d7c7a3e01..ae23bb491 100644
--- a/docs-site/next.config.mjs
+++ b/docs-site/next.config.mjs
@@ -1,15 +1,43 @@
 import { dirname } from "path";
+import { readFileSync } from "fs";
 import { fileURLToPath } from "url";
 import nextra from "nextra";
+import { bundledLanguages, createHighlighter } from "shiki";
 
 const configDir = dirname(fileURLToPath(import.meta.url));
 const isDev = process.env.NODE_ENV !== "production";
+const verityGrammar = JSON.parse(readFileSync(`${configDir}/syntaxes/verity.tmLanguage.json`, "utf8"));
+const lfglabsCreamTheme = JSON.parse(readFileSync(`${configDir}/themes/lfglabs-cream.json`, "utf8"));
 
 const withNextra = nextra({
   latex: true,
   search: {
     codeblocks: false,
   },
+  mdxOptions: {
+    rehypePrettyCodeOptions: {
+      theme: lfglabsCreamTheme,
+      getHighlighter(options) {
+        const langs = Object.keys(bundledLanguages).filter((lang) => lang !== "mermaid");
+
+        return createHighlighter({
+          ...options,
+          themes: [
+            lfglabsCreamTheme,
+            ...((options.themes ?? options.theme) ? [] : []),
+          ],
+          langs: [
+            ...langs,
+            {
+              ...verityGrammar,
+              name: "verity",
+              aliases: ["vty"],
+            },
+          ],
+        });
+      },
+    },
+  },
 });
 
 export default withNextra({
diff --git a/docs-site/package-lock.json b/docs-site/package-lock.json
index e756602c3..cc94869de 100644
--- a/docs-site/package-lock.json
+++ b/docs-site/package-lock.json
@@ -19,6 +19,7 @@
         "nextra-theme-docs": "^4.6.1",
         "react": "^19.2.1",
         "react-dom": "^19.2.1",
+        "shiki": "^3.23.0",
         "tailwind-merge": "^2.6.0",
         "tailwindcss": "^4.1.0"
       },
@@ -1377,38 +1378,82 @@
       }
     },
     "node_modules/@shikijs/engine-javascript": {
-      "version": "3.22.0",
-      "resolved": "https://registry.npmjs.org/@shikijs/engine-javascript/-/engine-javascript-3.22.0.tgz",
-      "integrity": "sha512-jdKhfgW9CRtj3Tor0L7+yPwdG3CgP7W+ZEqSsojrMzCjD1e0IxIbwUMDDpYlVBlC08TACg4puwFGkZfLS+56Tw==",
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/engine-javascript/-/engine-javascript-3.23.0.tgz",
+      "integrity": "sha512-aHt9eiGFobmWR5uqJUViySI1bHMqrAgamWE1TYSUoftkAeCCAiGawPMwM+VCadylQtF4V3VNOZ5LmfItH5f3yA==",
+      "license": "MIT",
       "dependencies": {
-        "@shikijs/types": "3.22.0",
+        "@shikijs/types": "3.23.0",
         "@shikijs/vscode-textmate": "^10.0.2",
         "oniguruma-to-es": "^4.3.4"
       }
     },
+    "node_modules/@shikijs/engine-javascript/node_modules/@shikijs/types": {
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/types/-/types-3.23.0.tgz",
+      "integrity": "sha512-3JZ5HXOZfYjsYSk0yPwBrkupyYSLpAE26Qc0HLghhZNGTZg/SKxXIIgoxOpmmeQP0RRSDJTk1/vPfw9tbw+jSQ==",
+      "license": "MIT",
+      "dependencies": {
+        "@shikijs/vscode-textmate": "^10.0.2",
+        "@types/hast": "^3.0.4"
+      }
+    },
     "node_modules/@shikijs/engine-oniguruma": {
-      "version": "3.22.0",
-      "resolved": "https://registry.npmjs.org/@shikijs/engine-oniguruma/-/engine-oniguruma-3.22.0.tgz",
-      "integrity": "sha512-DyXsOG0vGtNtl7ygvabHd7Mt5EY8gCNqR9Y7Lpbbd/PbJvgWrqaKzH1JW6H6qFkuUa8aCxoiYVv8/YfFljiQxA==",
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/engine-oniguruma/-/engine-oniguruma-3.23.0.tgz",
+      "integrity": "sha512-1nWINwKXxKKLqPibT5f4pAFLej9oZzQTsby8942OTlsJzOBZ0MWKiwzMsd+jhzu8YPCHAswGnnN1YtQfirL35g==",
+      "license": "MIT",
       "dependencies": {
-        "@shikijs/types": "3.22.0",
+        "@shikijs/types": "3.23.0",
         "@shikijs/vscode-textmate": "^10.0.2"
       }
     },
+    "node_modules/@shikijs/engine-oniguruma/node_modules/@shikijs/types": {
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/types/-/types-3.23.0.tgz",
+      "integrity": "sha512-3JZ5HXOZfYjsYSk0yPwBrkupyYSLpAE26Qc0HLghhZNGTZg/SKxXIIgoxOpmmeQP0RRSDJTk1/vPfw9tbw+jSQ==",
+      "license": "MIT",
+      "dependencies": {
+        "@shikijs/vscode-textmate": "^10.0.2",
+        "@types/hast": "^3.0.4"
+      }
+    },
     "node_modules/@shikijs/langs": {
-      "version": "3.22.0",
-      "resolved": "https://registry.npmjs.org/@shikijs/langs/-/langs-3.22.0.tgz",
-      "integrity": "sha512-x/42TfhWmp6H00T6uwVrdTJGKgNdFbrEdhaDwSR5fd5zhQ1Q46bHq9EO61SCEWJR0HY7z2HNDMaBZp8JRmKiIA==",
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/langs/-/langs-3.23.0.tgz",
+      "integrity": "sha512-2Ep4W3Re5aB1/62RSYQInK9mM3HsLeB91cHqznAJMuylqjzNVAVCMnNWRHFtcNHXsoNRayP9z1qj4Sq3nMqYXg==",
+      "license": "MIT",
       "dependencies": {
-        "@shikijs/types": "3.22.0"
+        "@shikijs/types": "3.23.0"
+      }
+    },
+    "node_modules/@shikijs/langs/node_modules/@shikijs/types": {
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/types/-/types-3.23.0.tgz",
+      "integrity": "sha512-3JZ5HXOZfYjsYSk0yPwBrkupyYSLpAE26Qc0HLghhZNGTZg/SKxXIIgoxOpmmeQP0RRSDJTk1/vPfw9tbw+jSQ==",
+      "license": "MIT",
+      "dependencies": {
+        "@shikijs/vscode-textmate": "^10.0.2",
+        "@types/hast": "^3.0.4"
       }
     },
     "node_modules/@shikijs/themes": {
-      "version": "3.22.0",
-      "resolved": "https://registry.npmjs.org/@shikijs/themes/-/themes-3.22.0.tgz",
-      "integrity": "sha512-o+tlOKqsr6FE4+mYJG08tfCFDS+3CG20HbldXeVoyP+cYSUxDhrFf3GPjE60U55iOkkjbpY2uC3It/eeja35/g==",
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/themes/-/themes-3.23.0.tgz",
+      "integrity": "sha512-5qySYa1ZgAT18HR/ypENL9cUSGOeI2x+4IvYJu4JgVJdizn6kG4ia5Q1jDEOi7gTbN4RbuYtmHh0W3eccOrjMA==",
+      "license": "MIT",
       "dependencies": {
-        "@shikijs/types": "3.22.0"
+        "@shikijs/types": "3.23.0"
+      }
+    },
+    "node_modules/@shikijs/themes/node_modules/@shikijs/types": {
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/types/-/types-3.23.0.tgz",
+      "integrity": "sha512-3JZ5HXOZfYjsYSk0yPwBrkupyYSLpAE26Qc0HLghhZNGTZg/SKxXIIgoxOpmmeQP0RRSDJTk1/vPfw9tbw+jSQ==",
+      "license": "MIT",
+      "dependencies": {
+        "@shikijs/vscode-textmate": "^10.0.2",
+        "@types/hast": "^3.0.4"
       }
     },
     "node_modules/@shikijs/twoslash": {
@@ -5377,17 +5422,19 @@
       }
     },
     "node_modules/oniguruma-parser": {
-      "version": "0.12.1",
-      "resolved": "https://registry.npmjs.org/oniguruma-parser/-/oniguruma-parser-0.12.1.tgz",
-      "integrity": "sha512-8Unqkvk1RYc6yq2WBYRj4hdnsAxVze8i7iPfQr8e4uSP3tRv0rpZcbGUDvxfQQcdwHt/e9PrMvGCsa8OqG9X3w=="
+      "version": "0.12.2",
+      "resolved": "https://registry.npmjs.org/oniguruma-parser/-/oniguruma-parser-0.12.2.tgz",
+      "integrity": "sha512-6HVa5oIrgMC6aA6WF6XyyqbhRPJrKR02L20+2+zpDtO5QAzGHAUGw5TKQvwi5vctNnRHkJYmjAhRVQF2EKdTQw==",
+      "license": "MIT"
     },
     "node_modules/oniguruma-to-es": {
-      "version": "4.3.4",
-      "resolved": "https://registry.npmjs.org/oniguruma-to-es/-/oniguruma-to-es-4.3.4.tgz",
-      "integrity": "sha512-3VhUGN3w2eYxnTzHn+ikMI+fp/96KoRSVK9/kMTcFqj1NRDh2IhQCKvYxDnWePKRXY/AqH+Fuiyb7VHSzBjHfA==",
+      "version": "4.3.6",
+      "resolved": "https://registry.npmjs.org/oniguruma-to-es/-/oniguruma-to-es-4.3.6.tgz",
+      "integrity": "sha512-csuQ9x3Yr0cEIs/Zgx/OEt9iBw9vqIunAPQkx19R/fiMq2oGVTgcMqO/V3Ybqefr1TBvosI6jU539ksaBULJyA==",
+      "license": "MIT",
       "dependencies": {
-        "oniguruma-parser": "^0.12.1",
-        "regex": "^6.0.1",
+        "oniguruma-parser": "^0.12.2",
+        "regex": "^6.1.0",
         "regex-recursion": "^6.0.2"
       }
     },
@@ -5701,6 +5748,7 @@
       "version": "6.1.0",
       "resolved": "https://registry.npmjs.org/regex/-/regex-6.1.0.tgz",
       "integrity": "sha512-6VwtthbV4o/7+OaAF9I5L5V3llLEsoPyq9P1JVXkedTP33c7MfCG0/5NOPcSJn0TzXcG9YUrR0gQSWioew3LDg==",
+      "license": "MIT",
       "dependencies": {
         "regex-utilities": "^2.3.0"
       }
@@ -5709,6 +5757,7 @@
       "version": "6.0.2",
       "resolved": "https://registry.npmjs.org/regex-recursion/-/regex-recursion-6.0.2.tgz",
       "integrity": "sha512-0YCaSCq2VRIebiaUviZNs0cBz1kg5kVS2UKUfNIx8YVs1cN3AV7NTctO5FOKBA+UT2BPJIWZauYHPqJODG50cg==",
+      "license": "MIT",
       "dependencies": {
         "regex-utilities": "^2.3.0"
       }
@@ -5716,7 +5765,8 @@
     "node_modules/regex-utilities": {
       "version": "2.3.0",
       "resolved": "https://registry.npmjs.org/regex-utilities/-/regex-utilities-2.3.0.tgz",
-      "integrity": "sha512-8VhliFJAWRaUiVvREIiW2NXXTmHs4vMNnSzuJVhscgmGav3g9VDxLrQndI3dZZVVdp0ZO/5v0xmX516/7M9cng=="
+      "integrity": "sha512-8VhliFJAWRaUiVvREIiW2NXXTmHs4vMNnSzuJVhscgmGav3g9VDxLrQndI3dZZVVdp0ZO/5v0xmX516/7M9cng==",
+      "license": "MIT"
     },
     "node_modules/rehype-katex": {
       "version": "7.0.1",
@@ -6188,16 +6238,39 @@
       }
     },
     "node_modules/shiki": {
-      "version": "3.22.0",
-      "resolved": "https://registry.npmjs.org/shiki/-/shiki-3.22.0.tgz",
-      "integrity": "sha512-LBnhsoYEe0Eou4e1VgJACes+O6S6QC0w71fCSp5Oya79inkwkm15gQ1UF6VtQ8j/taMDh79hAB49WUk8ALQW3g==",
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/shiki/-/shiki-3.23.0.tgz",
+      "integrity": "sha512-55Dj73uq9ZXL5zyeRPzHQsK7Nbyt6Y10k5s7OjuFZGMhpp4r/rsLBH0o/0fstIzX1Lep9VxefWljK/SKCzygIA==",
+      "license": "MIT",
+      "dependencies": {
+        "@shikijs/core": "3.23.0",
+        "@shikijs/engine-javascript": "3.23.0",
+        "@shikijs/engine-oniguruma": "3.23.0",
+        "@shikijs/langs": "3.23.0",
+        "@shikijs/themes": "3.23.0",
+        "@shikijs/types": "3.23.0",
+        "@shikijs/vscode-textmate": "^10.0.2",
+        "@types/hast": "^3.0.4"
+      }
+    },
+    "node_modules/shiki/node_modules/@shikijs/core": {
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/core/-/core-3.23.0.tgz",
+      "integrity": "sha512-NSWQz0riNb67xthdm5br6lAkvpDJRTgB36fxlo37ZzM2yq0PQFFzbd8psqC2XMPgCzo1fW6cVi18+ArJ44wqgA==",
+      "license": "MIT",
+      "dependencies": {
+        "@shikijs/types": "3.23.0",
+        "@shikijs/vscode-textmate": "^10.0.2",
+        "@types/hast": "^3.0.4",
+        "hast-util-to-html": "^9.0.5"
+      }
+    },
+    "node_modules/shiki/node_modules/@shikijs/types": {
+      "version": "3.23.0",
+      "resolved": "https://registry.npmjs.org/@shikijs/types/-/types-3.23.0.tgz",
+      "integrity": "sha512-3JZ5HXOZfYjsYSk0yPwBrkupyYSLpAE26Qc0HLghhZNGTZg/SKxXIIgoxOpmmeQP0RRSDJTk1/vPfw9tbw+jSQ==",
+      "license": "MIT",
       "dependencies": {
-        "@shikijs/core": "3.22.0",
-        "@shikijs/engine-javascript": "3.22.0",
-        "@shikijs/engine-oniguruma": "3.22.0",
-        "@shikijs/langs": "3.22.0",
-        "@shikijs/themes": "3.22.0",
-        "@shikijs/types": "3.22.0",
         "@shikijs/vscode-textmate": "^10.0.2",
         "@types/hast": "^3.0.4"
       }
diff --git a/docs-site/package.json b/docs-site/package.json
index d4038a9cc..633c284d8 100644
--- a/docs-site/package.json
+++ b/docs-site/package.json
@@ -6,7 +6,8 @@
   "description": "Verity documentation website - Minimal Lean EDSL for smart contracts",
   "scripts": {
     "dev": "next dev -p 3003",
-    "build": "next build && pagefind --site .next/server/app --output-path public/_pagefind",
+    "build": "next build --webpack && pagefind --site .next/server/app --output-path public/_pagefind",
+    "check:highlighting": "node scripts/check-verity-highlighting.mjs",
     "start": "next start -p 3003"
   },
   "dependencies": {
@@ -21,6 +22,7 @@
     "nextra-theme-docs": "^4.6.1",
     "react": "^19.2.1",
     "react-dom": "^19.2.1",
+    "shiki": "^3.23.0",
     "tailwind-merge": "^2.6.0",
     "tailwindcss": "^4.1.0"
   },
diff --git a/docs-site/scripts/check-verity-highlighting.mjs b/docs-site/scripts/check-verity-highlighting.mjs
new file mode 100644
index 000000000..814f875a9
--- /dev/null
+++ b/docs-site/scripts/check-verity-highlighting.mjs
@@ -0,0 +1,115 @@
+import { readFileSync } from "fs";
+import { dirname, join } from "path";
+import { fileURLToPath } from "url";
+import { bundledLanguages, createHighlighter } from "shiki";
+
+const here = dirname(fileURLToPath(import.meta.url));
+const docsRoot = join(here, "..");
+const grammar = JSON.parse(readFileSync(join(docsRoot, "syntaxes/verity.tmLanguage.json"), "utf8"));
+const theme = JSON.parse(readFileSync(join(docsRoot, "themes/lfglabs-cream.json"), "utf8"));
+
+const sample = `verity_contract UnlinkPool where
+  storage
+    relayersSlot : Address -> Uint256 := slot 0
+
+  linked_externals
+    external getCircuit(Address, Uint256) -> (Circuit)
+    external getCircuit_try(Address, Uint256) -> (Bool, Circuit)
+
+  modifier onlyRelayer := do
+    let sender ← msgSender
+    let isR ← getMapping relayersSlot sender
+    requireError (isR != 0) PoolUnauthorizedRelayer()
+
+  function nonreentrant(reentrancyLockSlot) transfer
+      (transactions : Array Transaction) with onlyRelayer : Unit := do
+    let txLen := arrayLength transactions
+    requireError (txLen != 0) PoolEmptyTransactions()
+    forEach "i" txLen (do
+      let txn := arrayElement transactions i
+      let verifierRouter ← getStorageAddr stateVerifierRouter
+      let (success, circuit) ← tryExternalCall "getCircuit"
+        [verifierRouter, txn.circuitId]
+      requireError success PoolCircuitNotRegistered()
+      requireError (circuit.verifier != 0) PoolCircuitNotRegistered()
+      let (proofOk, ok) ← tryExternalCall "verifySpend"
+        [circuit.verifier, abiEncode txn.proof, txn.merkleRoot,
+         txn.contextHash, txn.nullifierHashes, txn.newCommitments]
+      requireError proofOk PoolProofVerificationFailed()
+      requireError ok PoolProofVerificationFailed()
+      let leaves ← realCommitments txn.newCommitments maxUint
+      let startIndex ← nextLeafIndex
+      let newRoot ← insertLeaves leaves
+      emit "Transferred"
+        [newRoot, startIndex, leaves,
+         realNullifiers txn.nullifierHashes, txn.ciphertexts])
+`;
+
+const highlighter = await createHighlighter({
+  themes: [theme],
+  langs: [
+    ...Object.keys(bundledLanguages).filter((lang) => lang !== "mermaid"),
+    {
+      ...grammar,
+      name: "verity",
+      aliases: ["vty"],
+    },
+  ],
+});
+
+const tokens = highlighter.codeToTokens(sample, {
+  lang: "verity",
+  theme: "LFGLabs Cream",
+  includeExplanation: true,
+}).tokens.flat();
+
+function scopesFor(content) {
+  return tokens.flatMap((token) =>
+    token.explanation
+      .filter((part) => part.content.trim() === content || part.content.includes(content))
+      .flatMap((part) => part.scopes.map((scope) => scope.scopeName))
+  );
+}
+
+const expectations = [
+  ["verity_contract", "keyword.declaration.contract.verity"],
+  ["UnlinkPool", "entity.name.type.contract.verity"],
+  ["storage", "keyword.other.section.verity"],
+  ["relayersSlot", "variable.other.storage.verity"],
+  ["Address", "storage.type.verity"],
+  ["slot", "keyword.other.slot.verity"],
+  ["external", "keyword.declaration.external.verity"],
+  ["getCircuit", "entity.name.function.external.verity"],
+  ["modifier", "keyword.declaration.modifier.verity"],
+  ["onlyRelayer", "entity.name.function.modifier.verity"],
+  ["function", "keyword.declaration.function.verity"],
+  ["nonreentrant", "storage.modifier.reentrancy.verity"],
+  ["transfer", "entity.name.function.verity"],
+  ["with", "keyword.control.modifier-clause.verity"],
+  ["msgSender", "support.function.context.verity"],
+  ["getMapping", "support.function.storage.verity"],
+  ["requireError", "support.function.guard.verity"],
+  ["arrayLength", "support.function.storage.verity"],
+  ["forEach", "support.function.loop.verity"],
+  ["tryExternalCall", "support.function.external-call.verity"],
+  ["abiEncode", "support.function.abi.verity"],
+  ["proof", "variable.other.property.verity"],
+  ["PoolCircuitNotRegistered", "entity.name.exception.custom-error.verity"],
+  ["emit", "support.function.event.verity"],
+  ["\"Transferred\"", "entity.name.function.event.verity"],
+];
+
+const failures = expectations.filter(([content, expectedScope]) => {
+  const scopes = scopesFor(content);
+  return !scopes.includes(expectedScope);
+});
+
+if (failures.length > 0) {
+  console.error("Verity highlighting scope check failed:");
+  for (const [content, expectedScope] of failures) {
+    console.error(`- ${content}: expected ${expectedScope}, got ${scopesFor(content).join(", ") || "no token"}`);
+  }
+  process.exit(1);
+}
+
+console.log(`Verified ${expectations.length} Verity syntax highlighting scopes.`);
diff --git a/docs-site/syntaxes/verity.tmLanguage.json b/docs-site/syntaxes/verity.tmLanguage.json
new file mode 100644
index 000000000..71475c406
--- /dev/null
+++ b/docs-site/syntaxes/verity.tmLanguage.json
@@ -0,0 +1,519 @@
+{
+  "$schema": "https://raw.githubusercontent.com/martinring/tmlanguage/master/tmlanguage.json",
+  "name": "Verity",
+  "scopeName": "source.verity",
+  "fileTypes": [
+    "verity"
+  ],
+  "patterns": [
+    {
+      "include": "#comments"
+    },
+    {
+      "include": "#errors-and-events"
+    },
+    {
+      "include": "#strings"
+    },
+    {
+      "include": "#contract"
+    },
+    {
+      "include": "#sections"
+    },
+    {
+      "include": "#functions"
+    },
+    {
+      "include": "#modifiers"
+    },
+    {
+      "include": "#declarations"
+    },
+    {
+      "include": "#edsl"
+    },
+    {
+      "include": "#abi"
+    },
+    {
+      "include": "#field-access"
+    },
+    {
+      "include": "#types"
+    },
+    {
+      "include": "#storage-slots"
+    },
+    {
+      "include": "#addresses"
+    },
+    {
+      "include": "#numbers"
+    },
+    {
+      "include": "#operators"
+    },
+    {
+      "include": "source.lean"
+    }
+  ],
+  "repository": {
+    "comments": {
+      "patterns": [
+        {
+          "name": "comment.block.documentation.verity",
+          "begin": "/--",
+          "end": "-/"
+        },
+        {
+          "name": "comment.block.verity",
+          "begin": "/-",
+          "end": "-/"
+        },
+        {
+          "name": "comment.line.double-dash.verity",
+          "match": "--.*$"
+        }
+      ]
+    },
+    "strings": {
+      "patterns": [
+        {
+          "name": "string.quoted.double.verity",
+          "begin": "\"",
+          "end": "\"",
+          "patterns": [
+            {
+              "name": "constant.character.escape.verity",
+              "match": "\\\\."
+            }
+          ]
+        }
+      ]
+    },
+    "contract": {
+      "patterns": [
+        {
+          "name": "meta.contract.verity",
+          "match": "\\b(verity_contract)\\s+([A-Z][A-Za-z0-9_']*)\\s+(where)\\b",
+          "captures": {
+            "1": {
+              "name": "keyword.declaration.contract.verity"
+            },
+            "2": {
+              "name": "entity.name.type.contract.verity"
+            },
+            "3": {
+              "name": "keyword.control.where.verity"
+            }
+          }
+        },
+        {
+          "name": "meta.contract.check.verity",
+          "match": "(#check_contract)\\s+([A-Z][A-Za-z0-9_']*)\\b",
+          "captures": {
+            "1": {
+              "name": "keyword.other.directive.verity"
+            },
+            "2": {
+              "name": "entity.name.type.contract.verity"
+            }
+          }
+        }
+      ]
+    },
+    "sections": {
+      "patterns": [
+        {
+          "name": "keyword.other.section.verity",
+          "match": "^\\s*\\b(storage|types|inductive|errors|event_defs|constants|immutables|linked_externals)\\b"
+        },
+        {
+          "name": "meta.block.linked-externals.verity",
+          "begin": "^\\s*(linked_externals)\\b",
+          "beginCaptures": {
+            "1": {
+              "name": "keyword.other.section.linked-externals.verity"
+            }
+          },
+          "end": "^(?=\\s*(?:storage|types|inductive|errors|event_defs|constants|immutables|function|constructor|receive|fallback|modifier|local_obligations)\\b)",
+          "patterns": [
+            {
+              "include": "#comments"
+            },
+            {
+              "include": "#strings"
+            },
+            {
+              "name": "meta.external.typed.verity",
+              "match": "\\b(external)\\s+([a-zA-Z_][A-Za-z0-9_']*)\\s*(\\()",
+              "captures": {
+                "1": {
+                  "name": "keyword.declaration.external.verity"
+                },
+                "2": {
+                  "name": "entity.name.function.external.verity"
+                },
+                "3": {
+                  "name": "punctuation.definition.parameters.begin.verity"
+                }
+              }
+            },
+            {
+              "include": "#types"
+            },
+            {
+              "include": "#operators"
+            },
+            {
+              "include": "#numbers"
+            }
+          ]
+        },
+        {
+          "name": "meta.storage-field.verity",
+          "match": "^\\s*([a-zA-Z_][A-Za-z0-9_']*)\\s*(:)\\s*([^:=]+?)\\s*(:=)\\s*(slot)\\s+(0x[0-9A-Fa-f]+|[0-9]+)",
+          "captures": {
+            "1": {
+              "name": "variable.other.storage.verity"
+            },
+            "2": {
+              "name": "punctuation.separator.type.verity"
+            },
+            "3": {
+              "name": "storage.type.verity"
+            },
+            "4": {
+              "name": "keyword.operator.assignment.verity"
+            },
+            "5": {
+              "name": "keyword.other.slot.verity"
+            },
+            "6": {
+              "name": "constant.numeric.storage-slot.verity"
+            }
+          }
+        },
+        {
+          "name": "meta.constant.verity",
+          "match": "^\\s*([a-zA-Z_][A-Za-z0-9_']*)\\s*(:)\\s*([A-Z][A-Za-z0-9_']*)\\s*(:=)",
+          "captures": {
+            "1": {
+              "name": "constant.other.contract.verity"
+            },
+            "2": {
+              "name": "punctuation.separator.type.verity"
+            },
+            "3": {
+              "name": "storage.type.verity"
+            },
+            "4": {
+              "name": "keyword.operator.assignment.verity"
+            }
+          }
+        },
+        {
+          "name": "meta.external.verity",
+          "match": "^\\s*(external)\\s+([a-zA-Z_][A-Za-z0-9_']*)\\s*(\\()",
+          "captures": {
+            "1": {
+              "name": "keyword.declaration.external.verity"
+            },
+            "2": {
+              "name": "entity.name.function.external.verity"
+            },
+            "3": {
+              "name": "punctuation.definition.parameters.begin.verity"
+            }
+          }
+        }
+      ]
+    },
+    "functions": {
+      "patterns": [
+        {
+          "name": "meta.function.header.verity",
+          "begin": "^\\s*(function)\\b",
+          "beginCaptures": {
+            "1": {
+              "name": "keyword.declaration.function.verity"
+            }
+          },
+          "end": "(:=)\\s*(do)\\b",
+          "endCaptures": {
+            "1": {
+              "name": "keyword.operator.assignment.verity"
+            },
+            "2": {
+              "name": "keyword.control.do.verity"
+            }
+          },
+          "patterns": [
+            {
+              "name": "storage.modifier.reentrancy.verity",
+              "match": "\\bnonreentrant\\s*\\([^)]*\\)"
+            },
+            {
+              "name": "storage.modifier.verity",
+              "match": "\\b(payable|view|no_external_calls|allow_post_interaction_writes|cei_safe|initializer|reinitializer)\\b"
+            },
+            {
+              "name": "meta.modifier.clause.verity",
+              "match": "\\b(with)\\s+([a-zA-Z_][A-Za-z0-9_']*)",
+              "captures": {
+                "1": {
+                  "name": "keyword.control.modifier-clause.verity"
+                },
+                "2": {
+                  "name": "entity.name.function.modifier.verity"
+                }
+              }
+            },
+            {
+              "name": "entity.name.function.verity",
+              "match": "\\b[a-zA-Z_][A-Za-z0-9_']*(?=\\s*(?:\\(|:|with|$))"
+            },
+            {
+              "include": "#types"
+            },
+            {
+              "include": "#operators"
+            },
+            {
+              "name": "punctuation.definition.parameters.begin.verity",
+              "match": "\\("
+            },
+            {
+              "name": "punctuation.definition.parameters.end.verity",
+              "match": "\\)"
+            }
+          ]
+        },
+        {
+          "name": "meta.constructor.verity",
+          "match": "^\\s*(constructor|receive|fallback)\\b\\s*([a-zA-Z_][A-Za-z0-9_']*)?",
+          "captures": {
+            "1": {
+              "name": "keyword.declaration.function.verity"
+            },
+            "2": {
+              "name": "entity.name.function.verity"
+            }
+          }
+        },
+        {
+          "name": "meta.local-obligation.verity",
+          "match": "\\b(local_obligations|assumed)\\b|\\b([A-Za-z_][A-Za-z0-9_']*)\\s*(:=)\\s*(assumed)",
+          "captures": {
+            "1": {
+              "name": "keyword.other.obligation.verity"
+            },
+            "2": {
+              "name": "entity.name.tag.obligation.verity"
+            },
+            "3": {
+              "name": "keyword.operator.assignment.verity"
+            },
+            "4": {
+              "name": "keyword.other.obligation.verity"
+            }
+          }
+        }
+      ]
+    },
+    "modifiers": {
+      "patterns": [
+        {
+          "name": "meta.modifier.declaration.verity",
+          "begin": "^\\s*(modifier)\\s+([a-zA-Z_][A-Za-z0-9_']*)\\b",
+          "beginCaptures": {
+            "1": {
+              "name": "keyword.declaration.modifier.verity"
+            },
+            "2": {
+              "name": "entity.name.function.modifier.verity"
+            }
+          },
+          "end": "(:=)\\s*(do)\\b|$",
+          "endCaptures": {
+            "1": {
+              "name": "keyword.operator.assignment.verity"
+            },
+            "2": {
+              "name": "keyword.control.do.verity"
+            }
+          },
+          "patterns": [
+            {
+              "include": "#types"
+            },
+            {
+              "include": "#operators"
+            }
+          ]
+        },
+        {
+          "name": "storage.modifier.verity",
+          "match": "\\b(requires|modifies|with)\\b"
+        }
+      ]
+    },
+    "declarations": {
+      "patterns": [
+        {
+          "name": "keyword.declaration.lean.verity",
+          "match": "\\b(import|namespace|end|open|def|theorem|lemma|example|structure|inductive|where|deriving|instance|class)\\b"
+        },
+        {
+          "name": "keyword.control.lean.verity",
+          "match": "\\b(do|by|let|mut|if|then|else|match|return|pure|for|in|have|show|from|fun|forall)\\b"
+        },
+        {
+          "name": "support.function.tactic.verity",
+          "match": "\\b(simp|simp_all|rw|rfl|omega|constructor|cases|case|intro|intros|exact|apply|unfold|split|aesop|decide|norm_num)\\b"
+        }
+      ]
+    },
+    "edsl": {
+      "patterns": [
+        {
+          "name": "support.function.storage.verity",
+          "match": "\\b(getStorage|setStorage|getStorageAddr|setStorageAddr|getMapping|getMappingUint|getMapping2|setMapping|setMappingUint|setMapping2|structMembers|structMembers2|arrayLength|arrayElement)\\b"
+        },
+        {
+          "name": "support.function.context.verity",
+          "match": "\\b(msgSender|msgValue|blockTimestamp|blockNumber|contractAddress|chainid|blobbasefee|defaultState)\\b"
+        },
+        {
+          "name": "support.function.guard.verity",
+          "match": "\\b(require|requireSomeUint|requireError|revert|revertError)\\b"
+        },
+        {
+          "name": "support.function.external-call.verity",
+          "match": "\\b(tryExternalCall|externalCall|ecmBind|ecmCall|ecmDo|tryCatch)\\b"
+        },
+        {
+          "name": "support.function.event.verity",
+          "match": "\\b(emitEvent|emit)\\b"
+        },
+        {
+          "name": "support.function.loop.verity",
+          "match": "\\b(forEach|forEach2)\\b"
+        },
+        {
+          "name": "support.function.arithmetic.verity",
+          "match": "\\b(add|sub|mul|div|mod|pow|safeAdd|safeSub|safeMul|safeDiv|mulDivDown|mulDivUp|wMulDown|wDivUp|mulDiv512Down\\?|mulDiv512Up\\?|wordToAddress|keccak256)\\b"
+        },
+        {
+          "name": "support.function.spec.verity",
+          "match": "\\b(storageMapUnchangedExceptKeyAtSlot|storageMapUnchangedExceptKey|storageMapUnchangedExceptSlot|sameStorage|sameStorageAddr|sameContext|sameStorageAddrContext|sameEvents|sameExcept|run|getValue\\?)\\b"
+        },
+        {
+          "name": "variable.language.verity",
+          "match": "\\b(self|sender|thisAddress|totalSupply|owner|balances|allowances)\\b"
+        }
+      ]
+    },
+    "abi": {
+      "patterns": [
+        {
+          "name": "support.function.abi.verity",
+          "match": "\\b(abiEncode|abiHeadWord|abiWord|abiBytes|abiArray|abiDynamicHeadWord|abiDynamicTail)\\b"
+        }
+      ]
+    },
+    "errors-and-events": {
+      "patterns": [
+        {
+          "name": "entity.name.exception.custom-error.verity",
+          "match": "\\b[A-Z][A-Za-z0-9_']*Error\\b|\\bPool[A-Za-z0-9_']*(?=\\s*\\()"
+        },
+        {
+          "name": "entity.name.function.event.verity",
+          "match": "\"(?:[A-Z][A-Za-z0-9_']*(?:ed|n|d|red|redn|Transfer|Approval|Withdrawn|Transferred|Deposited))\""
+        }
+      ]
+    },
+    "field-access": {
+      "patterns": [
+        {
+          "name": "meta.field-access.verity",
+          "match": "(\\.)([a-zA-Z_][A-Za-z0-9_']*)",
+          "captures": {
+            "1": {
+              "name": "punctuation.accessor.verity"
+            },
+            "2": {
+              "name": "variable.other.property.verity"
+            }
+          }
+        }
+      ]
+    },
+    "types": {
+      "patterns": [
+        {
+          "name": "storage.type.verity",
+          "match": "\\b(Contract|ContractState|StorageSlot|Address|Uint256|Uint128|Uint64|Uint32|Uint16|Uint8|Bool|Unit|String|Bytes|List|Option|Tuple|MappingStruct|MappingStruct2|Prop|Nat|Int)\\b"
+        },
+        {
+          "name": "constant.language.boolean.verity",
+          "match": "\\b(true|false|none|some)\\b"
+        }
+      ]
+    },
+    "storage-slots": {
+      "patterns": [
+        {
+          "name": "constant.numeric.storage-slot.verity",
+          "match": "\\bslot\\s+(0x[0-9A-Fa-f]+|[0-9]+)"
+        },
+        {
+          "name": "keyword.other.slot.verity",
+          "match": "\\bslot\\b"
+        }
+      ]
+    },
+    "addresses": {
+      "patterns": [
+        {
+          "name": "constant.numeric.address.verity",
+          "match": "\\b0x[a-fA-F0-9]{40}\\b"
+        }
+      ]
+    },
+    "numbers": {
+      "patterns": [
+        {
+          "name": "constant.numeric.hex.verity",
+          "match": "\\b0x[0-9A-Fa-f]+\\b"
+        },
+        {
+          "name": "constant.numeric.decimal.verity",
+          "match": "\\b[0-9]+\\b"
+        }
+      ]
+    },
+    "operators": {
+      "patterns": [
+        {
+          "name": "keyword.operator.assignment.verity",
+          "match": ":=|<-|←|=>|→|->"
+        },
+        {
+          "name": "keyword.operator.comparison.verity",
+          "match": "==|!=|<=|>=|<|>"
+        },
+        {
+          "name": "keyword.operator.logical.verity",
+          "match": "&&|\\|\\||∧|∨|¬"
+        },
+        {
+          "name": "keyword.operator.arithmetic.verity",
+          "match": "\\+|-|\\*|/|\\^|%"
+        }
+      ]
+    }
+  }
+}
diff --git a/docs-site/themes/lfglabs-cream.json b/docs-site/themes/lfglabs-cream.json
new file mode 100644
index 000000000..6847bc484
--- /dev/null
+++ b/docs-site/themes/lfglabs-cream.json
@@ -0,0 +1,182 @@
+{
+  "$schema": "https://raw.githubusercontent.com/shikijs/textmate-grammars-themes/main/packages/tm-themes/schema.json",
+  "name": "LFGLabs Cream",
+  "type": "light",
+  "colors": {
+    "editor.background": "#fffaf1",
+    "editor.foreground": "#302b25",
+    "editorLineNumber.foreground": "#b9a992",
+    "editor.selectionBackground": "#eadcca",
+    "editor.inactiveSelectionBackground": "#f2e7d5"
+  },
+  "tokenColors": [
+    {
+      "scope": ["comment", "punctuation.definition.comment"],
+      "settings": {
+        "foreground": "#8a8175",
+        "fontStyle": "italic"
+      }
+    },
+    {
+      "scope": ["string.quoted.double", "string.quoted.double.verity"],
+      "settings": {
+        "foreground": "#6b6f32"
+      }
+    },
+    {
+      "scope": ["entity.name.function.event.verity"],
+      "settings": {
+        "foreground": "#3f7456",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["constant.numeric", "constant.numeric.hex", "constant.numeric.decimal", "constant.numeric.storage-slot"],
+      "settings": {
+        "foreground": "#8b4e2f"
+      }
+    },
+    {
+      "scope": ["constant.language.boolean", "constant.language.boolean.verity"],
+      "settings": {
+        "foreground": "#8b4e2f",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["keyword.declaration.contract.verity", "keyword.declaration.function.verity", "keyword.declaration.modifier.verity", "keyword.declaration.external.verity", "keyword.other.section.verity", "keyword.other.section.linked-externals.verity"],
+      "settings": {
+        "foreground": "#7b3f32",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["keyword.control.modifier-clause.verity", "storage.modifier.verity", "storage.modifier.reentrancy.verity"],
+      "settings": {
+        "foreground": "#875c24",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["keyword.control.do.verity", "keyword.control.lean.verity", "keyword.operator.assignment.verity"],
+      "settings": {
+        "foreground": "#8b7663"
+      }
+    },
+    {
+      "scope": ["keyword.operator", "punctuation.definition.parameters", "punctuation.separator", "punctuation.accessor.verity"],
+      "settings": {
+        "foreground": "#8b7663"
+      }
+    },
+    {
+      "scope": ["entity.name.type.contract.verity", "storage.type.verity", "support.type"],
+      "settings": {
+        "foreground": "#6d4b8f",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["entity.name.function.verity"],
+      "settings": {
+        "foreground": "#2f6c67"
+      }
+    },
+    {
+      "scope": ["entity.name.function.external.verity"],
+      "settings": {
+        "foreground": "#285f91",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["entity.name.function.modifier.verity"],
+      "settings": {
+        "foreground": "#7a5527",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["support.function.guard.verity"],
+      "settings": {
+        "foreground": "#a34537",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["support.function.external-call.verity"],
+      "settings": {
+        "foreground": "#285f91",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["support.function.event.verity"],
+      "settings": {
+        "foreground": "#3f7456",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["support.function.loop.verity"],
+      "settings": {
+        "foreground": "#734f96",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["support.function.abi.verity"],
+      "settings": {
+        "foreground": "#7b4c9a",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["support.function.storage.verity", "support.function.context.verity", "support.function.arithmetic.verity", "support.function.spec.verity"],
+      "settings": {
+        "foreground": "#2f6c67",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["entity.name.exception.custom-error.verity"],
+      "settings": {
+        "foreground": "#a34537",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["variable.other.property.verity"],
+      "settings": {
+        "foreground": "#785b1f",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["variable.other.storage.verity", "variable.language.verity", "variable.other"],
+      "settings": {
+        "foreground": "#31475f"
+      }
+    },
+    {
+      "scope": ["meta.block.linked-externals.verity"],
+      "settings": {
+        "foreground": "#53616a"
+      }
+    },
+    {
+      "scope": ["source.lean keyword", "keyword.declaration.lean.verity"],
+      "settings": {
+        "foreground": "#7b3f32",
+        "fontStyle": "bold"
+      }
+    },
+    {
+      "scope": ["source.lean entity.name.function", "support.function.tactic.verity"],
+      "settings": {
+        "foreground": "#2f6c67"
+      }
+    }
+  ],
+  "semanticHighlighting": false
+}