In 2013, a Pennsylvania man became the richest person on Earth … for about two minutes. PayPal had accidentally credited his account $92 quadrillion dollars. That's a 92 with 15 zeros behind it. But within minutes, PayPal realized their mistake, and took it all back. Too bad.

Mistakes like this — big, small and humongous — happen all too often and typically come down to bugs in "smart contracts," computer programs that facilitate digital transactions online. In the case of the PayPal bug, 92 quadrillion is the maximum value that a 64-bit computer can store in its memory. A bug in the code initiated a transfer of funds representing that gigantic number.

As more and more of our finances and purchasing behaviors move online, the importance of bug-free smart contracts has never been greater. Ankush Das, a Ph.D. student in the Computer Science Department (CSD) affiliated with CMU's CyLab Security and Privacy Institute, agonizes over it every day.

"If there is a way for a smart contract to accidentally pay you money — if that error exists — somebody will exploit it to pay themselves money. And this happens all the time, all over the place," said Das, who is advised by CyLab's Jan Hoffman, an associate professor in CSD. "It's very, very important that these smart contracts are free of errors."

Das is the lead designer and developer of a new programming language, which he's named Nomos, aimed at reducing such errors in smart contracts.

"All smart contracts — just like real contracts — have a predefined protocol," he said. "Nomos has a way for a programmer to specify what that protocol is. Then, when you're writing the actual program, the language will actually enforce that you satisfy your predefined protocol. If you make an error, it will say, 'No, no, no. This is not correct. There's a protocol mismatch.'"

Another feature of Nomos relates to transaction fees. In most scenarios, people rarely pay transaction fees themselves, passing the buck to the credit card companies or the vendors. But on a blockchain — the decentralized network of computers around the world facilitating and recording cryptocurrency transactions — users pay the transaction fee themselves.

"A cool and unique feature of Nomos is that whenever you write a smart contract, the language will automatically tell you how much the transaction fee will be," Das said. "There's a guarantee, a mathematical theorem running in the background, that says, 'If the language says the fee will be $5, then it will be exactly $5.' Nothing more, nothing less."

Das said that every transaction in the virtual world faces these potential challenges. Blockchains are just the most recent transparent application of smart contracts, exposing these issues to the world. Thus, the research ideas that power Nomos, like ensuring funds are not lost and that protocols are enforced, can be applied in any digital financial realm.

"People who are skeptical of transacting on certain websites or paying money in certain portals … the kind of work we are doing can help build people's trust in these systems," Das said.

Nomos is available as a web interface and its code is open-source on GitHub.