Argument Computer Corporation

Accelerate Certified Computing.

We're still in the early days of the Computing Revolution. We powered on the first general-purpose digital computers less than a century ago, and many remember a world substantially without them. Thinking machines are shockingly new, and we don't really know what (or perhaps who) they are yet. We’re in the middle of an epochal transformation whose nearest precedent is the invention of writing.

But computers can be scary. Every year, our world of machines and apps gets noisier and more confusing. Software lets you do amazing things, work better, connect with people you care about, but sometimes it seems like it's breaking society. How do we know who and what to trust anymore when things are changing so fast?

When computers work, they are glorious: elevating and emancipatory to the human spirit. When they don't, they're an Orwellian boot stamping on a user's face.

Our mission at Argument is computers that work.

Computers that ship with unforgeable formally-proven cryptographic certificates proving they were built correctly, without bugs, and with your—the user’s—best interests in mind. These certificates guarantee that computer programs do exactly what they claim to do, no more, no less.

Steve Jobs said that computers are like bicycles for the mind. Anyone who's ever ridden a bike through the streets of a car-centric city knows just how true that metaphor is.

From the dawn of urbanization until the 19th century, cities were locked into two dimensions, limited by how many stairs a person could climb. Neither horses, carriages, trains nor bicycles changed that. Until Elisha Otis invented an elevator that wouldn't send you hurtling to the earth if its hoisting rope failed, and suddenly cities unfolded into the third dimension. Computers can be more than bicycles: they can be skyscrapers.

The ix protocol is the foundation of our vision of certified computing. ix compresses Lean formal proofs into succinct zero-knowledge certificates, smaller than a kilobyte and verifiable in less than 100 ms anywhere. An ix certificate is the same size whether it's validating a small program or a large formal mathematics library like Mathlib. ix certificates are portable, trustless, and themselves built using formally verified infrastructure, and generating them is efficient: Mathlib can be certified from scratch in just a few hours. ix is also privacy-preserving, allowing disclosure of theorems while keeping the proofs themselves secret.

All of our work is open-source and permissively licensed, and we welcome community participation whether on our GitHub or Zulip.

We're here to build skyscrapers for the mind