HN user

wwilson

4,328 karma

Building something cool. Email me at: will.wilson@antithesis.com

Posts95
Comments103
View on HN
antithesis.com 20d ago

My quest to see all of Tetris

wwilson
73pts17
antithesis.com 4mo ago

A Fighting Retreat

wwilson
1pts0
antithesis.com 4mo ago

Formal Methods for Rust Unsafe

wwilson
4pts0
antithesis.com 7mo ago

We interfaced single-threaded C++ with multi-threaded Rust and lived

wwilson
1pts0
antithesis.com 7mo ago

Test ACID compliance with a ring test

wwilson
1pts0
antithesis.com 7mo ago

When your customer leads your Series A

wwilson
16pts0
www.ft.com 7mo ago

Startups promise to catch bugs in AI-generated software

wwilson
2pts0
antithesis.com 8mo ago

They don't even have eyes

wwilson
5pts0
antithesis.com 9mo ago

Did you get lucky or unlucky?

wwilson
2pts0
pracap.com 10mo ago

Global Crossing Is Reborn

wwilson
2pts0
www.youtube.com 11mo ago

Scaling Correctness: Marc Brooker on a Decade of Formal Methods at AWS [video]

wwilson
2pts0
www.youtube.com 12mo ago

FoundationDB: From Idea to Apple Acquisition

wwilson
4pts0
www.youtube.com 1y ago

Let's all write good software [video]

wwilson
2pts0
antithesis.com 1y ago

Fix the New Things First

wwilson
2pts0
antithesis.com 1y ago

Finding a way to make on-call better

wwilson
2pts0
antithesis.com 1y ago

The pragmatic magic of semi-formal methods

wwilson
3pts0
antithesis.com 1y ago

Antithesis for Founders

wwilson
6pts3
sqlsync.dev 1y ago

Antithesis Driven Testing

wwilson
6pts0
concerningquality.com 1y ago

Bug Bash 2025 conference writeup

wwilson
5pts1
www.youtube.com 1y ago

Experience with semi-formal proofs [video]

wwilson
3pts0
bugbash.antithesis.com 1y ago

BugBash 2025: Software reliability conference

wwilson
11pts1
www.antithesis.com 1y ago

Rolling for our new initiative: Test Composer

wwilson
5pts0
newsletter.pragmaticengineer.com 1y ago

How to debug large, distributed systems: Antithesis

wwilson
1pts0
antithesis.com 1y ago

Debugging in the Multiverse

wwilson
201pts58
antithesis.com 1y ago

No Ghost Policy

wwilson
1pts1
antithesis.com 1y ago

Security at Antithesis: A Manifesto

wwilson
1pts0
antithesis.com 2y ago

At the Mountains of Madness

wwilson
153pts85
antithesis.com 2y ago

Solving Zelda with the Antithesis SDK

wwilson
36pts8
antithesis.com 2y ago

How Antithesis finds bugs

wwilson
160pts53
antithesis.com 2y ago

Antithesis announces Artificial General 8-bit Intelligence (AG8I)

wwilson
21pts0

I’ve been running one for a while and love it. Have also built a Nix -> OpenWRT config language transpiler so that I can keep my router state in Nix files and have nice deterministic rollbacks etc. It’s been great!

Author here. That’s right — the challenge was representing a tree in an existing SQL database that we’d chosen for its pricing model. I think encoding a B-tree in SQL would be a lot less fun even than what we did.

[Disclaimer: Started Antithesis]

If you run your Hegel tests in Antithesis, you get this for free (along with various sorts of “non-local” assertions, perfect reproducibility even for concurrent or distributed code, etc.).

But yeah, not hard to hack together basic coverage guidance outside Antithesis. That works well for large classes of programs, just not a majority of them.

If I had been wearing my fiendish CEO hat at the time, I might have even said something like: "somebody pointing this out will be a great way to jumpstart discussion in the comments."

One of the evilest tricks in marketing to developers is to ensure your post contains one small inaccuracy so somebody gets nerdsniped... not that I have ever done that.

Glad you enjoyed the talk! Making Bombadil able to take advantage of the intelligence in the Antithesis platform is definitely a goal, but we wanted to get a great open source tool into peoples’ hands ASAP first.

