the thesis
Software for the agentic era
The marginal cost of producing code has collapsed — agents draft it by the thousand lines. What stays scarce is knowing what the code must do, and being able to trust that it does. Everything on this page is built on that belief.
Specify behavior, not implementation
The durable artifact is the specification: the state a system holds, the events it accepts, and what may never happen. Each rule starts as a user story and becomes something checkable — a property test, an executable spec, a theorem.
Make trust mechanical
A model produces plausible code and plausible tests — plausibility is what it is optimized for. So every claim climbs a ladder of evidence: types, tests, property-based tests, executable specifications, formal proofs. Done arrives with evidence attached, or it doesn't arrive.
Run agents like an organization
Written mandates for every delegation. Executable gates that freeze the definition of done before work starts. Independent auditors on different model families reviewing what the builders built: the one who writes the change is never the one who accepts it.
Formalize what must not break
For the kernel of a system — a ledger, a protocol, an identity scheme — invariants that hold in every reachable state, checked by a machine. Refactors that fail loudly instead of silently. Documentation that cannot rot, because it compiles.
selected work
What I'm building
Three threads: KERI — decentralized key management on hash-chained event logs, no blockchain required; wallet, signing, and on-chain data-structure work on Cardano; and infrastructure for running AI coding agents safely and observably.
keri-hs
KERI (Key Event Receipt Infrastructure) library in Haskell
keri-lean
Lean 4 formalization of KERI protocol invariants
keri-purs
KERI-based collective purchasing
aiken-csmt
Compact Sparse Merkle Trie for Aiken — non-hashed keys preserving ordering
air-gap-signer
Blockchain-agnostic air-gapped transaction signer for Raspberry Pi 4
cardano-keri
KERI AID on Cardano — self-certifying identifiers with pre-rotation for on-chain credential anchoring
Cardano Foundation work, hosted in the lambdasistemi org for practicality — lambdasistemi hosts the prototypes; the Foundation receives the released work.
capabilities
How the work gets done
The interests and the capacity behind the repos — the discipline the thesis is held to in practice.
Languages & stacks
Haskell first. Lean 4 for proofs, PureScript in the browser, Aiken on-chain, Rust at the FFI boundary, Nix for everything reproducible.
Formal methods
Protocol invariants formalized in Lean 4 before trusting them — KERI's event-log semantics, and authenticated data structures designed to be proved, not just tested.
Keys & signing
Air-gapped signers, BIP32-Ed25519 derivation, partial multisig signing — key management treated as the product, not an afterthought.
Track record
Self-hosted services running unattended since 2015, and upstream wallet work at Cardano Foundation on cardano-wallet.
running in production
Not demos
Actual services, actual users.
reactivegas
Distributed administration for a solidarity purchasing group (GAS) — prepaid accounts, group ledgers.
Running continuously since 2015 — currently offline while it's rebuilt from scratch on kelgroups.
labottegadiluca
A woodworker's studio site
lambda calculus
Interactive beta-reduction reducer — build an expression, watch it reduce step by step
Running since 2016 — rebuilt on GHC's wasm backend, replacing the retired GHCJS toolchain. source
contact
Get in touch
Open to conversations about identity infrastructure, Cardano, formal methods, and building software with agents — paolo.veronelli@gmail.com.