Website updates for 0.6.0 release

examples.md

@@ -157,7 +157,11 @@ The [KEMPRF](https://github.com/ProofFrog/examples/blob/main/Schemes/KEM/KEMPRF.
 
 A ProofFrog formalization of the four hybrid PQ/T KEM combiners specified in the IRTF CFRG draft [*Hybrid PQ/T Key Encapsulation Mechanisms*](https://datatracker.ietf.org/doc/html/draft-irtf-cfrg-hybrid-kems-10). Each framework combines a post-quantum KEM with a "traditional" component — either another KEM or a nominal group — via a key-derivation function: **UG** and **CG** use a nominal group, **UK** and **CK** use a second KEM; **U**(niversal) and **C**(2PRI) name the two combiner constructions. Each is modelled in two variants (a seed-form matching the draft's primary definition and an expanded-form cache), giving machine-checked proofs of correctness, IND-CCA security (for both the post-quantum and traditional branches), and the LEAK-BIND and HON-BIND binding properties.
 
-This case study motivated much of the new lazy-map random-oracle and group-exponent machinery in the 0.5.0 engine. The [full README](https://github.com/ProofFrog/examples/blob/main/applications/cfrg-hybrid-kems/README.md) documents the modelling choices, the mapping from draft sections to files, and the assumptions each proof relies on (including important caveats about implicit rejection and the absence of a quantum-attacker model).
+This case study motivated much of the lazy-map random-oracle and group-exponent machinery added to the engine in 0.5.0. The [full README](https://github.com/ProofFrog/examples/blob/main/applications/cfrg-hybrid-kems/README.md) documents the modelling choices, the mapping from draft sections to files, and the assumptions each proof relies on (including important caveats about implicit rejection and the absence of a quantum-attacker model).
+
+As of ProofFrog 0.6.0, the case study also carries a **report of its findings** and a **companion document summarizing the advantage bound and assumptions of each of the 57 proofs**, both alongside the rewritten README in the same directory. Every proof now declares a [`bound:` clause]({% link manual/language-reference/proofs.md %}), so `prove` checks the concrete advantage bound the proof claims as well as the sequence of hops.
+
+Ten of those proofs reduce a hop to a statistical fact about reprogramming a random oracle, stated as one of six helper games in [`games/ROM/`](https://github.com/ProofFrog/examples/tree/main/applications/cfrg-hybrid-kems/games/ROM), each carrying a declared `advantage <= ...;` clause. Each of those six games ships with an EasyCrypt proof of the bound it declares (`games/ROM/*.ec`), so the numbers the helper games assert are checked by a second tool rather than taken on trust. These EasyCrypt files are written directly rather than produced by any exporter, and they cover the six helper games only — not the hybrid KEM theorems that use them.
 
 See the [`applications/cfrg-hybrid-kems/`](https://github.com/ProofFrog/examples/tree/main/applications/cfrg-hybrid-kems) directory for all scheme definitions, games, and proofs.
 

index.md

@@ -38,6 +38,7 @@ See the [installation instructions]({% link manual/installation.md %}) for detai
 
 ## Recent updates
 
+- **Jul. 22, 2026: Release of [ProofFrog version 0.6.0](https://github.com/ProofFrog/ProofFrog/releases/tag/v0.6.0)** featuring concrete advantage bounds (the engine now synthesizes the bound a verified proof establishes, and checks a bound the proof claims), a preliminary LaTeX export backend, tuple-destructuring bindings, an Emacs mode for FrogLang, and a substantial wave of soundness fixes to the canonicalization and equivalence layers — anyone relying on a proof checked by 0.5.0 should re-run it under this release
 - **Jun. 7, 2026: Release of [ProofFrog version 0.5.0](https://github.com/ProofFrog/ProofFrog/releases/tag/v0.5.0)** featuring a large new case study (machine-checked proofs of the [CFRG hybrid KEM combiners](https://datatracker.ietf.org/doc/html/draft-irtf-cfrg-hybrid-kems-10) and a Hashed ElGamal KEM), new FrogLang features for random-oracle and group-based proofs (lazy-map random oracles, collection iteration, sampling with exclusions, and a `requires:` block), expanded canonicalization power, and several engine correctness fixes
 - Jun. 7, 2026: Release of [ProofFrog VS Code Extension version 0.1.1](https://marketplace.visualstudio.com/items?itemName=ProofFrog.prooffrog) on VS Code Extension Marketplace
 - **Apr. 16, 2026: Release of [ProofFrog version 0.4.1](https://github.com/ProofFrog/ProofFrog/releases/tag/v0.4.1)** featuring proof engine improvements