Antithesis | Distributed Systems Breaker Extraordinaire | Full-time | SF or London or DC

---

Have you always wanted to channel your inner Kyle Kingsbury? We are looking to hire somebody with a deep understanding of distributed systems who can bring open source or customer software under test in our platform and find fun issues in it.

Preferred locations: SF, London, DC. Remote is a possibility for this role if you're really good (though be aware that we're a very in-person company culturally speaking, so it might be annoying for you).

To apply: email 'will' at our company domain with a description of something interesting that you've worked on.

It’s not quite a fair comparison, since an RL agent is trying to learn a policy that wins fair and square, while a fuzzer is able to take back moves. But if you’re working in a domain (like anything that can be simulated) where “time travel” is possible, you’d have to be crazy not to use it!

The longer you run it, the cleaner the run gets. But Metroid is a very compute-intensive game to fuzz, and we were already nearing the limits of what BigQuery could do for us with that run.

Yes, this is a really fun idea and something that we want to do. Though these days we’re setting our sights higher than Nintendo…

A funny story though: a regular conference gimmick we have is “Man vs. Machine” where we have attendees race our fuzzer to the end of Mario level 1-1. We did this at the final year of Strange Loop, and the fuzzer was winning handily until not one, not two, but three different professional speedrunners walked by and destroyed us.

Corensic was impressive tech. I actually debriefed with one of their founders years ago. IIRC, their product was focused on finding single-process concurrency bugs.

Deterministic hypervisors are by no means new. Somebody once told me that VMWare used to support a deterministic emulation mode (mostly used for internal debugging). Apparently they lost the capability some time ago.

There have historically been two giant adoption challenges for DST.

(1) Previously, you had to build your entire system around one of the simulation frameworks (and then not take any dependencies).

(2) It’s way too easy to fool yourself with weak search/input generation, which makes all your tests look green when actually you aren’t testing anything nontrivial.

As you say, Antithesis is trying to solve both of these problems, but they are very challenging.

I don’t know of anybody else who has a reliable way of retrofitting determinism onto arbitrary software. Facebook’s Hermit project tried to do this with a deterministic Linux userspace, but is abandoned. (We actually tried the same thing before we wrote our hypervisor, but found it didn’t work well).

A deterministic computer is a generically useful technology primitive beyond just testing. I’m sure somebody else will create one someday, or we will open-source ours.

DST was i̶n̶v̶e̶n̶t̶e̶d̶ popularized at FoundationDB a little over a decade ago, and has been quietly gathering steam ever since. If you’re interested in the technique, the FDB paper has some good info in section 4 and section 6.2: https://www.foundationdb.org/files/fdb-paper.pdf

(Disclosure: I am an author.)

I also gave a talk overview of it at Strange Loop back in 2015, but don’t have the youtube link handy.

If you’re interested in trying DST, we have a new company that aims to make it a much easier lift, especially for existing projects that can’t be retrofitted onto one of the many simulation frameworks: https://antithesis.com

Happy to answer any questions about the approach, here or over email.

No, we don’t require any paravirtualization at all, and nothing needs to be manually rewritten. I’m not sure where you got that impression.

It also is not in any sense a replay engine. We don’t need to record anything except the inputs!

Yes, unfortunately we have not figured out how to rewind time in the real world yet. When we do, there are a lot of choices I'm going to revisit...

Good suggestion on leaving LD_PRELOAD unset if it was previously unset. We will fix that.

I’m torn on whether MD_PRELOAD or LD_PRELOAF is more obnoxious to other programs.

Fun fact: A previous version of this program used an even more inscrutable `env[0][0]+=1`, which is great as a sort of multilingual C/English pun, but terrible in the way that all “clever” code is terrible.

Biggest advantages I know of for dynamic linking:

* You can use the LD_PRELOAD trick to override behavior at runtime.

* You can run with entirely different implementations of the dynamically linked library in different places.

* Software can pick up interface-compatible upgrades to its dependencies without being re-compiled and distributed again.

We use all three of these tricks in our SDKs, FWIW. But it is still a giant pain in the ass.