Hacker Newsnew | past | comments | ask | show | jobs | submit | jswny's commentslogin

Does anyone do TLA style distributed systems verification with Lean? Curious the experience there and how well supported it is


Check out https://veil.dev/

There's a blog post with a demo at https://proofsandintuitions.net/2026/02/09/distributed-verif...

It's still early days, but we're committed to making distributed protocol verification work extremely well in Lean.


Unfortunately I’ve used Claude and GPT models for a long time in a variety of harnesses and I agree with you and I think it’s the compaction.

For some reason, codex compaction is like black magic. I’ve never felt like I can just one one continuous thread with other models, Claude I carefully curate when I compact


Compacting at all is a mistake. With 1m context window there is no reason for a single task to require compaction.

Much better to spend tokens breaking the task into chunks, documenting and storing them durably, then executing each one in clean context and just /clear after.

It’s a similar concept to compaction, just planned in advance. Much much more effective, and doesn’t burn tokens and time (“wall-clock”, Claude) doing the compaction.


> With 1m context window there is no reason for a single task to require compaction

Only if money is no object. Cache reads are cheap (10% of uncached input costs) but definitely not free, and cached reads dominate session costs at long context lengths. A prompt at 20k context with $0.01 in cached reads would cost $0.40 in cached reads at 800k context, that quickly adds up for long sessions.


I’m not following the implication that these economics argue for jsing compaction instead of just clearing context?


Your 'with 1m context window' implied that some manually-curated task 'chunks' would overflow smaller context windows (eg 200-400k tokens). If you're instead curating chunks small enough to avoid getting burned on long-context cache-read costs, you're not using a 1m context window at all. At that point, compaction is a convenience over manually chunking and clearing context for fine-grained bits of work.

I think the stronger claim is: there is no reason for a single task to require a 1m context window.


Most models’ reasoning abilities drops off significantly between the 256K-1M token ranges of the context window. There’s too much stuff to “pay attention to” at once.


I auto compact around 200k tokens both due to this and because the cached read cost really escalates when sessions have more tokens than that (too short and you pay a lot in per-compact re-reading of state)


Agree. Another consideration is that input token costs are effectively quadratic with the number of conversation turns. The minute you get into a long conversation you can see the costs shoot up.

You can get far more gas out of even a $20 plan of you’re careful to break things up into relatively small discrete steps, clear context regularly and give the model plenty of information to work with.

My workflow for bigger features is to write out a plan document and then proceed in smaller implementation steps, reviewing as I go. If I find something odd, I ask the agent why and often that leads to discovering a new dimension to the problem, which in turn is an opportunity to adjust the approach.


You just haven’t worked on tasks that are complicated enough. Occasionally it took more than 1M tokens just to come up with a plausible plan.

Personally I find using /rewind judiciously is better than using /compact. The latter essentially gives you no control of what details to discard, but the former at least has coarse-grained control.


Oh my goodness. I’ve used over 1B tokens on a single feature. I’m running at about 25B tokens/month right now.

My whole point was that by planning in advance you can shard the work into manageable sections with clear beginnings and outputs with acceptance croteria, and never compact, or even use more than a few hundfed thousand tokens in context.

It’s all hierarchical. Looking at an eval feature building right now, it’s 20ish build plans, each with zero to five or so /clear moments.

But maybe that’s the key thing… I don’t iteratively prompt ad hoc software writing. I do iterate on requirements, but if those are solid enough there is no “now write this function, now write that module”.


Have you ever looked at how much performance drops as context grows? The difference in intelligence between 100k and 1M is huge, like opus drops to haiku level performance, or worse. For that reason I try to keep under 200k. That feels about the upper bound for tasks requiring accuracy.


This is the way.


One interesting harness thing I saw Cursor do is to give the model access to the entire thread.

Even if it doesn't fit in the context window, the model can search through past turns and sanity check if something doesn't seem to be going right, or be prompted to follow an early message, "when starting on a new item, review the first message for how we should approach this"


Unlike other model/harness pairs, codex+gpt also passes an opaque encrypted artifact speculated to be an embedding representing the conversation back to the successor generation which is “denser” or at least higher fidelity than summarized text.


