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