The cybersecurity company Atalanta has released Argo, a commercial product built on the technology it used to harden Viasat's satellite network after the 2022 Russian attack that opened the war in Ukraine. What sets the tool apart is its claim: instead of estimating that a system is probably secure, Argo tries to prove mathematically that specific security properties hold. Atalanta announced the release on August 18, described in an Associated Press report.
Almost every defense a satellite operator deploys today rests on probability. Penetration tests sample the ways an attacker might get in. Code review catches the flaws a human reviewer happens to notice. Threat models rank the scenarios that seem most likely. Each of these narrows the odds of a breach without ever closing them, and the space sector has spent three years discovering how wide those odds still are. Researchers keep finding unencrypted links, default credentials, and command interfaces they describe as trivial to exploit. Argo is an attempt to change the terms of that problem.
What the 2022 Viasat attack actually broke
The relevance of the Viasat case is specific. On February 24, 2022, hours before Russian forces crossed the border, an attacker logged into a misconfigured VPN used to administer the KA-SAT network, reached the management system that pushes software to the modems, and deployed a wiper called AcidRain. The malware overwrote the flash memory of tens of thousands of SurfBeam2 modems. Viasat's own security chief later put the count between 40,000 and 45,000 devices across Ukraine and Europe. Spillover knocked out remote monitoring of 5,800 Enercon wind turbines in Germany. SentinelOne, which named and analyzed the malware, tied it to prior Russian tooling, and the UK and EU formally attributed the operation to Russia.
The satellite in orbit was never touched. The attack was a ground-segment compromise: one credential, one management channel, one piece of software behaving in a way its operators had not reasoned about. That is precisely the layer Argo is built to examine.
Proof instead of probability
Atalanta calls its approach software understanding, and the engine underneath it is formal methods, a decades-old branch of computer science that uses mathematical logic to prove statements about how code behaves. Where a test checks the outcomes a team thought to try, a formal proof reasons about entire classes of inputs and, in principle, every state a system can reach. Argo combines that technique with AI and digital engineering so the proofs can be updated as a system changes rather than rebuilt from scratch. In the company's own description, the goal is to verify that a software-controlled system performs correctly across normal, abnormal, and hostile conditions.
The idea has a track record in exactly the kind of cyber-physical system a satellite ground segment resembles. In DARPA's High-Assurance Cyber Military Systems program, engineers formally verified the flight software of a Boeing unmanned helicopter, then invited red teams to attack it in operation. The attackers could not compromise its defenses. The lesson was that mathematical guarantees can hold up against a determined adversary, not just a checklist.
Why a vendor tool matters now
Formal verification has long carried a reputation for being slow, expensive, and reserved for aerospace and chip design. The significance of the Viasat work is that an operator running a live commercial network used it to produce evidence, not adjectives. Viasat's chief of cyber strategy, Nick Saunders, told the AP that the year-long effort with Atalanta gave the company a way to develop an understanding of how its systems resist attack, and to produce the math that backs the claim. For a sector where security has often meant a completed questionnaire, provable evidence about the ground segment is a different standard.
Greg Shannon, chief cybersecurity scientist at Idaho National Laboratory, estimated that DARPA has invested well over 2 billion dollars in formal methods over roughly two decades and expects such tools to become part of standard development kits within a decade or two. The Pentagon's chief technology officer, Emil Michael, has said he wants the underlying mathematics to become the Defense Department's gold standard for cybersecurity. The technology behind Argo has also been tapped for the Department of Energy's Genesis Mission on autonomous reactors.
The limits worth stating plainly
A proof is only as good as the properties and assumptions it encodes. Formal verification confirms that a system behaves as modeled; it cannot rule out a threat no one thought to specify, and modeling a large system is itself demanding work. It does nothing for the closed-source flight software running on satellites already in orbit, which cannot be re-architected and often cannot be patched. And the same pairing of AI with formal reasoning that helps defenders map a system also helps attackers understand one faster. Argo narrows the gap between what operators build and what they can prove about it. On the ground segment, where the last major space-cyber catastrophe began with a single misconfiguration, narrowing that gap is worth taking seriously.
News first reported by The Associated Press, with technical background from SentinelOne and CyberScoop.
