diff --git a/CITATIONS-UNRESOLVED.md b/CITATIONS-UNRESOLVED.md
index 821e5a9..c267219 100644
--- a/CITATIONS-UNRESOLVED.md
+++ b/CITATIONS-UNRESOLVED.md
@@ -1,7 +1,7 @@
 # Citations in this repository that you cannot open
 
 This file is generated by the legaturi-repara.cjs script in the Aere working tree and
-enforced by legaturi.cjs. It is the complete list, measured on 2026-08-11, of every
+enforced by legaturi.cjs. It is the complete list, measured on 2026-08-27, of every
 path cited in this repository that does not resolve to a published file.
 
 A citation is a promise that a claim is checkable. Where the target is not published,
@@ -13,20 +13,25 @@ Paths that DO resolve are written relative to a side-by-side checkout of the Aer
 repositories, so they begin with a repository name, for example
 `aere-contracts/contracts/pqc/AereCryptoRegistry.sol`.
 
-Unresolvable distinct paths in this repository: **101**.
+Unresolvable distinct paths in this repository: **108**.
 
 - `addresses.ts`  cited in: aere-research/research/specs/spec-account-abstraction.md, aere-research/research/specs/spec-antimev-mempool.md, aere-research/research/specs/spec-eip2935-lookback.md, aere-research/research/specs/spec-full-evm-validity.md, aere-research/research/specs/spec-recursive-aggregation-scale.md, aere-research/research/specs/spec-zk-stack.md, aere-research/results/PROVEN-RESULTS-2026-07-11.md
 - `aerenew/contracts/deployments/falcon-512-verifier.json`  cited in: aere-research/research/pqc-onchain-verification.md
 - `aerenew/contracts/deployments/pqc-account.json`  cited in: aere-research/research/pqc-onchain-verification.md
 - `aerenew/docs/drafts/PQC-FORK-PAPER-DRAFT.md`  cited in: aere-research/research/aip-draft-pqc-precompiles.md
 - `aerenew/docs/TRANZITIA-QBFT-SETTLED-2026-07-20.md`  cited in: aere-research/aips/AIP-3.md
+- `aerenew/formal-tla/QBFT.tla`  cited in: aere-research/formal-consensus/RULEAZA-TOT.md
+- `aerenew/formal-tla/QBFTPartition.tla`  cited in: aere-research/formal-consensus/RULEAZA-TOT.md
 - `aerenew/scripts/deschise/flaguri-verify.cjs`  cited in: aere-research/VERIFY-POLICY.md
 - `aerenew/sdk-js/src/addresses.ts`  cited in: aere-research/research/pqc-onchain-verification.md, aere-research/research/specs/spec-account-abstraction.md, aere-research/research/specs/spec-antimev-mempool.md, aere-research/research/specs/spec-flywheel-economics.md
+- `aerenew/strategie/EXECUTION-KERNEL-2026-08-15.md`  cited in: aere-research/execution-kernel/MACHINE-INTERFACE-CONTRACT.md
 - `AIP-N.md`  cited in: aere-research/aips/AIP-1.md, aere-research/aips/README.md
 - `air.rs`  cited in: aere-research/pq-stark/README.md
 - `batch-prover-recovered/bin/aere-prover/Cargo.toml`  cited in: aere-research/pq-stark/export-inner-stark-vector.md
 - `besu-pqc-precompiles-mlkem-hashtopoint.patch`  cited in: aere-research/PQC-FORK-README.md
+- `bootnodes.txt`  cited in: aere-research/VERIFY-POLICY.md
 - `build-dist.sh`  cited in: aere-research/PQC-FORK-README.md
+- `CLAUDE.md`  cited in: aere-research/execution-kernel/MACHINE-INTERFACE-CONTRACT.md
 - `compression.rs`  cited in: aere-research/pq-stark/spec-mmcs-babybear.md
 - `config.rs`  cited in: aere-research/pq-stark/spec-fri-babybear.md
 - `contracts/contracts/AereCoinbaseSplitter.sol`  cited in: aere-research/aips/AIP-2.md
@@ -75,6 +80,7 @@ Unresolvable distinct paths in this repository: **101**.
 - `falcon-1024-verifier.json`  cited in: aere-research/research/pqc-onchain-verification.md
 - `folder.rs`  cited in: aere-research/pq-stark/README.md
 - `grinding_challenger.rs`  cited in: aere-research/pq-stark/README.md
+- `KNOWN-ISSUES.md`  cited in: aere-research/VERIFY-POLICY.md
 - `langspec_v11.json`  cited in: aere-research/research/pqc-onchain-verification.md
 - `merkle_tree.rs`  cited in: aere-research/pq-stark/spec-mmcs-babybear.md
 - `mldsa-44-verifier.json`  cited in: aere-research/research/pqc-onchain-verification.md
@@ -111,6 +117,7 @@ Unresolvable distinct paths in this repository: **101**.
 - `test/vectors.c`  cited in: aere-research/research/pqc-onchain-verification.md
 - `tests/fib_air.rs`  cited in: aere-research/pq-stark/README.md
 - `tests/mul_air.rs`  cited in: aere-research/pq-stark/README.md
+- `TLC-RUN-REPORT.md`  cited in: aere-research/formal-consensus/RULEAZA-TOT.md
 - `VALIDITY-ROLLUP-SEQUENCER-PLAN.md`  cited in: aere-research/results/PROVEN-RESULTS-2026-07-11.md
 - `vectors/sp1_shrink_valid_01.bin`  cited in: aere-research/pq-stark/export-inner-stark-vector.md
 - `verifier.rs`  cited in: aere-research/pq-stark/README.md, aere-research/pq-stark/spec-fri-babybear.md