I think it makes a lot of sense for businesses, but I really don’t get why companies like this don’t provide an individual usage tier that costs some flat amount with an explicit prohibition of for-profit use. I just want to try the thing out, not have a lengthy e-mail conversation with a salesperson, and my design input isn’t relevant.
I get the deterministic hypervisor stuff. I get adding assertions. But what techniques does Antithesis explore the state space? Are we looking at a policy like go-explore (random exploration from the frontier of known states) or a beam search? Does the search policy derive from existing research on fuzzers/constraint-solvers? Is the search policy evaluated offline, or is the exploration policy being learned online, to improve the efficacy of state-space navigation in new contexts?
We’ve got a research team (hiring!) that’s constantly developing better exploration policies. So the true answer is that this is constantly in flux.
We intentionally don’t share too much about what the strategy here is as its a bit secret sauce and a bit too fluid to pin down.
We collect signals from our SDKs assertions, coverage information, and logs produced by your program to autonomously decide what is worth exploring further. We do look at existing research and that deeply inspires our research team. Ie. I hear them talk about surprisal, multi-armed bandits, frontiers, etc.
I really don’t want you to die of curiosity, so come join our discord! Anyone is welcome and we’re pretty good about answering your many questions: discord.gg/antithesis
(I’m currently a TL at antithesis, but not for the research team)
Super cute. I think it’s underappreciated by folks outside the field how clever coverage-guided fuzzing tools have become, and how general of search tools they can be, in the right context. I’m becoming excited to have an opportunity to try out Antithesis for real.
I think of this post as a spiritual successor to IJON, a fuzzer paper from a few years ago which introduced a set of annotation methods spiritually similar to Antithesis’ “sometimes assertions,” and used those to automatically solve Super Mario Bros on the NES.
Title reminds me of a few years ago when I tried solving Zelda puzzles with Alloy: https://github.com/mk12/zeldalloy. Though reading further, it’s quite different. I had no idea something like Antithesis SDK existed.
After reading, I still don’t think I fully understand what Antithesis is. I think the bit that’s getting me is how something could be completely reproducible unless you ran it on actual hardware.
This is really neat. It’s a shame Antithesis is “call for pricing” expensive and not just, like, monthly fee expensive.
“call for pricing” is usually a covert way to extract design input from prospects, so can’t really blame them.
I think it makes a lot of sense for businesses, but I really don’t get why companies like this don’t provide an individual usage tier that costs some flat amount with an explicit prohibition of for-profit use. I just want to try the thing out, not have a lengthy e-mail conversation with a salesperson, and my design input isn’t relevant.
Wow, maybe using Antithesis to test my work on desktop Linux accessibility isn’t as crazy as I thought. Looks expensive, though.
Incredible. But how does it woooooork ??
I get the deterministic hypervisor stuff. I get adding assertions. But what techniques does Antithesis explore the state space? Are we looking at a policy like go-explore (random exploration from the frontier of known states) or a beam search? Does the search policy derive from existing research on fuzzers/constraint-solvers? Is the search policy evaluated offline, or is the exploration policy being learned online, to improve the efficacy of state-space navigation in new contexts?
So many questions. I am dying of curiosity.
We’ve got a research team (hiring!) that’s constantly developing better exploration policies. So the true answer is that this is constantly in flux.
We intentionally don’t share too much about what the strategy here is as its a bit secret sauce and a bit too fluid to pin down.
We collect signals from our SDKs assertions, coverage information, and logs produced by your program to autonomously decide what is worth exploring further. We do look at existing research and that deeply inspires our research team. Ie. I hear them talk about surprisal, multi-armed bandits, frontiers, etc.
I really don’t want you to die of curiosity, so come join our discord! Anyone is welcome and we’re pretty good about answering your many questions: discord.gg/antithesis
(I’m currently a TL at antithesis, but not for the research team)
Super cute. I think it’s underappreciated by folks outside the field how clever coverage-guided fuzzing tools have become, and how general of search tools they can be, in the right context. I’m becoming excited to have an opportunity to try out Antithesis for real.
I think of this post as a spiritual successor to IJON, a fuzzer paper from a few years ago which introduced a set of annotation methods spiritually similar to Antithesis’ “sometimes assertions,” and used those to automatically solve Super Mario Bros on the NES.
Title reminds me of a few years ago when I tried solving Zelda puzzles with Alloy: https://github.com/mk12/zeldalloy. Though reading further, it’s quite different. I had no idea something like Antithesis SDK existed.
After reading, I still don’t think I fully understand what Antithesis is. I think the bit that’s getting me is how something could be completely reproducible unless you ran it on actual hardware.
They run your software on their virtualized, deterministic OS which is a fork of one of the BSDs, I forget which.
They use their own deterministic fork of bhyve on FreeBSD.
aside: Oh, Andrew Kelley! I didn’t expect that you’d be the person to respond to me. You’re on my “people I think are cool” list on my website.
The more I hear about people using BSDs for different tasks, the more I feel like I should spend some time using one.
Cheers, thanks for the kind words