- Observed velocity: v0.4.0 to v0.7.2 in one day, 80+ Lisp commits.
Bottleneck is human review of Screamer-flagged 5%, not coding.
- Revised: v1.0.0 in 3-5 weeks (~80 cycles, 2-3h human review).
Lisp Machine hardware in 2-4 weeks (~60 cycles, ~4-6h review).
Full Stoa v2.0.0 (editor, browser, shell) in 2-3 weeks.
Total to self-driving Lisp Machine: 8-12 weeks.
- Beyond bootstrap: system writes Stoa (~150K lines), Agora (~100K),
hardware VHDL (~50K). Human only writes design decisions and
reviews the 5% edge cases Screamer flags.
- The triad replaces every layer of computing: cognition, environment,
network — one gate stack, one prover, no cloud, no gatekeeper,
no per-token fee. A complete alternative infrastructure that
the system writes itself, one ACL2-verified submission at a time.
- Passepartout IS the PDS — memory-object (SHA-256 hash) maps
directly to Agora Note (CIDv1). Gate stack verifies every note.
- Stoa: Lish editor + Nyxt browser + Lish shell in one Lisp image.
v2.0.0→v6.0.0: Qt/WebKit erosion to pure-Lisp browser, tagged
RISC-V hardware, world models.
- Agora: self-sovereign DID, DIDComm, Note primitives, Relay Network,
compute marketplace, contracts, liquid democracy.
- The triad replaces every layer of the modern computing stack:
cognition, environment, network, app model, compute, identity,
commerce — all built on one gate stack, one memory model, one prover.
- Agora implementation is a separate body of work comparable to
Passepartout itself.
- Current Passepartout: ~10,700 lines, 2 months one dev
- To v1.0.0: +4,500 lines, 4-6 months
- Lisp Machine hardware integration: +6,000 lines, 3-6 months
- Total: ~21,000 lines, 9-14 months one dev, 5-7 months team of 2-3
- Why small: Lisp is 3-10x denser, primitives are reused across
domains, ACL2 proofs replace test fixtures, LLM generates boilerplate
- Comparison: Hermes ~50K, Claude Code ~100K, Llama.cpp ~200K
- Not a moonshot. A well-scoped engineering project.
- Every subdomain for bootstrapping the Lisp Machine is software:
RISC-V ISA, SBCL runtime, ACL2 logic, CIC type theory, compiler
optimization, device drivers. Every one flips.
- Fastest sequence: Day 1 ingestion (LLM + human review), Day 1-2
profiling (benchmark sweep), Day 2-3 active probing (synthetic
microcode routines), Day 3-7 transfer + sufficiency (ACL2 verifies
new dispatch routines, zero LLM tokens)
- Result: self-driving Lisp Machine in under a month with one
human review session and a Tenstorrent P150
- Sufficiency flip is per-domain, not global. Poetry never flips.
- Three knowledge types: structural (published rules), empirical
(observations), performance (profiling data)
- Fastest acquisition: active sandboxed probing, contrastive queries
to human (not waiting for HITL to accumulate), ontology transfer
from related domains, benchmark harness
- Codified domain: flip within days (hours LLM + hours expert review)
- Uncodified learnable domain: flip within weeks (probe + real use)
- Never-flip domains: system is honest, LLM handles 100%
- LLM proposes code at every bootstrap stage (microcode, CIC kernel,
macro layers, gate rules) — symbolic engine verifies before accepting
- Weak model = more retries (5-15), strong model = fewer (1-3)
Both produce 100% verified output because the symbolic engine catches
all mistakes
- The critical transition: not better LLMs, but the sufficiency flip
applied to hardware. Once enough facts about runtime behavior
accumulate, the system proposes microcode optimizations with zero
LLM tokens.
- Surprise result: a barely competent LLM is sufficient for the full
bootstrapping chain. It's slower and costs more in API calls, but
reaches the same destination.
- ACL2 proves semantic equivalence for Passepartout's own Lisp code
today; for other languages via logical specification modeling
- CIC prover (future) extends to dependent-type-level equivalence
across language boundaries
- Self-driving threshold: when system can synthesize and load its
own FPGA microcode or RISC-V dispatch from within the running image
- Tenstorrent P150 (72 RISC-V cores) is particularly interesting:
microcode is RISC-V software, not FPGA hardware — system writes,
compiles, loads, benchmarks its own core dispatch logic
Six-stage workflow: codebase ingestion (AST as facts), goal translation
(LLM, 10%), Screamer constraint satisfaction (80%), ACL2 plan verification,
incremental execution with Merkle snapshots per step and rollback on test
failure, final re-verification.
Key limit: ACL2 cannot prove semantic equivalence of arbitrary programs.
Gap filled by: tests as empirical verification, API contract checking
(structural equivalence of public interfaces), human review with full
provenance of semantic changes.
Comparison with Claude Code: Passepartout trades higher up-front planning
overhead for zero-token constraint checks, ACL2-verified scope control,
instant per-step rollback, and a Merkle chain from before to after.
Three distribution tiers: code-only (AGPL), code+knowledge (commercial
data package), code+knowledge+hardware (verification appliance).
The upgrade challenge: instances diverge in both code and knowledge.
A 'git pull' breaks because new code expects fact structures the old
store doesn't have. Solved by:
- Ontology versioning flags old facts for re-verification
- Degradation to fallback mode, not crash
- Reversible upgrades via Merkle snapshots
- Delta distribution (diffs against current ontology version)
- Per-instance verified migration (run new code against old facts in
sandbox; ACL2 reports compatibility; operator reviews only failures)
Business model: code free, migration scripts subscription, domain
knowledge packages subscription, firmware bundled with hardware.
- 1980s: memory K/MB, 1-10MHz CPUs, simple software, testing-sufficient.
C fit in 64KB; Lisp needed 40MB and GC cycles. The market chose throughput.
- Today: memory and transistors are free (billions on an ARM core).
Software is too complex for testing alone. Cost of failure > cost of
verification.
- Inversion: 1980s said correctness is a luxury. 2020s says correctness
is the only affordable option.
- Passepartout exploits this: verification appliance for K/year replaces
00K/year in compliance failures.
- The historical fork: C won on economics, not merit — RISC/commodity PC
ecosystem optimized for C, not for Lisp
- Passepartout's reversal path: verification appliance vertical → FPGA
Lisp μcode → custom ASIC economics
- Lisp for embedded: compile-to-C (ECL, PreScheme), tiny Lisps (uLisp,
FemtoLisp), Lisp-as-macro-generator for C
- Microbiology as Lisp: DNA homoiconicity, hot-reloadable image, auto GC,
interpreted execution, self-modifying source, duck typing, concurrent
real-time GC (apoptosis)
- Biology proves the Lisp model is efficient at planetary scale