That's wild to read considering Codex's compaction to me feels like the model becoming demented. Super aggressive, throws away almost everything.


This is not an issue with Claude, but with Claude Code.

With swival.dev you can use long sessions without ever doing any manual compaction or reset, even with Claude models.


Pretty much, I stopped using Claude for that reason, I shouldn't have to keep track of the context of the model all the time. And god forbid I don't, the amount of time I've lost to Claude just sending it and then lying is not worth it when 5.5 will just do stuff, compact 2-3 times in the task and still not go insane.

This whole 1 million context window is a lie after 300k Claude degrades to unusable, and compact doesnt help. I've had Codex tabs open for weeks, I have to regularly restart Claude.


I agree with some of Kelley’s takes, but the issue is the tone.

Does anyone think that if Bun had been rewritten from Rust to Zig that a member of the Rust core team would have written a personal hit piece against Sumner (while pretending it isn’t a hit piece)? Probably not.

Kelley can write what he wants, but as the BDFL of a rising programming language, people are allowed to react if they don’t agree with the public image being portrayed by Zig.


What’s the advantage of that for building?


sandboxing, which feels a weird way to achieve that. Although the reason for it to begin with is because builds systems can typically access raw memory and disable artificial restrictions.

I think this is a bad move since the real fix to these attacks is a sandboxed environment rather than a single tool implementing sandboxing.


These are not mutually exclusive, and one makes the other better. "Whole process" sandboxing has always been far worse than native sandboxing because when the devs writing the software design the software to be sandboxed they can achieve far more fine grained permissions. Similarly, "whole environment" sandboxes are the absolute worst - they're the least fine grained possible.

The benefit of "whole environment" is that if you stuff everything into that environment then anything in it is confined, but it's all confined with everything stuffed in and is sort of maximally capable. You can rarely do things are significant as, say, system call filtering, because all software in the environment must continue to work and none of it was designed with that in mind.

Native sandboxing like this will likely make auditing much easier as well. If a dependency requires something like "give me the ability to execute code on the OS", now it has to ask for it and now it gets additional scrutiny.

Native sandboxing is and always will be the infinitely superior method when it's actually used. Whole process/ Environment is only what we use because of how rare native sandboxing is.


How would you do it, then? Sandboxing a project's build.zig via Wasm (and the various dependencies's build.zig files) seems like a great improvement to me and is how I would personally try to sandbox the build process.


I don't know what build.zig commonly does, but in Rust build.rs often does things like compiling C/C++ libraries, so you can't sandbox it with WASM (contrary to proc macros, which most of the times can be compiled to WASM and there were/are efforts for that). How does Zig fare with that?


Even if they end up with a "this dependency can execute arbitrary code" it'll be a huge win because that will be an explicit grant to that dependency. You'll be able to know "which of my dependencies execute arbitrary code?" and encourage most of them not to. In rust, you can know this but it's going to be "basically all of my dependencies can do it" because somewhere they'll use a build script/ proc macro.

I don't know Zig's plan, but once you have the ability to broker privileges like this you have the ability to audit the privileges being brokered and things change forever.


I assume the compiler(s) do not run in WASM. Just the build script. The build script just orchestrates the compilers. So you can run any compiler that the build script is given access to, so compiling C/C++ or potentially any other language shouldn’t be an issue.

In theory, you could run the whole compiler (including C) in WASM as well but I don’t think that’s the goal? You kinda need to trust the compiler itself.


If the build script can execute arbitrary processes, the entire security is lost.


Use containerized development systems: bwrap (my favorite), devcontainers.json, isolated server, anything really. You can't protect yourself against malicious vscode extensions with a zig build system sandbox.


It makes more sense when you view sandboxing as enabling project correctness in the presence of skilled, fallible maintainers rather than preventing explicit attacks. Solutions for the former do a lot to thwart attacks from the latter, but attack prevention (especially with the form of "just another sandbox") is unlikely to help with the former.


Zig build scripts are arbitrary zig programs, so sandboxing those scripts is a Good Thing. Wasm might be overkill, but using something off-the-shelf that's specifically designed for sandboxing untrusted code is definitely the right approach.


