Original title: A shallow dive into formal verification
Original author: Vitalik
Original translation: Peggy, BlockBeats
Editor's note: With the rapid advancement of AI programming capabilities, software security is facing a new paradox: AI can generate code more efficiently, but it can also find vulnerabilities more effectively. This issue is particularly crucial for the cryptocurrency industry. Once there is a defect in smart contracts, ZK proofs, consensus algorithms, and on-chain asset systems, the consequences are often not mere software errors, but irreversible financial losses and a collapse of trust.
Vitalik discusses in this article another pathway to code security in the AI era: formal verification. In simple terms, it does not rely on human auditors to check the code line by line, but instead expresses the properties that the program should satisfy as mathematical propositions and then uses machine-checkable proofs to verify whether these properties hold. In the past, formal verification remained in a relatively niche realm due to high barriers and cumbersome processes; however, as AI can assist in code writing and proofs, this approach is regaining practical significance.
The core judgment of the article is not that "formal verification can solve all security problems." On the contrary, Vitalik repeatedly reminds us that "provably secure" does not equal absolute security: proofs might overlook critical assumptions, the specifications themselves could be incorrectly written, unverified code, hardware boundaries, and side-channel attacks could also become new sources of risk. Still, it provides a more reliable security paradigm: expressing developers' intentions in multiple ways, and then allowing the system to automatically check if these expressions are compatible with each other.
This is particularly important for Ethereum. Future Ethereum will increasingly rely on complex underlying components, including STARKs, ZK-EVM, quantum-resistant signatures, consensus algorithms, and high-performance EVM implementations. The implementation of these systems is extremely complex, but their core security goals can be relatively clearly formalized. It is precisely in these scenarios that AI-assisted formal verification may offer the greatest value: letting AI handle writing efficient code and proofs, while humans are responsible for checking whether the proven propositions truly align with their desired security goals.
From a broader perspective, this article is also Vitalik's response to network security in the AI era. In the face of stronger AI attackers, the answer is not to abandon open-source, give up smart contracts, or revert to relying on a few centralized institutions, but to compress critical systems into smaller, more verifiable, and trustworthy "security cores." AI will lead to a large increase in rough code, but it may also make truly important code safer than in the past.
Here is the original text:
Special thanks to Yoichi Hirai, Justin Drake, Nadim Kobeissi, and Alex Hicks for their feedback and review of this article.
In recent months, a new programming paradigm has rapidly emerged in the cutting-edge development circles of Ethereum and many other corners of the computing field: developers write code directly using very low-level languages, such as EVM bytecode, assembly language, or using Lean, and verify its correctness by writing machine-checkable mathematical proofs in Lean.
If applied correctly, this method could potentially generate extremely efficient code and may be much safer than past software development methods. Yoichi Hirai referred to it as "the ultimate form of software development." This article will attempt to explain the basic logic behind this method: what formal verification can actually do, where its shortcomings and boundaries lie—both in the context of Ethereum and in the broader software development field.
What is formal verification?
Formal verification refers to the process of writing mathematical proofs of theorems in a manner that can be automatically checked by machines.
To provide a relatively simple yet interesting example, we can examine a basic theorem about the Fibonacci sequence: there is an even number among every three numbers, while the other two are odd.
A simple method of proof is to use mathematical induction, progressing three numbers at a time.
First, let’s look at the base case. Let F1 = F2 = 1, F3 = 2. Through direct observation, it can be seen that this statement—"when i is a multiple of 3, Fi is even; in other cases, Fi is odd"—holds true before x = 3.
Next is the inductive step. Assume the statement holds before 3k+3, meaning we already know the parity of F3k+1, F3k+2, and F3k+3 is odd, odd, even respectively. Thus, we can calculate the parity of the next group of three numbers:
From this, we have completed the derivation from "the known statement holds before 3k+3" to "confirming the statement also holds before 3k+6." By continuously repeating this reasoning, we can be confident that this pattern holds for all integers.
This argument is convincing to humans. But what if you want to prove something that is a hundred times more complex, and you truly want to confirm that you haven’t made a mistake? At this point, you can construct a proof that will also be convincing to a computer.
It would roughly look like this:
This is the same reasoning, just expressed in Lean. Lean is a programming language often used for writing and verifying mathematical proofs.
It looks quite different from the "human version" proof I provided earlier, and there are good reasons for this: what is intuitive to a computer is completely different from what is intuitive to a human. The computers referred to here are the traditional "computers"—"deterministic" programs made of if/then statements, rather than large language models.
In the proof above, you are not emphasizing the fact that fib(3k+4) = fib(3k+3) + fib(3k+2); you stress that fib(3k+3) + fib(3k+2) is odd, while that grandly named omega tactic in Lean will automatically combine this with its understanding of the definition of fib(3k+4).
In more complex proofs, you sometimes must explicitly state at every step: which mathematical law allows you to make this move, and these laws may sometimes bear obscure names like Prod.mk.inj. But on the other hand, you can also expand huge polynomial expressions one step at a time and only need to write a line with expressions like omega or ring to complete the proof.
The lack of intuitiveness and the cumbersome nature here are significant reasons why machine-verifiable proofs, despite existing for nearly 60 years, have remained in niche areas. However, at the same time, many things that were previously nearly impossible are quickly becoming feasible due to the rapid advances in AI.
Verifying computer programs
At this point, you might think: All right, so we can get computers to verify the proofs of mathematical theorems, and finally determine which crazy new discoveries about prime numbers are true and which are just errors buried in hundreds of pages of PDF papers. Maybe we can even figure out whether the proof about the ABC conjecture by Shinichi Mochizuki is actually correct! But aside from satisfying curiosity, what practical significance does this have?
The answer can have many facets. For me, a very important answer is: verifying the correctness of computer programs, especially those involving cryptography or security. After all, computer programs themselves are mathematical objects. Therefore, proving that a computer program operates in a certain way essentially means proving a mathematical theorem.
For example, suppose you want to prove whether encrypted communication software like Signal is truly secure. You can first clarify mathematically what "secure" means in this context. In summary, you want to prove that under certain cryptographic assumptions, only individuals with the private key can gain any information about the message content. In reality, there are many important security properties.
And it turns out there is indeed a team trying to clarify this matter. One of the security theorems they proposed looks something like this:
Here is a summary of the theorem's meaning by Leanstral:
passive_secrecy_le_ddh theorem is a compact reduction that indicates, under the random oracle model, the passive message confidentiality of X3DH is at least as hard to break as the DDH assumption.
In other words, if an attacker can break the passive message confidentiality of X3DH, then they can also break DDH. Since DDH is generally assumed to be a hard problem, X3DH can also be seen as resistant to passive attacks.
The theorem proves that if an attacker can only passively observe Signal's key exchange messages, they cannot distinguish the final generated session key from a random key with more than negligible probability advantage.
If combined with a proof demonstrating that AES encryption is implemented correctly, you then have a proof that the Signal protocol's encryption mechanism can withstand passive attackers.
Similar verification projects already exist that are used to prove the secure implementation of TLS and other cryptographic components within browsers.
If you can achieve end-to-end formal verification, then you are not just proving that a certain protocol description is theoretically secure, but that the specific code being run by users is also secure in practice. From the user's perspective, this greatly increases the level of "no trust": to fully trust this code, you do not need to examine the entire codebase line by line, but only check those statements that have already been proven true.
Of course, there are some very important asterisks that need to be reserved, especially regarding what the keyword "security" actually means. It is easy for people to forget to prove the truly essential claims; it is also easy to encounter a situation where the claims needing proof have no simpler description than the code itself; and very easy to inadvertently introduce some assumptions that ultimately do not hold into the proof. You can also easily argue that only a certain part of the system really needs formal proof, but later find that in other parts, even at the hardware level, key vulnerabilities arise. Even the implementation of Lean itself may have bugs. But before discussing these headache-inducing details, let's further explore: if formal verification could be ideally and correctly completed, what near-utopian prospects it might bring.
Security-focused formal verification
Bugs in computer code are already worrisome.
When you put cryptocurrency into immutable on-chain smart contracts, code bugs become even more terrifying. Because once the code goes wrong, hackers from North Korea might automatically transfer all your money away, leaving you with almost no recourse.
When all of this is wrapped up in zero-knowledge proofs, code bugs become even more frightening. Because if someone successfully breaches the zero-knowledge proof system, they could withdraw all funds, and we might be completely unaware of where the problem lies—worse yet, we might not even know that a problem has occurred.
As we have powerful AI models, code bugs will also become even more terrifying. For instance, models like Claude Mythos, after two years of improvements, might now be able to automatically discover these vulnerabilities.
Some people, facing this reality, began to advocate for abandoning the fundamental concept of smart contracts or even believe that cyberspace can never become a domain where the defender inherently possesses an asymmetric advantage over attackers.
Here are some quotes:
To secure a system, you need to spend more tokens discovering vulnerabilities than attackers need to exploit them.
Moreover:
Our industry has been built around deterministic code. Write code, test it, deploy it, and then know it will run correctly—but in my experience, this contract is breaking down. Among the pinnacle operators in truly AI-native companies, codebases have begun to turn into something like "you have to believe it will run," and the probability of that belief can no longer be precisely specified.
Worse yet, some believe the only solution is to abandon open-source.
This would be a bleak future for cybersecurity. Especially for those who care about the decentralization and freedom of the internet, it will be an extremely grim future. The entire spirit of cyberpunk is fundamentally built on the idea that defenders have the advantage online. Building a digital "castle"—whether it manifests as encryption, signatures, or proofs—is far easier than destroying it. If we lose this, internet security will have to come from economies of scale, from pursuing potential attackers worldwide, and more broadly, from a binary choice: either dominate everything or face destruction.
I disagree with this judgment. I have a much more optimistic vision for the future of cybersecurity.
I believe that the challenges brought about by powerful AI vulnerability discovery capabilities are indeed severe, but they represent a transitional challenge. Once the dust settles and we enter a new equilibrium, we will arrive at a state that is more favorable to defenders than in the past.
Mozilla agrees with this. To quote them:
You may need to reorder priorities for everything else and invest in this task in a continuous and focused manner. But there is light at the end of the tunnel. We are very proud to see how teams are stepping up to tackle this challenge, and others will do the same. Our work is not done yet, but we have crossed a tipping point and started to see a future that is far more than just "barely keeping up." The defenders finally have a chance for decisive victory.
…
The number of defects is finite, and we are entering a world where we can finally identify them all.
Now, if you search for "formal" and "verification" in Mozilla's article, you will find that neither term appears. A positive future for cybersecurity does not strictly depend on formal verification, nor on any single technology.
So what does it depend on? Essentially, it comes down to the following diagram:
Over the past few decades, many technologies have driven the trend of "reducing the number of vulnerabilities":
type systems;
memory-safe languages;
improvements in software architecture, including sandboxes, permission mechanisms, and more generally, clearly distinguishing the "trusted computing base" from "other code";
more effective testing methodologies;
an increasing number of pre-written and audited software libraries.
AI-assisted formal verification should not be viewed as a brand new paradigm but seen as a powerful accelerator: it is accelerating a trend and paradigm that has long been moving forward.
Formal verification is not a panacea. But in certain scenarios, it is particularly applicable: that is, when the goals are much simpler than the specific implementations. This is especially evident in some of the trickiest technologies that will be deployed in Ethereum's next major iteration, such as quantum-resistant signatures, STARK, consensus algorithms, and ZK-EVM.
STARK is a very complex software. But its core security properties are very easy to understand and can be easily formalized: if you see a proof pointing to the hashes H of program P, input x, and output y, then either the hash algorithm used by STARK has been broken, or P(x) = y. Therefore, we have the Arklib project, which attempts to create a fully formally verified STARK implementation. Another related project is VCV-io, which provides foundational oracle computing infrastructure for formal verification of various cryptographic protocols, many of which are dependencies of STARK itself.
Even more ambitious is evm-asm: this is a project that attempts to build a complete EVM implementation and formally verify it. Here, the security properties are not so clear. Simply put, its goal is to prove that this implementation is equivalent to another EVM implementation written in Lean; the latter pursues intuitiveness and readability to the greatest extent without considering specific operational efficiency.
Of course, theoretically, it is still possible for a situation to arise where we have ten EVM implementations that have all been proven equivalent but share the same fatal flaw, and this flaw somehow allows an attacker to transfer all ETH from an address they do not have permission to control. However, the probability of such an occurrence is much lower than if today a single EVM implementation had such a flaw. Another important security property that we only truly realized its significance after painful experience—resilience against DoS attacks—also tends to be relatively easy to specify.
Two other important directions are:
Byzantine fault tolerant consensus. In this area, formally defining all the expected security properties is similarly challenging. However, given that related bugs have always been very common, attempts at formal verification are still worthwhile. Thus, there is currently some ongoing work on Lean consensus implementations and their proofs.
Smart contract programming languages. Relevant examples include formal verification work in Vyper and Verity.
In all of these cases, a huge incremental value brought by formal verification is that these proofs are truly end-to-end. Many of the trickiest bugs are often interactive bugs that occur at the boundaries of two subsystems considered separately. For humans, making end-to-end reasoning about the entire system is too challenging; but automated rule-checking systems can achieve this.
Efficiency-focused formal verification
Let’s take a look at evm-asm. It is an EVM implementation.
But it is an EVM implementation directly written in RISC-V assembly language.
It is literally assembly in the literal sense.
Here is the ADD opcode:
The choice of RISC-V is because the currently built ZK-EVM provers typically work by proving RISC-V and compiling the Ethereum client to RISC-V. Therefore, if you directly write an EVM implementation in RISC-V, theoretically, it should be the fastest implementation you can get. RISC-V can also be run very efficiently on ordinary computers, and RISC-V laptops already exist. Of course, to achieve truly end-to-end, you must also perform formal verification on the RISC-V implementation itself or the arithmetic representation of the prover. But don't worry—such work is already underway.
Writing code directly in assembly is something we did frequently fifty years ago. Since then, we have gradually shifted to writing code in high-level languages. High-level languages sacrifice some efficiency, but in exchange, they allow for much faster code writing, and more importantly, they enable much quicker understanding of others' code—this is a necessary condition for security.
With the combination of formal verification and AI, we have the opportunity to "go back to the future." Specifically, it means having AI write assembly code and then provide formal proofs verifying that the assembly code has the properties we desire. At least, this desired property can simply be: it is completely equivalent to an implementation optimized for readability, written in some human-friendly high-level language.
In this way, there is no longer a need for a code object to balance between readability and efficiency. We will have two separate objects: one is the assembly implementation, optimized solely for efficiency and tailored to the specific execution environment's needs; the other is the safety claim or high-level language implementation, optimized solely for readability. Then we use a mathematical proof to verify the equivalence between the two. Users can first automatically verify this proof; thereafter, they only need to run that fast version.
This is very powerful. Yoichi Hirai calls it "the ultimate form of software development," and not without reason.
Formal verification is not a panacea
In cryptography and computer science, there is a tradition almost as old as formal methods themselves: criticizing formal methods or, more broadly, criticizing the reliance on "proofs." The related literature is full of practical examples. We can start with those simpler handwritten proofs in early cryptography. Menezes and Koblitz criticized them like this in 2004:
In 1979, Rabin proposed a cryptographic function that is "provably" secure in some sense, meaning it has a reductionist security property.
The so-called reductionist security claim is that anyone who can find the message m from the ciphertext y must also be able to factor n.
Shortly after Rabin proposed his encryption scheme, Rivest pointed out, ironically, that the very feature that provided it with extra security would lead the system to completely collapse in the face of another class of attackers called "chosen ciphertext" attackers. Specifically, if an attacker could somehow lure Alice into decrypting a ciphertext of their own choosing, then the attacker could follow the same process Sam used in the previous paragraph to factor n.
Menezes and Koblitz subsequently cited several examples. They collectively present a pattern: designing cryptographic protocols around being "easier to prove" often makes the protocols less "natural" and more prone to collapse in scenarios that the designers never considered.
Now, let’s return to machine-verifiable proofs and code. Here is an example from a 2011 paper where bugs were found in the formally verified C compiler:
We found the second CompCert issue reflected in two bugs. These two bugs would generate code like: stwu r1, -44432(r1)
Here, a very large PowerPC stack frame is being allocated. The problem is that the 16-bit displacement field has overflowed. CompCert's PPC semantics did not specify constraints on the width of this immediate value because it assumed the assembler would catch out-of-bounds values.
Let’s look at another paper from 2022:
In CompCert-KVX, commit e2618b31 fixes a bug: the "nand" instruction was printed as "and"; while "nand" would only be selected in the rare ~(a & b) mode. This bug was discovered through the compilation of randomly generated programs.
By today, in 2026, Nadim Kobeissi wrote about vulnerabilities in formal verification software in Cryspen:
In November 2025, Filippo Valsorda independently reported that libcrux-ml-dsa v0.0.3 would generate different public keys and signatures on different platforms given the same deterministic inputs. This bug resided in the _vxarq_u64 built-in function wrapper, which implements the XAR operation used in the SHA-3 Keccak-f permutation. The fallback path passed incorrect parameters to the shift operation, resulting in a corrupted SHA-3 hash on ARM64 platforms without hardware SHA-3 support. This is a Type I failure: the built-in function was marked as verified, while the entire NEON backend did not complete runtime safety or correctness proofs.
Moreover:
The libcrux-psq crate implements a post-quantum pre-shared key protocol. In the decrypt_out method, the AES-GCM 128 decryption path calls .unwrap() on the decryption result rather than continuing to propagate the error. A malformed ciphertext can cause the process to crash.
These four issues can be grouped into two categories:
The first category is that only parts of the code were verified because verifying the remaining parts was too difficult; the result proves that the unverified code is more prone to bugs than the author had anticipated, and these bugs are often more critical.
The second category is that the author forgot to explicitly specify some critical attribute that was needed to be proven.
Nadim's article classifies the failure modes of formal verification; he also lists other types of failures. For example, another major type is that the formal specifications themselves are incorrect, or the proofs contain erroneous claims that the build system silently accepts.
Finally, we can look at formal verification failures occurring at the interface between software and hardware. A common issue here is whether the verification system can withstand side-channel attacks. Even if you protected the message using a theoretically fully secure encryption method, if someone a few meters away can capture electrical fluctuations and extract your private key after hundreds of thousands of encryptions, then you are still not secure.
"Differential power analysis" is a well-understood example of such techniques.
Differential power analysis is a common side-channel attack. Source: Wikipedia
In the past, attempts were also made to prove that systems could withstand such attackers. However, any such proof requires some mathematical model about the attacker, and only then can you prove security under that model. Sometimes, the "d-probing model" is used: which assumes that the attacker can probe a known upper limit on the number of locations in the circuit. But the issue is that some forms of leakage cannot be captured by such a model.
A common issue observed in this article is transitional leakage: if the observed signal does not depend on the specific value at a certain location but rather on the change of this value, then often, you can recover the necessary information from the two values—the old value and the new value—rather than just relying on one value. The article also categorized other forms of leakage.
For decades, these criticisms of formal verification have, in turn, helped improve formal verification. Compared to the past, we are now more adept at being vigilant about such issues. Yet even today, it is still not perfect.
From a broader perspective, there is actually a common thread here: formal verification is powerful. But regardless of how marketing wraps it up as offering "provable correctness," so-called "provable correctness" fundamentally cannot prove that software or hardware is "correct" in the true sense.
For most people, "correct" roughly means: the behavior of that thing aligns with the user's understanding of the developer's intent.
And "secure" roughly means: that thing's behavior will not deviate from the user’s expectations in a way that harms their interests.
In both cases, correctness and security ultimately boil down to a comparison: one side being a mathematical object, the other being human intent or expectation. Strictly speaking, human intent and expectations are also mathematical objects—after all, the human brain is a part of the universe, and the universe follows physical laws; theoretically, if you have enough computing power, you can simulate them. But they are extremely complex mathematical objects that neither the computer nor we can truly understand or even read. For practical purposes, we can treat them as black boxes. The reason we retain some understanding of our own intents and expectations is that everyone has years of experience observing their thoughts and inferring those of others.
Also, because we cannot directly encode raw human intent into a computer, formal verification cannot prove the comparison between a system and human intent. Therefore, "provable correctness" and "provable security" do not actually prove what humans understand as "correctness" and "security"—there is no method to truly accomplish this until we can simulate the human brain.
So, what are the truly useful aspects of formal verification?
I tend to view test suites, type systems, and formal verification as different implementations of the same underlying programming language safety approach—which might also be the only truly meaningful way to put it. Their commonality lies in the redundancy of expressing our intentions in different ways, and then automatically checking whether these different statements are compatible with each other.
For instance, look at the following Python code:
Here, you’ve expressed your intent in three different ways:
First, directly: by implementing the Fibonacci formula in code.
Second, indirectly: by declaring that the inputs, outputs, and intermediate steps in the recursion are all integers through the type system.
Third, through a case-packaged approach: namely, test cases.
When running this file, the system will use these samples to check if the formula holds. The type checker can verify whether operations between types are compatible: adding two integers is a valid operation, and will yield another integer. Type systems are often very useful in physical computing: if you are calculating acceleration but the result is measured in m/s instead of m/s², you know you've made a mistake. Moreover, the "case-packaged" definition, where test cases are one of the methods, tends to align better with how humans process concepts compared to direct, explicit definitions.
The more different ways you can express your intent, the better; ideally, these ways should be sufficiently different from each other, forcing you to think about the same issue in different ways. Consequently, if all these expressions end up being mutually compatible, the probability of accurately expressing what you wanted is also higher.
The essence of secure programming is to express your intentions in different ways and then automatically verify whether these expressions are compatible with each other.
Formal verification can push this approach further. With formal verification, you can describe your intentions with virtually as many redundant ways as you wish; only when these descriptions are compatible will the program pass verification.
You can simultaneously produce an optimized implementation and a slower but human-readable one, and verify whether the two are consistent. You can also ask ten friends to list the mathematical attributes they believe this program should satisfy, and check whether the program meets them all; if not, further investigate whether it’s the program at fault or if that mathematical attribute itself is problematic. AI can make all of the above work extremely efficient.
How should I get started?
Realistically, you are unlikely to personally write proofs. The fundamental reason why formal methods have not truly proliferated is that most people find it challenging to grasp how to write these damn proofs.
Can you tell me what the following code means?
(If you’re curious, it is one of many sub-lemmas in a proof. This proof concerns a specific security claim about a variant of the SPHINCS signature: that is, unless a hash collision occurs, generating a signature for a specific message requires using a value that is at a higher position on a particular hash chain relative to any other message’s signature. Therefore, the information it needs cannot be computed from another signature.)
You do not need to hand-write the code and proof; instead, have AI help you write the program—either directly in Lean or, for speed, in assembly—and prove the various properties you want during this process.
One benefit of this task is that it is inherently self-validating, so you do not need to keep an eye on it constantly. You can let AI run it continuously for several hours. The worst-case scenario is simply that it spins its wheels without making progress; or, as my Leanstral once did, change the claim it was asked to prove to make its job easier.
What you ultimately need to check is whether the proposition it proved is indeed what you wanted to prove.
In this SPHINCS signature variant, the final statement is as follows:
This is actually barely close to the edge of "readable":
If the number generated from one hash digest (dig1) is not equal to the number generated from another hash digest (dig2), then the following statement cannot hold:
For every number, every digit of dig1 is less than or equal to the corresponding digit of dig2;
For every number, every digit of dig2 is less than or equal to the corresponding digit of dig1.
Here, what is being compared are the "extended numbers" (wotsFullDigits) generated through adding checksums. This means, inevitably, in some positions, the extended number of dig1 will be higher; and in others, the extended number of dig2 will be higher.
In writing proofs with large language models, I find Claude to be quite usable, and DeepSeek 4 Pro is also capable enough. Leanstral is a promising alternative: it is a smaller, open-source weight model, fine-tuned specifically for Lean writing. It has 119 billion parameters, but only activates 6 billion parameters per token, so it can run locally, albeit slowly—around 15 tokens per second on my laptop.
According to benchmark tests, Leanstral outperformed many much larger general models:
Based on my current personal experience, it is slightly weaker than DeepSeek 4 Pro but remains effective.
Formal verification will not solve all our problems. But if we wish to establish a model of internet security that does not require everyone to trust a few powerful organizations, then we need to be able to trust code— including trust in code even when facing powerful AI adversaries. AI-assisted formal verification can help us make important strides in that direction.
Like blockchain and ZK-SNARKs, AI and formal verification are also highly complementary technologies.
Blockchain brought open verifiability and censorship resistance at the cost of privacy and scalability; while ZK-SNARKs bring privacy and scalability back—indeed, even stronger than before.
AI enables large-scale code writing, but at the cost of reduced accuracy; while formal verification brings accuracy back—in fact, stronger than in the past.
By default, AI will generate a large amount of very rough code, leading to an increase in the number of bugs. Indeed, in some scenarios, allowing an increase in bugs is even the correct trade-off: if the impact of these bugs is light, then flawed software is better than no such software at all. But in this case, there remains an optimistic future for network security: software will continue to differentiate into "unsafe peripheral components" around a "security core."
These unsafe peripheral components will run in sandboxes and will only be granted the minimum permissions necessary to complete their tasks. The security core will manage everything. If the security core collapses, everything collapses—your personal data, your money, and more will be affected. But if a peripheral unsafe component fails, the security core can still protect you.
When it comes to the security core, we will not allow buggy code to proliferate. We will actively control the size of the security core to keep it small enough, or even shrink it further. Instead, we will invest all the additional capabilities brought by AI into enhancing the security of the security core itself, enabling it to bear the high trust burden in a highly digital society.
Your operating system kernel, or at least a portion of it, will be one such security core. Ethereum will be another. Ideally, at least in all non-high-performance intensive computing, the hardware you use will also become a third security core. Some IoT-related systems will be the fourth.
At least among these security cores, the old adage—that bugs are inevitable and you can only strive to discover them before the attackers do—will no longer hold. It will be replaced by a more hopeful world where we can achieve true security.
Of course, if you are willing to entrust your assets and data to software that is poorly written and might accidentally send them all into a black hole, you will still have that freedom.
免责声明：本文章仅代表作者个人观点，不代表本平台的立场和观点。本文章仅供信息分享，不构成对任何人的任何投资建议。用户与作者之间的任何争议，与本平台无关。如网页中刊载的文章或图片涉及侵权，请提供相关的权利证明和身份证明发送邮件到support@aicoin.com，本平台相关工作人员将会进行核查。
