They do however want strict measures in place to avoid abuse, and the export control was the only tool they had to stop Anthropic from releasing the model.

Though I also wonder if it's even possible to patch things without severely crippling the abilities of the model.

Not taking a dig at people, it was not a terrible choice earlier. Not like these models are inventing net new ways to exploit systems.

You just need to create a simple workload - think of it like an e2e test case you care about. It can be in any language or lib. Next you need to run this test in our VM.

We then simulate 100s of realistic production scenarios like slow network, different cpu scheduling etc. and save the environments where your test case fails.

Those failing environments can be inspected, you can replay then and they will always produce the exact same result.

Every non-deterministic property is turned into a knob you or a coding agent can control. We have helped teams perfectly reproduce support incidents and found bugs in some of the world's most well tested software (including a database).

Comments URL: https://news.ycombinator.com/item?id=48607073

Points: 13

# Comments: 2

Thank god people protested against it and made them drop the plan.

Because we have tools and techniques that can guarantee the absence of certain behavior in a bounded state space using formal methods (even unbounded at times)

Sure, it's hard to formally verify everything but if you are dealing with something extremely critical why not design it in a way that you can formally verify it?

But yeah, the easy button is keep throwing more tokens till you money runs out of money

The first thing you’d probably try is to generate random sequences of pushes and pops, run a lot of tests, and wait for something to break. Using both operations feels like the most thorough way to test. It seems like the best coverage, the highest chance of finding a bug. But is it?

If you pick push and pop at random, half and half, you’ll need about 370,000 tests before you ever hit the overflow. That number isn’t a mistake. Pushes and pops cancel each other out, like a random walk: the stack goes up a bit, then down, then up again. Getting to 33 items is like flipping a coin and getting 33 heads in a row. It almost never happens.

Now try something different. Before each test, pick a random non-empty subset of the API. With two operations, you get three cases: both push and pop, just push, or just pop. In a third of your tests, you’ll only use push, so every operation grows the stack. The bug shows up right away.

If you leave out features at random when you write tests, you find the stack bug about a third of the time. Every test that only uses push will overflow. Before, the chance was almost zero. The tests that only use push are the ones that catch the bug, and you get those just by picking random subsets. You didn’t have to guess that pop was the problem. Doing less actually finds more.

Claude Code has been super helpful in this; however, I had to do a lot of back-and-forth to verify the output in an IDE and then prompt Claude again with suggestions to fix the proof.

Yesterday, Axiom, one of the model labs working on a foundation model specializing in mathematics, released AXLE, the Lean Engine. The first thing I did was create a Skill so Claude Code can use it as a verifier for Lean code it writes.

Works surprisingly well.

Comments URL: https://news.ycombinator.com/item?id=47279369

Points: 2

# Comments: 1

Comments URL: https://news.ycombinator.com/item?id=46877745

Points: 1

# Comments: 0

Comments URL: https://news.ycombinator.com/item?id=46752457

Points: 4

# Comments: 2

Comments URL: https://news.ycombinator.com/item?id=46741678

Points: 8

# Comments: 2

I have been experimenting with multiple GTM and CRM setups to book more demos with potential customers. They were all super painful to use; most felt very restrictive and basically pushed you to leave your creativity at the door.

So I vibe-coded the sales GTM tool I wanted, it's basically a clean interface for Claude Code running very specific tasks: 1. Enriching leads with very high-quality information - Use Chrome to browse LinkedIn, construct an org chart, see what people are interacting with, etc. 2. Score each enriched lead based on our internal criteria, a lot of which is based on the Founding Sales book. 3. Find the decision maker at each org and reach out to them.

Once we remove 90% of the noise and have a list we should spend our time on, we decided to send out cold emails.

A week later - 10 booked demos! This is insane. Feel free to try it yourself, it's local first, MIT license - https://github.com/chaitanyya/sales - Open an issue, the entire app is heavily vibe-coded and may be a little rough.

Comments URL: https://news.ycombinator.com/item?id=46697157

Points: 5

# Comments: 1

More often than not, people test the wrong things; they struggle to even identify the right properties to test.

I question my worldview on this because I don't think it's a particularly difficult problem. There are companies like Antithesis that have done incredible work in this space.

I am building in automated property-based testing, and it's not an easy sell.