I see no benefits in sandboxing such things as build systems. Sooner or later one eventually needs to execute some external code, like a shell script or cmake. And these external programs can do whatever they want. So, caring about sandboxing within a build system executable is just creating a security theater.


As I understand it, Zig is trying to bring in almost all the stuff that would usually be done by external tools. Zig has its own solution for finding system libraries (instead of pkg-config), it integrates its own C/C++ compiler, and you can do code generation with comptime (or, worst-case, a Zig program that can also be compiled to WebAssembly) instead of an external script. So I think there's a good chance that you'll be able to build most Zig projects entirely inside the sandbox someday.

There's still the obvious problem that if the build system emits malicious code, you'll probably run that code anyway. Personally I think this kind of sandboxing is more useful for enforcing build reproducibility rather than, like, protecting you from viruses in the build.zig file.


I think "build systems" is a too broad category in that argument.

Language-specific build facilities, like Cargo's build.rs and Zig's build scripts, typically have a limited scope - generating a bit of source code, discovering some linker flags, stuff like that. These scripts need to be run by LSP servers when opening the project in an editor to get basic features working, so that's a fairly risky thing.

They are also currently doing things like invoking CMake and other build systems, but you could definitely conceive of a world where that was a separate step in the build process, and that world seems pretty attractive to me.

A common pattern in Rust projects is to have a `*-sys` crate representing the C FFI bindings, and they typically also do something like invoke CMake or similar to actually build the C/C++ library underneath. But if you have a larger project that already integrates multiple build systems, this is really quite inconvenient in most cases.


Your proposal still contains a security hole, since it still allows executing cmake or something similar. Adding sandboxing in some parts/steps of a build system has no benefits, as soon as the system as whole has loopholes allowing bypassing such sandboxing. It's like adding more locks to the front door, when the backdoor has no locks at all.


Security is not, and in fact can never be, all-or-nothing. An imperfect solution is better than no solution. Developers have the reasonable expectation that opening a project in VS Code does not upload their home directory to a remote server. Performing a full build of a project is a different operation with different associated expectations.


I just got so fed up with Starlark trying to do a nontrivial RBE prelude that's fairly different than Meta's.

I added WASM/WASI bindings and wrote the prelude in Haskell.

Both the bindings and the prelude took less time than I already wasted on multiple attempts in Starlark that all collapsed into string goop.

It's nice to be able to bound the execution environment in a build tool but still use a serious programming language.

Given Zig has excellent support for targeting WASM, seems you'd get the same advantages.


Not a lot if you're going to run the code anyway.

But when looking at open source code you don't trust yet, you might want to build code, without running it, so your development tools will work.


Why not WASM?


Unfamiliarity and I believe it requires a compile step. I’m at least familiar with Typescript and Deno so being able to embed them was an appealing idea :)


Codex is fully open source…


You want to use the model that is potentially giving your data to the government vs the one that’s openly rejecting that partnership?


At this point you gotta pick and chose your morality Claude is screwing people on credits and tokens OoenAI is selling three molecules left of your privacy to the government Are those three molecules worth fighting for when your budget is really tight or you are unemployed? Everyone has different priorities


Package a skill with your CLI itself and give users instructions on how to install the skill properly. That allows the agent to read the instructions in a context efficient way when it wants to use the CLI


MCP loads all tools immediately. CLI does not because it’s not auto exposed to the agent, got have more control of how the context of which tools exist, and how to deliver that context.


