Synthetic Minds (YC S'18) raises $5.5M from Khosla Ventures and Pantera Capital to build program synthesizers

Synthetic Minds is backed by Y Combinator, and just announced its $5.5M seed round. We are thrilled to partner with Khosla Ventures and Pantera Capital. The capital will be used to build the team, meet customer demand, and make progress on our aim of democratizing software creation using program synthesis.

On Monday we announced our seed round, and our graduation from Y Combinator's Summer 2018 batch. I am excited to have found partners who share our view of the future. Building alongside Vinod Khosla, Paul Veradittakit and Joey Krug will be fun. In this post, I'll lay out what lies ahead. But before I do that, a little context.

Synthetic Minds is built with one objective: democratize software creation.

The backstory

In 2015, I first met Vinod during YC investor office hours. I was running my previous biotech company 20n. He told me I need to be working on program synthesis. I thought he was joking. He probably wasn't.

"Program synthesis" is domain jargon for automation that can write computer code.

Earlier in 2010, I had joined UC Berkeley as a postdoc to Ras Bodik. I had just finished my PhD in program synthesis, and work in it was starting to brew. Armando, another of Ras' advisees was the first in this new era with "program synthesis" in his PhD title and mine was the second1. I had spent 4 years at that point on synthesis working with other amazing collaborators including Sumit Gulwani. Around that time, you could fit the number of people working on program synthesis on a stairwell. Quite literally. Below is that group in 2009, and then in 2012.

YC: Take 1

From 2013-17 I was building 20n with my co-founder Chris. YC was one hell of a ride, all the way from the fun interview with Jessica, Trevor, Sam and Geoff; to the amazing help from Geoff, Paul B., Michael, Aaron, and Aaron. Below are some snapshots from that journey (descriptions on hover, or hold down on mobile).

Taking 20n through YC was incredibly useful. The second pic shows Michael Siebel working with us at 1am the night before demo day, and we manufactured real product, built an incredible team, and eventually open-sourced our platform for genetic engineering design.

2018 is different

Since then activity in program synthesis has grown immensely with work being done at Microsoft, many academic centers, SRI, OpenAI, Google Brain/DeepMind. In 2018, courses are being taught on program synthesis (!), conferences dedicated to it, and commercial interest.

The computing landscape is also different. 1) "$/per line of code" has never been higher, 2) we have gone from "code changes every minute" (agile) to "code is unchangeable/law" (blockchain), 3) "$/compute" is tending towards zero.

Building an automation that writes code is within sight, mostly from the cheap compute. It has a business model because of code permanence and because code and data is literally money now. I started building Synthetic Minds in Fall 2017 and participated in the YC Summer 2018 batch.

YC: Take 2

YC became even better between W15 and S18. Shout out to the partners who helped Synthetic Minds: Yuri, Adora, Geoff, Michael, Aaron, and Aaron.

Again, the founder peer network is unparalleled and S'18 had an extra treat with Paul and Jessica taking a hiatus from their retirement to hang out with the batch.

Incredible customer base

“Writing secure smart contracts is extremely difficult, imagine if all of NASA’s rockets’ code were open source. It’ll be impossible for humans to detect all potential vulnerabilities a contract could have. Synthetic Minds synthesizes adversarial programs to attempt to find vulnerabilities that developers don’t want to have, but can’t find all on their own, but computers can.”
Joey Krug (Pantera)

Synthetic Minds' offers a unique solution for writing smart contracts.

Our automation first "reads" Solidity code. In domain jargon, we call it a formal verifier. Normally, it would be computationally intractable to do this comprehensively. But we already established that compute basically costs $0 today. We run our algorithms over many days on a large cluster of servers.

More importantly though, it comes down to UX. Program synthesis plays a critical role. In a few years, synthesizers will understands the functionality desired, and build provably correct code. Right now, our customers want to see how their contracts are going to behave when deployed. Our automation "writes" other contracts that interact with our customer's code. This UX is infinitely easier: Feed the system a Solidity contract, get back Solidity for other contracts that will interact with it in meaningful ways.

We opened up to customers in Summer 2018 and saw immediate demand. I have been working with some incredible projects. Trustless smart contract platforms present a unique execution environment. Executions will be truncated, interactions across contracts will exhibit interleaving behavior, and executions will be permanent. The limitations imply our customers have unique ways of building their solutions; and the language novelty mixed with permanence of executions makes everybody nervous about correctness.

Paying customers are using Synthetic Minds

“Pantera believes that every company building smart contracts will benefit from the automated verification and synthesis technology that Synthetic Minds has built.”
Paul Veradittakit (Pantera)

We have paying customers using our synthesizer. I have been humbled by the amount of inbound interest, and sincerely apologize to all the projects that have been kind enough to wait.

Seed Fundraise

Y Combinator is useful in multiple ways. The obvious ones are defining focus, mechanics of "stage-0" startups, showing technical founders how to sell, reputation and network access. The non-obvious, most important, one is the founder peer group.

When building hard-tech there are few people that appreciate and support it better than the team at Khosla Ventures. Over multiple sessions with Vinod driving and Maryanna, Kanu, Samir, and Sven helping out, we found complete alignment on the plan of action to build Synthetic Minds.

At Pantera, when meeting Joey Krug in-person, I did not know whether he wanted to talk about Augur as a customer or Pantera as an investor :). Joey is the co-founder of Augur, and Pantera's co-CIO. He and I had been discussing using Synthetic Minds for Augur earlier in the summer. When Paul Veradittakit joined the conversation, it became obvious that Pantera's involvement would greatly focus our attention on the right problems.

Eventually, it was a no-brainer to partner with Khosla Ventures and Pantera Capital to get us to the next stage.

In 2 years, access to code and data will be very different

One may argue that through 2000-2010, mass access to data was enabled albeit at the cost of centralizing it behind walled-gardens. 2010 onwards, Nakamoto consensus has demonstrated how all data created/used within its one application can be made universal and open. In contrast, building code is still a restricted activity. It should be unacceptable that only 0.28% of the population (programmers) have the ability to make software.

“We believed in the team at Synthetic Minds and their expertise to build hard tech that will further grow adoption of smart contracts, both in the public and enterprise domains. They are uniquely positioned to enable an enterprise-grade, safe, smart contract platform."

"Provably correct smart contracts through program synthesis are key steps needed for smart contracts on the blockchain and for software in general.”
Vinod Khosla

Synthetic Minds will focus on synthesis as the gateway into the smart contract ecosystem, and software in general.

UX = Synthesis

We really care about democratizing software creation, i.e., building automation that can read and write code so that human input goes into deciding what to build rather than how.

Value = Digital

PoW is an incredible at converting physical resources into digital. As more value becomes and stays digital (goods, tokens, exchanges), viability of this closed ecosystem is tied to its correctness. We will be working hard to enable that.

Infrastructure = Perpetual

Infrastructure that is perpetually running is a great side-effect of a decentralized network. While public networks are obvious starting points, we'll be exploring synthesis applications in the enterprise.

Come build with us

I am looking for technical people excited about the prospect of automating software creation. An interest in smart contracts would be appreciated. There are lots of interesting infrastructure, search space exploration, smart contract encoding, and scaling problems to be tackled. We have barely scratched the surface, and are looking for fun engineers to build this together.

See more: