Flow Equivalence: A Step on the Path to Formally Verified Asynchronous Design

This post focuses on Galois’s silicon projects and related research efforts around asynchronous circuit design as we approach the 27th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2021), to be hosted by Galois as a virtual conference September 7–10, 2021. In a recent blog post, we shared Galois’s interest in asynchronous circuit design. […]

Read More

The Next Assembly Line – The Quest for Scalable Automation in Software

In 1913 Henry Ford invented the assembly line and forever changed the way the world made physical products. For more than 100 years, the industrial society launched new technologies, new industries, and educational programs focused on perfecting manufacturing and scaling automation via incremental improvements over time.  Process improvement techniques that utilize statistics and mathematical concepts, […]

Read More

Why Asynchronous Design?

This post focuses on Galois’s silicon projects and related research efforts around asynchronous circuit design as we approach the 27th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2021), to be hosted by Galois as a virtual conference September 7–10, 2021. Since our founding, most of Galois’s R&D projects have focused on software and […]

Read More

Proof Repair and Code Generation

Proofs are our bread and butter at Galois – we apply proofs to many different assurance problems, from compiler correctness to hardware design. Proofs and the theorem proving technologies that apply them are very powerful, but that power comes with a cost. In our experience, proofs can be difficult to maintain over time as systems […]

Read More

Conjuring Correct-by-Construction Code That is Safely Composable System-Wide

The title of our blog post may sound like a directive from a Dungeon Master, but it’s firmly rooted in Galois’s forward-thinking computer science.  C/C++ code is the foundation of our most critical systems – even “new” systems nearly always incorporate legacy code. But this type of component reuse carries its own dangers because we […]

Read More

Trustworthy Data Integration: Machine Learning to Expose Financial Corruption

The world was taken by storm when the International Consortium of Investigative Journalists (ICIJ), along with other media bodies, released millions of documents exposing financial chicanery and political corruption. The leaks detailed how prominent people, such as Icelandic Prime Minister Sigmundur Davíð Gunnlaugsson, used offshore entities for illegal activities. Perhaps the most famous of these […]

Read More

Cryptographic Assurance with Cryptol

Field arithmetic code is important and has edge cases lurking everywhere. Cryptol is a tool that can guarantee you’ve got the edge cases right! In this post, we continue reproducing an NCC Group Post about programming in z3. In our last post, we checked the implementation of part of the QUIC protocol. Now we’ll explore […]

Read More

Of Protocols and Pythons

We’ve been working to improve usability for SAW, our tool for verification of C and Java programs. The primary way that users interact with SAW is its specification and scripting language. In order to make SAW as accessible as possible, Python can now be used as that language for SAW! We’ve built an example to […]

Read More