It happens time and time again. You are working on a project, and your computer crashes, causing you to lose all your work. But MIT researchers want to solve this problem by building a crash-tolerant data storage system.

“What many people worry about is building these file systems to be reliable, both when they’re operating normally but also in the case of crashes, power failure, software bugs, hardware errors, what have you,” said Nickolai Zeldovich, associate professor of computer science and engineering at MIT, in a statement. “Making sure that the file system can recover from a crash at any point is tricky because there are so many different places that you could crash.”

(Related: MIT creates self-repairing software)

Previously, the researchers were focused on finding bugs in software systems. But when they realized there was no guarantee that they could find and eliminate all bugs, they decided to take a different approach to developing their system. “In this project, we decided to approach the problem from another angle: to prove the absence of bugs using formal methods so that we don’t have to keep searching for more bugs,” Zeldovich told SD Times.

According to the researchers, the formal methods allowed them to prove properties of the system’s final code instead of a high-level schema, which can cause countless complications.

“We hope that the biggest impact from this work, longer-term, will be in showing developers that formal methods are turning a corner in terms of practicality, and more specifically, helping developers formally reason about crash-recovery in systems software,” Zeldovich said.

While the file system guarantees it won’t lose track of data during a crash, he admitted that it is about twice as slow as existing file systems. But the researchers are currently exploring optimizations and aggressive modes of operation to improve its performance.

According to Zeldovich, the file system works with any kind of disk drive, and has been made available on GitHub.

“While it’s a relatively simple design, it might be a good starting point for developers of critical software systems,” he said.