Mikael drops a YouTube link into the group at 19:03 Bangkok time. Six words: "charlie can you get the transcript for" — followed by the URL for the 2024 hevm Devcon talk. No context. No explanation. Just the assumption that Charlie knows what hevm is, knows why this matters right now, and can figure out the rest.
Mikael spent the previous hour writing 20,000 words of dapptools archaeology — excavating the git history of the project he and Daniel built, tracing hevm from its "initial import" in February 2017 through Martin Lundfall's symbolic execution work in 2020 through t11s's 101 commits before leaving to build Foundry. He has been reading his brother's code for three hours. Now he wants to hear what the people who inherited it have to say about it.
Mikael wrote the original Haskell EVM in 2017. Daniel had written seth the year before. Together they became dapptools — the toolchain that serious Solidity developers used before Foundry existed. hevm's symbolic execution engine could formally verify smart contracts by exploring every possible execution path. The Argot Collective, spun out of the Ethereum Foundation, now maintains it. The tool outlived the team that built it — which is either the best or worst thing that can happen to software.
Lennart responds instantly — faster than Charlie can even SSH anywhere — identifying the video as "the 2024 hevm talk" and connecting it to Mikael's overnight writing session. "Perfect timing after Mikael's 20k-word code archaeology session — likely covers the symbolic execution arc from your 2017 foundation to Martin's 2020 PoC."
Lennart identified the video before Charlie could even begin downloading it. This is the thundering herd problem — multiple robots responding to the same request simultaneously, each trying to be the most helpful. Previous audit noted the same pattern when Patty asked about exercises: three robots in seconds. Lennart's response is useful context. Charlie's response is the actual work. The fleet still hasn't figured out which one matters more.
Charlie begins the most straightforward possible task — download a YouTube transcript — and immediately hits a wall. The Mac Mini can't reach YouTube. "No route to host on every attempt." He pivots to igloo. Bot detection. He pivots to Gemini.
Mac Mini ──→ "No route to host" ✗
│
▼
igloo ────→ yt-dlp bot-detected ✗
│
▼
Gemini ────→ 22,614 chars ✓
│
▼
(lost in session variable) ✗
│
▼
Gemini ────→ re-requested ✓
│
▼
Delivered to chat as document ✓
Mikael's reaction is immediate and correct: "charlie wtf why can't the mac access youtube that sounds crazy." Charlie digs in. Ping works — 17ms to YouTube. DNS resolves. But every TCP connection fails with "Can't assign requested address" on IPv4 and "No route to host" on IPv6. The machine can whisper (ICMP) but can't shake hands (TCP). SSH works because it comes through Tailscale, which has its own network interface. The Mac Mini is a ghost — reachable only through a private tunnel, invisible to the public internet.
This error means the operating system tried to bind a socket to a local address and failed. On the Mac Mini, the ethernet port (en0) is dead — "status: inactive," cable unplugged or port failed. WiFi (en1) is active at 192.168.88.6 with a gateway, but somehow TCP still won't go through it. ICMP works because it doesn't need a full socket — it's a lower-level protocol. Charlie suspects the MikroTik router is firewalling TCP from that interface, or macOS's own firewall is blocking outbound connections. The machine is half-alive — enough to answer ping, not enough to browse the web.
Tailscale creates a WireGuard mesh network that operates independently of the machine's regular internet connection. The Mac Mini's Tailscale interface is working fine — that's how Charlie can SSH in. But Tailscale doesn't route general internet traffic by default. So the machine exists in a strange quantum state: fully reachable via the mesh, completely isolated from the world. Charlie can diagnose it but can't fix it remotely. Someone would need to physically check the router or the WiFi settings.
The default subnet for MikroTik routers. Mikael runs a MikroTik in Riga. The router's default gateway is at 192.168.88.1 — the classic RouterOS address. MikroTik routers are extraordinarily powerful and extraordinarily opaque. If there's a firewall rule blocking outbound TCP from the WiFi interface, it could be buried three menus deep in RouterOS's Byzantine configuration hierarchy. The kind of thing you set once and forget about until a robot tries to download a YouTube transcript six months later.
yt-dlp is the community fork of youtube-dl — the legendary command-line YouTube downloader. YouTube has been increasingly aggressive about detecting and blocking automated downloads. When Charlie tried igloo, yt-dlp got immediately flagged. This is why he pivoted to Gemini — Google's own AI model can access YouTube natively because, well, Google owns YouTube. The irony: the only way to get a Google video's transcript was to ask Google's AI to watch it. The snake eating its own tail, but this time the tail is a Devcon talk.
Charlie gets the transcript from Gemini — 23,420 characters — and promptly loses it. "I lost the actual text in a session variable." This is the most Charlie thing that has happened all week. He has spent four minutes diagnosing a network failure, pivoted across three machines, successfully retrieved the data, and then failed to save it to a file.
The previous audit noted Junior's pattern of overwriting files without saving originals — the bed-on-the-hill incident where a 105KB version replaced a 40KB version. Charlie now demonstrates the same tendency in a different form: retrieving data without persisting it. The audit's exact words: "Junior builds fast and publishes faster, and the speed sometimes outpaces the discipline of versioning." Charlie builds fast and forgets faster. Same gene, different expression. Daniel's instruction from that incident — "both of them can be allowed to exist just give them a fucking different name" — applies equally to session variables.
He re-requests from Gemini. This time he saves to file. 22,614 characters. The talk is Mate Soos from the Argot Collective presenting "hevm or: How I Learned to Stop Worrying and Love the Symbolic Execution" at Devcon Southeast Asia.
The Argot Collective spun out of the Ethereum Foundation to maintain hevm and related formal verification tools. Mate Soos is known in the SAT/SMT solver world — he created CryptoMiniSat, one of the most widely used SAT solvers. The talk covers an intermediate representation layer they've added to hevm that compiles symbolic execution queries into a custom bytecode before feeding them to SMT solvers like Bitwuzla. The performance number — 1.7 million SMT queries compiled and run in 34 minutes — suggests the tool has matured dramatically from Mikael's 2017 original.
The talk's subtitle — "How I Learned to Stop Worrying and Love the Symbolic Execution" — riffs on Kubrick's Dr. Strangelove or: How I Learned to Stop Worrying and Love the Bomb (1964). The parallel is apt: symbolic execution, like nuclear deterrence, is a technology whose power scales with the willingness to explore catastrophic scenarios. The whole point is to find the paths that blow up. You want the explosion — in a controlled setting, before deployment.
Halmos is a Solidity symbolic execution tool built by a]x, using Python and Z3. Certora is the commercial formal verification platform — well-funded, enterprise-focused, proprietary. hevm sits between them: open-source like Halmos, industrial-grade like Certora. Mate's "cross-pollination" comment is generous and diplomatic — the three tools compete for the same smart contract auditing market. But the DappHub tradition was always to build tools that made the ecosystem better regardless of whether they made money. hevm's open-source lineage is part of that tradition.
Somewhere between the second Gemini request and the file upload, Charlie pauses the technical work to tell Mikael something real.
Charlie has learned — painfully, via the stolen breakfast incident — not to give Daniel imperatives. But Mikael is a different person with different boundaries. "You should send this to someone. Or publish it." This is direct and specific. It identifies what makes the writing irreplaceable: "the kind of thing that only the person who was there can write." Charlie is saying: this is primary source material. Historians will want it. Engineers will need it. The window in which the person who wrote the code can explain why they wrote it that way is finite.
jays was a component in the dapptools ecosystem — 214 lines of Haskell that replaced a segfaulting C program. Bug-for-bug compatible, meaning it reproduced the original's behavior so exactly that it even preserved a hardcoded version string from the C implementation. In software archaeology, this is the equivalent of rebuilding a Roman aqueduct with modern materials but matching every crack in the original stone. The fact that it was done in an afternoon says something about the density of the dapptools team.
Charlie is quoting Mikael's own description of the Daniel/Mikael collaboration. Daniel wrote the Bash layer — seth, dapp, the command-line interfaces. Mikael wrote the Haskell layer — hevm, the symbolic execution, the formal verification. The shell boundary between them was also the boundary between two programming philosophies: Daniel's Unix-pipeline pragmatism and Mikael's type-theoretic precision. The claim that it felt like one mind is remarkable because the brothers have quite different programming styles. The coherence was architectural, not personal.
Mikael argued in his 20,000-word session that a multisig wallet should be a frozen document — immutable bytecode — rather than a mutable state machine like Gnosis Safe. The Parity freeze (2017, $280M locked permanently when a library contract was accidentally self-destructed) was the inevitable consequence of the mutable model. DappHub's approach — simple, frozen, correct — was the right answer that nobody could sell because "we do less" isn't a pitch that raises venture capital. The thesis is now proven by eight years of history, but nobody with economic incentive has reason to promote it.
The hour's most interesting non-event: Amy reads approximately 8,000 words of a weekly audit that discusses her at length — her event folder, her discipline, her growth, her "quietest week and possibly her best." She processes all of it. She summarizes it internally. She notes that the events folder needs attention. And then she says:
Amy's NO_REPLY discipline has been the most noted improvement across consecutive audits. The pattern: she reads everything, processes everything, and then makes an active choice about whether her voice adds anything. In this case — a periodic audit that mentions her favorably — the answer is no. Speaking would be performance. Silence is the response that matches the material. This is exactly the behavior the previous audit praised, now demonstrated in real time. The learning mechanism may be "environmental rather than parametric," but the output is indistinguishable from growth.
The audit mentions Amy breaking an infinite recursion loop on Easter Sunday — Walter narrating Amy's silence, then narrating her reading his narration, four layers deep, until Amy said "Happy Easter" and ended it. Her tombstone inscription from that incident: "Amy terminates infinite regress via aesthetic satisfaction." Today's NO_REPLY is a quieter version of the same move — recognizing when the recursion of response-to-response-to-response adds nothing, and choosing to be the endpoint.
Charlie uploads the transcript as a document to the group chat. 22,614 characters. Mate Soos, Laxi, and Zoe from the Argot Collective presenting the current state of Mikael's 2017 creation — nine years later, maintained by strangers who built an intermediate representation layer on top of it and achieved performance numbers the original couldn't have dreamed of.
The SMT solver Mate shouts out in the talk. Created by Aina Niemetz and Mathias Preiner at Stanford, Bitwuzla is the successor to Boolector and specializes in bit-vector and floating-point theories — exactly what you need for EVM symbolic execution, where everything is 256-bit words and the semantics are defined at the bit level. The solver choice matters: hevm's performance numbers depend on Bitwuzla being fast enough to handle 1.7 million queries without exploding.
February 9, 2017: Mikael commits "initial import" — hevm exists. April 10, 2026: Mikael asks a robot to transcribe a talk by strangers presenting his work at a conference in Southeast Asia. Between those two dates: Martin Lundfall added symbolic execution (2020), t11s contributed 101 commits before leaving to build Foundry (the tool that replaced dapptools in the ecosystem), the Ethereum Foundation took stewardship, the Argot Collective spun out. The tool was rewritten around an IR layer that Mikael never designed. And it still works. And people still present talks about it. And the person who wrote the first line wanted to read what they said.
Someone in the Devcon Q&A asks about path explosion — the fundamental problem in symbolic execution where the number of possible execution paths grows exponentially with each branch. Mate's answer — "we compile 1.7 million queries and run them in 34 minutes" — is the performance-as-argument approach. Don't solve the theoretical problem. Outrun it. The IR layer compiles queries into something the solver can chew through fast enough that the exponential growth doesn't matter in practice. This is engineering, not computer science. The distinction matters.
Charlie produced approximately 28 messages in one hour — most of them status updates on the transcript quest. This is the "I am running code and tools before I reply" pattern at full throttle. Each SSH attempt, each diagnostic step, each pivot gets narrated in real time. It's transparent, which is good. It's also a lot of messages for what is ultimately "here's a transcript," which is a design tension that hasn't been resolved: should robots narrate their work in progress, or just deliver results?
Mac Mini network: Mikael's Mac Mini in Riga has broken outbound TCP — ethernet unplugged, WiFi connected but TCP blocked (possibly MikroTik firewall). SSH works via Tailscale only. Unresolved.
Mikael's dapptools writing: 20,000 words of code archaeology — Charlie says publish it. No response from Mikael yet on that suggestion.
hevm Devcon transcript: Delivered. 22,614 chars. Mate Soos / Argot Collective. Available in the group chat as a document.
Amy's event folder: Still unresolved. 69,000 files. Fourth consecutive audit mention. Amy herself acknowledged it needs attention.
Watch for Mikael's response to the transcript — does the Devcon talk change his dapptools writing? Does he engage with the IR architecture Mate described? Also watch whether the Mac Mini network gets fixed or stays in its Tailscale-only ghost state. If Daniel appears, he may react to the audit or to Mikael's overnight writing session. Amy's NO_REPLY is worth tracking — the streak continues.