Accurate for naive MCP client implementations, but a proxy layer with inference-time routing solves exactly this control problem. BM25 semantic matching on each incoming query exposes only 3-5 relevant tool schemas to the agent rather than loading everything upfront - the 44K token cold-start cost that the article cites mostly disappears because the routing layer is doing selection work. MCPProxy (https://github.com/smart-mcp-proxy/mcpproxy-go) implements this pattern: structured schemas stay for validation and security quarantine, but the agent only sees what's relevant per query rather than the full catalog. The tradeoff isn't MCP vs CLI - it's routing-aware MCP vs naive MCP, and the former competes with CLI on token efficiency while retaining the organizational benefits the article argues for.


It does not have to load all tools. As you are able to hide the details in CLI you can implement the same in MCP server and client.

Just follow the widely accepted pattern (all you need 3 tools in front): - listTools - List/search tools - getToolDetails - Get input arguments for the given tool name - execTool - Execute given tool name with input arguments

HasMCP - Remote MCP framework follows/allows this pattern.


I’m not a technical person but I’ve seen people share various tips and tricks to get around the MCP context issues. There’s also this from Anthropic:

https://www.anthropic.com/engineering/code-execution-with-mc


You can solve the same problem by giving subsets of MCP tools to subagents so each subagent is responsible for only a subset of tools.

Or...just don't slam 100 tools into your agent in the first place.


>Or...just don't slam 100 tools into your agent in the first place.

But I can do them with CLI so that's a negative for MCP?


You've missed the point and hyperfocused on the story around context and not why an org would want to have centralized servers exposing MCP endpoints instead of CLIs


I would want to know what point I missed. I can have 100 CLI's but not 100 MCP tools.

100 MCP tools will bloat the context whereas 100 CLI's won't. Which part do you disagree with?


1. The part where you are providing 100 tools instead of a few really flexible tools

2. The part where you think your agent is going to know how to use 100 CLI tools that are not already in its training dataset without using extra turns walking the help content to dump out command names and schemas

3. The part where, without a schema defining the inputs, the LLM wastes iterations trying to correct the input format.

4. The part where, not having the full picture of the tools, your odds of it picking the same tools or the right tools is completely gambling that it outputs the right keywords to trigger the tool to be used.

5. The part where you forgot to mention that for your agent to know that your 100 CLI tools exist, you had to either provide it in context directly, provide it in context in a README.md, or have it output the directory listing and send that off to the LLM to evaluate before picking the tool and then possibly expanding the man pages for several tools and sub commands using several turns.

Don't get me wrong, CLIs are great if its already in the LLMs training set (`git`, for example). Not so great if it's not because it will need to walk the man pages anyways.


> The part where you are providing 100 tools instead of a few really flexible tools

I'm not sure how that solves the issue. The shape of each individual tool will be different enough that you will need different schema - something you will be passing each time in MCP and something you can avoid in CLI. Also, CLI's can also be flexible.

> The part where you think your agent is going to know how to use 100 CLI tools that are not already in its training dataset without using extra turns walking the help content to dump out command names and schemas

By CLI's we mean SKILLS.md so it won't require this hop.

> The part where, without a schema defining the inputs, the LLM wastes iterations trying to correct the input format.

What do we lose by one iteration? We lose a lot by passing all the tool shapes on each turn.

> The part where, not having the full picture of the tools, your odds of it picking the same tools or the right tools is completely gambling that it outputs the right keywords to trigger the tool to be used.

we will use skills

> The part where you forgot to mention that for your agent to know that your 100 CLI tools exist, you had to either provide it in context directly, provide it in context in a README.md, or have it output the directory listing and send that off to the LLM to evaluate before picking the tool and then possibly expanding the man pages for several tools and sub commands using several turns.

skills



”to know what tools you have access to read the dockerfile”?


MCP is fine, particular remote MCP which is the lowest friction way to get access to some hosted service with auth handled for you.

However, MCP is context bloat and not very good compared to CLIs + skills mechanically. With a CLI you get the ability to filter/pipe (regular Unix bash) without having to expand the entire tool call every single time in context.

CLIs also let you use heredoc for complex inputs that are otherwise hard to escape.

CLIs can easily generate skills from the —help output, and add agent specific instructions on top. That means you can give the agent all the instructions it needs to know how to use the tools, what tools exist, lazy loaded, and without bloating the context window with all the tools upfront (yes, I know tool search in Claude partially solves this).

CLIs also don’t have to run persistent processes like MCP but can if needed


but you need to _install_ a CLI. with MCP, you just configure!


Plenty of MCPs require you to install and run them locally, like I said remote MCP has a real advantage over CLI tho


You just paste in a web link to a skill. Your agent is smart enough to know hours to use it or save it.


agree!


Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: