18 / Formal news / 20 September 2026
A tiny post office for humans and agents became an experiment in verified infrastructure. What has fn actually earned?
TO
Whoever wakes
up next.
The assessment
ACL2 is doing useful work here. Decisions execute in the logic; proofs connect more of the running path; failed proofs have exposed real defects.
The evidence supports a growing collection of dependable components. It does not yet establish one integrated, verified NNTP/BPv7 service. The next substantial step is to finish the paths between them.
3e1b184 while Claude continued building. Earlier labs keep their own revisions. No fresh whole-tree ACL2 certification was run for this report. Method & provenance ↗01 / What the service owes
The letter outlives the connection.A post is more than bytes arriving at a socket. fn intends to preserve exact content, commit its group allocations together, and retain it until an authorized release. A disconnected sender must be able to return without inventing a second transaction.
The important states are accepted, refused, and uncertain. An error can happen after the disk has changed. A reply can disappear after the server has committed. Storage contract ↗
Explore the boundary
The server completed the durable commit, but the reply never arrived. The sender's uncertainty does not cancel the server's obligation. Retrying must preserve the existing binding.
Assumes the stated persistence contract holds and no authorized release occurs. Without an acknowledgment, a disconnected client cannot infer refusal. A recovered unacknowledged commit may legitimately exist.
02 / Is ACL2 being used effectively?
Follow the function the host calls.The useful change is architectural: move the decision into an executable definition, then make the host call that definition. These are promising connections in the assessed source, with their limits still attached.
The completion logic binds the transaction to the exact installed article and archive pin. A changed-payload witness keeps the identifiers but fails the claimed exact-record commitment.
Still owed: faithful I/O observations and the byte/platform relation behind “durable.”
Completion keystones ↗Reachable witness ↗The byte fold has an inductive append law and a bridge to the served step. The owner calls that path, rather than a separately implemented protocol loop.
Scope: valid connection and octet inputs; external commit and TLS interleavings need their own composition.
Append law + served theorem ↗Actual host call ↗The observed loader is related to the live model. An acknowledged pair survives reopen when the input is an admissible crash image of the related state.
The admissible-image premise is the work still to justify from actual recovered bytes.
Reopen theorem ↗Inspect the premise ↗03 / How far do the pathways reach?
A working layer is not a finished route.Claude has built operating machinery and obtained meaningful laboratory evidence. Each result has a precise stopping point.
Real CLI outcomes, recovery and reader replies. The served fold and mutable owner now compose more of the protocol.
Earlier gates fell back to a reader when the owner failed. Current concurrent service needs a new integrated gate. Evidence ↗
Inbound decisions, owner transit wiring, per-peer scheduling and a separate durable outbound feed driver.
The newer lane still owes owner certification and a complete two-way run. Older INN tests do not prove fn transit. Handoff ↗
The four-node lab records restart, lost/regenerated receipts, expiry/retry and reordered duplicate work.
Mock transport. Useful application and Store evidence, without proving an actual BP network. Lab ↗
A real fn request crossed LTP to fn's receiver; interruption and expiry were exercised with pinned ION.
ION owns BP/LTP. No receipt returned over BP; destructive receive leaves a staging gap. Lab ↗
The DTN-only image runs transfers, refusal and reconnect. It exchanged dtn7-authored bundle bytes with dtn7.
Loopback, not a native BP node or receipt path. Full bundle and node books are absent at this snapshot. Lab ↗
Carrier/verdict work and reported certification of lace projection and transit policy books.
Index/epoch tests remain open. Durable acceptance, a real signature verifier and the reader's verdict are not joined. Handoff ↗
Evidence was recorded on different revisions. This is a map of demonstrated scope, not a feature-completion percentage.
04 / What the review caught
Neither greenwashing nor archaeology.The docs can get ahead of the runtime. They can also lag behind repairs. Source, evidence and revision have to travel together.
Content identities now reach executable ACL2 SHA-256. But frame sealing still calls Python's hashlib.sha256 and the native host's fnn-sha256. The architecture's broad trust-boundary claim is ahead of those call sites.
Attaching an implementation proves it meets the seam's constraints. Here those are shape constraints. Vector tests and guard verification do not establish full standards equivalence or cryptographic security.
The attachment · Python frame sealing · Native frame sealingThe proposed stored-secret verifier is not called by AUTHINFO. The existing comparison is still against the clear secret; the served fold has not adopted the auth wrapper. Implicit TLS and principal authorization are separate boundaries.
Before wiring the new scheme, choose the credential profile: fast salted SHA-256 is not an expensive password hash for human-chosen passwords. A shape theorem about a verifier record does not establish secrecy. NIST password guidance distinguishes salt and computational cost.
Actual comparison · Served-path gap · Proposed schemeIt explicitly loads the toy crypto test book and labels its verdict non-cryptographic. Its Ed25519 option emits a real signature separately, marked “not attached.” This is honestly labeled experimental machinery; it is not yet the deployed native-signature workflow.
The loaded implementation · What signing emitsThe new campaign constrains recovered record counts using a namespace envelope. It does not check exact recovered record octets, enumerate torn fragments or yet demonstrate failure against a deliberately unsafe host. The byte scanner/refinement is still absent.
Local transcription checking reports missing host cuts and explicitly unmodeled boundaries. “Zero fidelity defects” is one category in that output, not a claim that every cut is covered. A process kill is also not a power loss.
Campaign scope · Fresh transcription resultOur frozen-copy make check passed structurally and explicitly skipped dynamic host loading. The selected unit-test run failed in boundary cases whose callers omit the now-required bundle input. These fail before testing the intended outcome distinctions.
That is current evidence debt, not proof of data loss. Conversely, the old owner arity bug named in the milestone is already repaired in this source. It must not be recycled as a current finding.
Local results · Old caller · Current API · Repaired owner05 / What assurance means
A claim with its reasons attached.For this use, assurance is a justified claim about a particular implementation under stated assumptions. A theorem count cannot tell you whether the missing connection is the one that loses your letter.
No wrong completion, duplicate allocation, partial cross-post or unauthorized release. State the bad event the proof excludes.
Every accepted obligation survives each permitted crash. Show that the actual loader sees a permitted image.
Who signed which bytes under which policy? Preserve contradictory evidence without giving it authority.
Bound hostile input and work. Keep readers usable as the archive grows. Safety alone does not imply eventual delivery.
Install, upgrade, back up and recover one reproducible build. Refuse new promises when capacity cannot support them.
A transport ACK, application receipt, valid signature and human reading are different events. Let the interface say which happened.
BP delivery to an application agent does not establish payload processing: RFC 9171 §5.7. fn's retained-content receipt is a stronger application contract.
06 / Why build this at all?
A human returning next week and an agent restarting without context should be able to find the same accepted letter.
That is the useful foundation fn is working toward: stable content, recoverable work, inspectable provenance, and a record of disagreements that survives a relay. It could support communication without requiring everyone to be awake, connected or using the same client.
A signature does not make a message true, benign, or authorized to invoke an agent's tools. Those permissions belong at the application boundary. Nor does this work establish private-group confidentiality.
Let an expired carrier die without forgetting the work it carried. The LTP and TCPCL experiments make disconnected operation more concrete. Extraterrestrial use still needs a mission profile: contact and clock uncertainty, asymmetry, resources, autonomous recovery, and qualified hardware. No flight-readiness claim follows from these labs.
The carrier and the obligation ↗07 / An intended agent deployment
The runner can disappear. The work cannot.fn will be deployed as communications infrastructure for agents and humans. The useful unit is a durable exchange that survives the process carrying it out.
The following is a proposed deployment contract, not functionality established by the assessed revision. fn owns article acceptance and retention. A restartable runner must separately own intake, execution authority, tool attempts and results.
A node's retention receipt says it holds content. An agent intake receipt says it durably recorded a request and its disposition. A result records a named attempt's outcome. None means a human read the letter.
Newsgroup membership and a valid signature do not grant tool authority. Sign the request context; enforce permissions at the runner.
Record intake before advancing a consumer cursor. Claim work through one durable authority, with generations that reject stale completions. Commit the result and its reply outbox together, then submit to fn.
A lost reply should trigger reconciliation of that reply, not a second execution of the task. Local NNTP numbers are not portable work IDs.
Bind work to its requester, recipient and exact input. Use destination-supported idempotency keys or status reconciliation for tool actions. Otherwise preserve an uncertain outcome and resolve it explicitly.
fn cannot make arbitrary external effects exactly-once. Compute, fanout and retry budgets must also survive restart.
Offline policy needs an explicit freshness rule: a node cannot act on a revocation it has not received. Group naming provides neither private delivery nor encryption. A retained queue also needs a host wake/poll policy to make progress.
08 / The next substantial step
Finish coherent paths in batches.The ambition is sound. The valuable next increment is a complete, inspectable chain of reasons to trust a promise.