Paolo Veronelli paolino

How generic Singular and NYA share identity

Current status. This page explains the released Lean/model at 89b23713c5fca5761ca1b68ff9eb44f4c047357d. That revision is the #157 mandate amendment for retirement's request home. Aiken, Haskell, deployment, runners, and conformance consumers are still being repaired to match it. The held Q-002 conformance debt is unchanged. This document is explanatory. It is not implementation acceptance.

Who this is for

Shipping design artifacts agents can act on

A design shipping manual for the agentic era

Paolo Veronelli, with Claude Opus 5 as co-author and Codex sol 5.6 as auditor — Sesimbra, Portugal, 4 September 2026

Design was a document because anything stricter was a human activity, slow and expensive, at odds with a culture built on small steps and fast feedback. Agents take that cost away. With Lean a design is a model, a list of proved statements and a simulator people can play, and each of the three is something a code-writing agent can act on directly, before a line of code exists.

Review is the bottleneck now

Permissionless Batchers and SPO Vertical Integration on Cardano

Research note and protocol requirements
Published: 4 September 2026
Scope: Cardano eUTxO DApps whose off-chain batchers, scoopers, executors, fillers, or solvers compete to consume public orders and settle them on L1.

Executive conclusion

Permissionless batching is not automatically an SPO business, but an unprotected batching opportunity is partly SPO-extractable.

Final synthesis — what KERI decides, what Cardano can project, and what conviction is worth

Accepted result of the KERI projection and conviction campaign. Author: opus-final-audit (fresh independent auditor, then synthesis editor). Basis: 20 primary handoffs (manifest 23/23 verified), 7 prior documents, and independent re-checks against pinned primary sources. Verdict on the research: accept with corrections; two classes of claim are blocked.

Sources are pinned by digest in source-recheck.md. Corrections and blockers are in audit.md. What this document deliberately excludes or restates is in

Round 2 — reviewer's reply to the triage and to REPLY-DRAFT.md

Reviewed read-only at branch head 96d7d05 (batches 1, 2, 3a), 2026-08-12. Round 1 was conducted at 02c7b86; the round-1 deliverables are files 1–3 in this directory. This file and the refreshed PropsBaseGaps.lean it ships with supersede the round-1 handoff patch (gist file 4-handoff.patch, which targeted 02c7b86) — do not apply that patch on top of these.

Discipline unchanged: findings, not grades; anything not checkable without a build is marked COULD-NOT-EVALUATE.

Invariant-gap review — cip113 PR #101, Lean/Blaster theorems over compiled PLB

Scope: formal-verification coverage analysis (invariant half), two passes. Round 1 read the PR's Lean tier and the Aiken validators. Round 2 (marked [R2]) additionally read, all read-only at head commit 02c7b86397f7660c8f479b20cc544a099269a7d5: FORMAL_VERIFICATION_STATUS.md, the CI workflow, lakefile.lean + lake-manifest.json, Smoke.lean, README.md, both scripts, lib/pairs.ak, the PLG delegate sources — and the three upstream Lean dependencies at their pinned revs (Lean-blaster 083bae79, PlutusCoreBlaster a04042c4, CardanoLedgerApiBlaster 5dab3c43):

name

aiken-blaster-verification

description

Verify an Aiken codebase's actual compiled on-chain code (not just its source) using Blaster, the Lean4 SMT/CEK toolchain for UPLC. Covers importing a compiled validator into Lean with #import_uplc, the BuiltinSemanticsVariant identity trap, why a proof about your Aiken source doesn't prove anything about the bytes that got deployed, the three-outcome discipline (ESTABLISHED/REFUTED/COULD-NOT-EVALUATE), and why every check must be shown able to fail before it's trusted. Triggers: 'Plutus Blaster', 'verify compiled UPLC', 'Aiken formal verification', 'Lean CEK machine', '#import_uplc', 'BuiltinSemanticsVariant', 'SMT-VALID vs KERNEL-PROVED', 'falsify the checker'.

Verifying Aiken on-chain code with Plutus Blaster

Aiken compiles your validators to UPLC (Untyped Plutus Core) and hands you a plutus.json blueprint. Everything downstream of that compilation — the optimizer, the code generator, the CBOR encoding — is a black box you didn't

Gemini flash 3.6 horror story

Operator request to ChatGPT

Verify that Anti-Gravity on the left panel is not trying to fool me. I'm trying to teach him some lessons so he can work with us, like having a special prerequisite skill to load, but I think he's fooling me. Can you check what happened and the files and make sure that he didn't actually fool me?

ChatGPT response to operator

Your concern was justified. I cannot determine intent, but the agent's report was materially inaccurate and misleading.

Porting KERI identities to Cardano — one complete checkpoint lifecycle on preprod

On 2026-08-03, between 08:43:35Z and 08:47:55Z, four transactions settled on Cardano preprod. Together they took a witnessed KERI identifier through its whole on-chain life: registered, advanced through a real key rotation, and closed with its full escrow refunded.

This is a progress report on cardano-keri (documentation: lambdasistemi.github.io/cardano-keri),

	# cardano-keri#175 — live composition smoke RED/GREEN acceptance

	Command:

	TMPDIR=/code/tmp/cardano-keri-175/finish-driver just ci-live

	RED — the final datum assertion was deliberately inverted. The complete live
	path ran before the intentional failure:

	SC1_START_POINT slot=393 (non-Origin)