- 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
