chaitanyya

The usable formal methods hackathon. Build a piece of real-world production software, and formally verify it.

in all our hearts they were always rated CCC

Anthropic is probably overcharging for Claude API usage. I enabled API based billing for 2 sessions on Claude Code and it logged 700m input tokens.

I don't believe US government wanted to restrict the model use to US citizens only. The bad actors will and can find their ways around it.

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.

How much of it is just exposing poor engineering practices people got away with because it was not economically viable earlier to spend human hours to exploit a system?

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.

Thanks, we need a lot of work in the docs and the homepage. A lot of that part was very rushed.

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.

This reminds me of the free internet Facebook tried to launch in India to kill net neutrality

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

What do they mean when they say "no diminishing returns?" does this essentially mean the code you are testing has no bounded state space and you continue to find infinite paths?

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

Good shit! going to experiment with some complex use cases

Imagine a stack with two operations: push and pop. There’s a bug lurking in it. If you ever put more than 32 items on the stack, it crashes. You don’t know this yet. Your job is to find the bug.

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.

I have been getting into Lean4, mostly playing around with writing proofs for properties of distributed software systems.

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.

Well it definitely killed mine so I can't say this is not true

what does that even mean? these two are not even closely related, though your tool may help be useful for our sales agent

What you are about to read took us less than 3 hours to put together. Built using Claude Code, and uses Claude Code as a backend (lol, I know).

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.

It's an interesting one. Every time I speak with engineering teams about reliability and correctness, they all want more of it, yet when it comes to investing in it, it's never really a priority.

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.

"IBM to acquire OpenAI" somebody should put this up on polymarket lol