Somewhere near the end of my interview with Imandra co-founders Grant Passmore and Denis Ignatovich, I finally felt like I really understood what they've built.
But it took a fairly awkward analogy.
Imandra, which bills itself as a reasoning-as-a-service company, uses artificial intelligence to essentially show how an algorithm would play out under an infinite number of scenarios. I asked the co-founders if it'd be fair to compare it to Dr. Strange looking into millions of possible future outcomes before the big battle at the end of Hollywood blockbuster "Avengers: Infinity War."
They had not seen it. But perhaps that's not surprising. The duo is busy taking on a serious challenge that has a chance to play a significant role protecting consumers and businesses from the unintended consequences of algorithms.
What are those consequences? From Imandra's perspective, they run the gamut -- from helping in-house teams verify their work on B2B systems to high-volume financial trading; and from bulletproofing algorithms that help steer autonomous vehicles to applications in aerospace.
Imandra is industry-agnostic. But Ignatovich has a background as a quant on Wall Street, and Imandra's only publicly visible client is Goldman Sachs.
"It's interesting," Mark Cuban wrote. "But you will burn all your cash moving to Silicon Valley."
In essence, it's taking some of the math-based formal verification developed a decade ago to verify how hardware will work under an infinite number of scenarios and applying that foundation to software. Instead of looking at algorithms as engineering artifacts, it looks at them as mathematical artifacts that can be subjected to established, high-level math.
Typically, an algorithm might be subjected to 100 or so test cases. Maybe more depending on its use cases.
“But by virtue of time and space, you’re only ever running it through a finite number of tests," Passmore told me. "And these systems in general may have an infinite number of possible scenarios. So if you think of a trading system or an auto-pilot system for an autonomous vehicle, no finite number of tests is going to cover the whole state space of the systems. It’s just a drop in the bucket. It’s like throwing darts in the dark, and you’re always wondering ‘what parts of the state space have I not tested?’”
While Imandra established its beachhead in finance, it's also focused on applications in autonomous vehicles and beyond. One of its most recent releases is called Robot OS, which analyzes the safety of robotic controllers.
Passmore and Ignatovich see their role in policing algorithms as larger than just solving problems for any single industry.
“Our mission is to bring this type of rigorous new AI to the masses so we can have proper governance and regulation around algorithms," Passmore said. "We believe strongly that ... our safety is relying on these companies' algorithms that have classically been so opaque. We have to make these things transparent and we have to make them explainable."
Passmore and Ignatovich first met as students at the University of Texas in Austin, where they became roommates. They were inspired by Robert S. Boyer and J Strother Moore, UT professors who helped pioneer formal verification methods with the automated theorem prover.
After graduating from UT, Passmore went into academia, with stints at Carnegie Mellon, The University of Edinburgh, ultimately earning a doctorate from the University of Cambridge. His later work focused on auto-pilot systems for airplanes. Ignatovich, meanwhile, went to Wall Street, where he worked as a quantitative analyst with Deutsche Bank. He later moved to the bank's London office.
During their early careers, key events, such as the $440 million loss because of a trading glitch at Knight Capital, helped them realize the potential for more rigorous verification of algorithms used in these high-risk situations fraught with complex guidelines and nearly infinite scenarios.
“What we realized, really, is that if you think about trading algorithms and auto-pilot systems, the problems are really similar – just different applications," Ignatovich said.
IMANDRA by Aesthetic Integration from David Hobizal on Vimeo.
After forming Imandra in London, the co-founders considered moving to Silicon Valley before deciding to move their startup to Austin this year. They moved the company, in part, for Austin's talent pool, which is deepening as companies including Oracle, AMD and Apple help attract the type of R&D and quantitative reasoning expertise Imandra needs.
They also came here because celebrity investor Mark Cuban told them to. The co-founders said they sent Cuban an email looking for potential investors.
“He wasn’t the right person for us as an investor,” Ignatovich said. “But he’s like ‘You guys are insane. If you continue this, why not come to Texas?’”
Passmore pulled up the old email on his phone. In it, Cuban was skeptical of a move to California. "It's interesting," Cuban wrote. "But you will burn all your cash moving to Silicon Valley."
Passmore and Ignatovich saw his point and the potential savings, and they soon decided Austin would be better than Silicon Valley for their startup.
In April, Imandra announced it had raised $5 million in seed funding from Austin's LiveOak Venture Partners, as well as AlbionVC and IQ Capital in the U.K.
Even the investment was subjected to Imandra's mathematics.
“Here’s a little-known fact," Passmore said. "When we have a term sheet and we have to decide if we’re going to accept … we actually have an Imandra model of our cap table with different classes of shares, what are the rights associated with them and how does that evolve. And we can ask Imandra, ‘If we accept these terms, is there a sequence of events where we could lose control of the board?’"
