Original Title: A Shallow Dive into Formal Verification

Original Author: Vitalik

Translation: Peggy, BlockBeats

Editor's Note: As AI programming capabilities rapidly advance, software security is facing a new paradox: AI can more efficiently generate code and also more efficiently discover vulnerabilities. For the crypto industry, this issue is particularly critical. Once defects appear in smart contracts, ZK proofs, consensus algorithms, and on-chain asset systems, the consequences are often not just ordinary software bugs but irreversible fund losses and trust collapse.

What Vitalik discusses in this article is another path to code security in the AI era: formal verification. Simply put, it does not rely on human auditors to line-by-line check the code but rather formulates properties that the program should satisfy as mathematical propositions, and then uses machine-checkable proofs to verify if these properties hold true. In the past, formal verification has been relatively niche in the research and engineering fields due to its high barrier and cumbersome process. Still, with AI's ability to assist in code writing and proving, this methodology is regaining practical significance.

The key conclusion of the article is not that "formal verification can solve all security issues." On the contrary, Vitalik repeatedly emphasizes that so-called "provably secure" does not equal absolute security: proofs may overlook crucial assumptions, specifications themselves may be incorrect, unverified code, hardware boundaries, and side-channel attacks may also become new sources of risk. However, it still provides a more reliable security paradigm: expressing developers' intentions in multiple ways and then letting the system automatically check if these expressions are compatible with each other.

This is particularly important for Ethereum. The future of Ethereum will increasingly rely on complex underlying components, including STARKs, ZK-EVM, post-quantum signatures, consensus algorithms, and high-performance EVM implementations. The implementations of these systems are extremely complex, but their core security goals can often be formalized relatively clearly. It is precisely in such scenarios that AI-assisted formal verification may bring the most value: letting AI be responsible for writing efficient code and proofs, while humans are responsible for verifying whether the finally proven propositions truly correspond to their desired security goals.

From a more macro perspective, this article is also Vitalik's response to network security in the AI era. Faced with stronger AI attackers, the answer is not to abandon open source, smart contracts, or to re-depend on a few centralizing institutions but to compress critical systems into smaller, more verifiable, more trustworthy "security cores." AI may lead to a significant increase in rough code, but it may also make truly important code safer than ever.

The following is the original text:

Special thanks to Yoichi Hirai, Justin Drake, Nadim Kobeissi, and Alex Hicks for their feedback and review of this article.

Over the past few months, a new programming paradigm has been rapidly emerging in the Ethereum research and development community and many other corners of the computing world: developers directly writing code in very low-level languages, such as EVM bytecode, assembly language, or using Lean to write code and then validating its correctness through authoring machine-checkable mathematical proofs in Lean.

If done right, this approach has the potential to produce highly efficient code and may be much safer than traditional software development practices. Yoichi Hirai refers to it as the "ultimate form of software development." This article will attempt to explain the underlying logic of this approach: what formal verification of software can achieve, where its limitations 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 authoring of mathematical theorems in a way that can be automatically checked by a machine.

To provide a relatively simple yet still interesting example, we can look at a basic theorem about the Fibonacci sequence: every third number is even, and the other two are odd.

A simple way to prove this is by using mathematical induction, progressing three numbers at a time.

Let's first consider the base case. Let F1 = F2 = 1, F3 = 2. By direct observation, it can be seen that this proposition—"when i is a multiple of 3, Fi is even; otherwise, Fi is odd"—holds true before x = 3.

Next is the inductive step. Assume that the proposition holds true up to 3k+3; in other words, we already know the parity of F3k+1, F3k+2, F3k+3 are odd, odd, even, respectively. We can then determine the parity of the next set of three numbers:

Thus, we have completed the deduction from "known proposition holds up to 3k+3" to "confirmed proposition holds up to 3k+6." By repeating this reasoning, we can be confident that this pattern holds true for all integers.

This argument is persuasive to humans. But what if you need to prove something a hundred times more complex, and you really want to make sure you haven't made a mistake? In that case, you can construct a proof that is convincing to a computer as well.

It would look something like this:

1111₂

It's the same reasoning, just expressed in Lean. Lean is a programming language commonly used to write and verify mathematical proofs.

It looks very different from the "human version" proof I gave above, and for good reason: what is intuitive to a computer is completely different from what is intuitive to a human. Here, when we refer to a computer, we mean the old sense of a "computer" — a "deterministic" program composed of if/then statements, not a large language model.

In the proof above, you are not emphasizing the fact that fib(3k+4) = fib(3k+3) + fib(3k+2); you are emphasizing that fib(3k+3) + fib(3k+2) is odd, and Lean's mighty omega tactic will automatically marry this with its understanding of fib(3k+4).

In a more complex proof, you sometimes have to be explicit at every step: which mathematical law exactly allows you to take this step, and these laws sometimes come with some obscure names like Prod.mk.inj. But on the flip side, you can expand a huge polynomial expression in one step and simply write a line like omega or ring to complete the argument.

The lack of intuitiveness and the tediousness here is why machine-verifiable proofs, although existing for nearly 60 years, have always remained in a niche domain. But at the same time, many things that were almost impossible in the past are rapidly becoming feasible due to the swift progress of AI.

Verifying Computer Programs

At this point, you might be thinking: so we can have a computer verify a proof of a mathematical theorem, finally allowing us to determine which of those wild new discoveries about prime numbers are real and which are merely errors buried in a hundred-page PDF paper. Maybe we can even figure out if Shinichi Mochizuki's proof of the ABC Conjecture is correct! But beyond satisfying curiosity, what practical significance does this have?

There can be many answers. And for me, a very crucial answer is: verifying the correctness of computer programs, especially those involving cryptography or security. After all, a computer program is a mathematical object itself. Therefore, proving that a computer program will run in a certain way is essentially proving a mathematical theorem.

For example, suppose you want to prove whether encrypted communication software like Signal is truly secure. You can first articulate in a mathematical way what "security" means in this context. In general, what you want to prove is: under certain cryptographic assumptions, only the person possessing the private key can learn any information about the message content. In reality, there are certainly many important security properties.

And indeed, there is a team that is already trying to figure this out. One of the security theorems they proposed looks something like this:

Here is Leanstral's summary of the meaning of this theorem:

The passive_secrecy_le_ddh theorem is a tight reduction demonstrating that under the Random Oracle Model, the passive message secrecy of X3DH is at least as hard to break as the DDH assumption.

In other words, if an attacker could break the passive message secrecy of X3DH, then they could also break DDH. Since DDH is usually assumed to be a hard problem, X3DH can also be considered to withstand passive attacks.

This theorem proves that if an attacker can only passively observe Signal's key exchange messages, they cannot distinguish the final derived session key from a random key with an advantage greater than negligible probability.

If combined with a proof that AES encryption is correctly implemented, then you obtain a proof that the encryption mechanism of the Signal protocol can resist passive attackers.

Similar verification projects already exist, used to prove the security implementation of TLS and other browser-crypto components.

If you can achieve end-to-end formal verification, then what you're proving is not just that a protocol description is theoretically secure, but that the specific code run by users is also secure in practice. From a user's perspective, this significantly enhances the level of "trustlessness": to fully trust this piece of code, you don't need to painstakingly inspect the entire codebase line by line, just review those statements that have already been proven.

Of course, there are some very important caveats to keep in mind, especially about what the keyword "security" really means. It is easy for people to forget to prove truly essential claims; to encounter situations where the claim to be proven has no more concise description than the code itself; and to sneak in assumptions in the proof that eventually do not hold. It's also easy to argue that only a specific part of the system really needs formal proof, but in the end, another part, even down to the hardware level, gets hit by a critical vulnerability. Even Lean's own implementation may have bugs. But before delving into these headaches-inducing details, let's delve further into what kind of almost utopian prospect formal verification, if ideally and correctly done, might bring.

Security-Oriented Formal Verification

A bug in computer code is already a cause for concern.

When you place cryptocurrency into an immutable on-chain smart contract, a code bug becomes even more terrifying. Because once the code is flawed, North Korean hackers could automatically drain all your funds, and you would have almost no recourse.

When all of this is further enveloped in zero-knowledge proofs, a code bug becomes even more terrifying. Because if someone successfully compromises the zero-knowledge proof system, they could siphon off all the funds, and we might have no idea where the issue lies—worse still, we might not even know that the problem has occurred at all.

When we have powerful AI models, code bugs become even more terrifying. For instance, a model like Claude Mythos, after two years of refinement, might be able to autonomously uncover these vulnerabilities.

Confronted with this reality, some are advocating for the abandonment of the fundamental concept of smart contracts, even asserting that cyberspace can never truly become a domain where the defending side holds an asymmetric advantage over the attacking side.

Here are some quotes:

To fortify a system, you need to spend more tokens on finding vulnerabilities than attackers spend on exploiting them.

And also:

Our industry is built around deterministic code. Write code, test it, deploy it, and then know that it will function as intended—but based on my experience, this covenant is breaking down. Among the top operators of truly AI-native companies, the codebase has started to become something that you "believe will work," and this belief's corresponding probability can no longer be precisely articulated.

Even worse, some believe that the only solution is to move away from open source.

For cybersecurity, this paints a bleak future. This would be an especially bleak future for those who care about internet decentralization and freedom. The entire cypherpunk ethos fundamentally rests on this idea: in the realm of the internet, the defending side has the advantage. Erecting a digital "castle"—whether through encryption, signatures, or proofs—is meant to be much easier to do than to dismantle. If we lose this, then internet security will only come from economies of scale, from globally hunting down potential attackers, or more broadly, from a binary choice: either total dominance or annihilation.

I disagree with this assessment. I have a much more optimistic vision for the future of cybersecurity.

I believe that the significant challenge posed by the powerful AI-driven vulnerability discovery is indeed daunting, but it is a transitional challenge. Once the dust settles and we move into a new equilibrium, we will reach a state that is more favorable to the defense side than ever before.

Mozilla also agrees with this. Quoting them:

It may require reprioritizing all other affairs to dedicate in a sustained and focused manner to this mission. But there is light at the end of the tunnel. We are very proud to see how the team has stepped up to this challenge, and others will too. Our work is not yet done, but we have crossed a turning point and are beginning to see a future that is far beyond just “keeping up,” a better future. The defense finally has an opportunity to achieve a decisive victory.

…

The number of vulnerabilities is finite, and we are entering a world where we can finally discover all of them.

Now, if you search for the terms "formal" and "verification" using Ctrl+F in this Mozilla article, you will find that neither of the two words appears. The positive future of cybersecurity does not strictly rely on formal verification or any other single technology.

So, what does it rely on? Basically, on the image below:

Over the past few decades, many technologies have been driving the trend of “reducing the number of vulnerabilities”:

Type systems;

Memory-safe languages;

Software architecture improvements, including sandboxes, permission mechanisms, and more generally delineating a “trusted computing base” from “other code”;

Better testing methods;

Accumulated knowledge about secure and insecure coding patterns;

Increasingly pre-written and audited software libraries.

AI-assisted formal verification should not be seen as an entirely new paradigm but as a powerful accelerator: it is speeding up a trend and paradigm that has long been advancing.

Formal verification is not a panacea. But in certain scenarios, it is particularly applicable: when the goal is much simpler than the specific implementation. This is especially evident in some of the most challenging technologies to be deployed in the next major iteration of Ethereum, such as post-quantum signatures, STARKs, consensus algorithms, and ZK-EVM.

STARK is a very complex piece of software. However, the core security property it achieves is easy to understand and formalize: if you see a proof pointing to the hash H of program P, input x, and output y, then either the hash algorithm used by STARK has been broken, or P(x) = y. Hence, we have the Arklib project, which aims to create a formally verified STARK implementation. Another related project is VCV-io, which provides foundational oracle computation infrastructure that can be used for the formal verification of various cryptographic protocols, many of which are dependencies of STARK itself.

More ambitious is evm-asm: a project attempting to build a complete EVM implementation and formally verify it. Here, the security properties are not as clear. In simple terms, its goal is to prove that this implementation is equivalent to another EVM implementation written in Lean, which can strive for intuitiveness and readability without considering specific operational efficiency.

Of course, theoretically, it is still possible that we have ten EVM implementations all proven to be equivalent to each other, yet they all share a common fatal flaw that somehow allows an attacker to drain all ETH from an address they don't control. However, the probability of this scenario occurring is much lower compared to a single EVM implementation today having such a flaw. Another security property, anti DoS capability, which we truly realized the importance of only after a painful experience, can be relatively easily defined.

Two other important directions are:

Byzantine Fault Tolerant consensus. In this area, formalizing all desired security properties is also not easy. But given how prevalent related bugs have been, attempting formal verification is still worthwhile. Therefore, there is ongoing work on Lean consensus implementations and their proofs.

Smart contract programming languages. Examples include formal verification work in Vyper and Verity.

In all 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 boundary between two subsystems considered separately. For humans, it's too challenging to reason about the entire system end-to-end, but automated rule-checking systems can.

Efficiency-Oriented Formal Verification

Let's take another look at evm-asm. It is an EVM implementation.

But it is an EVM implementation written directly in RISC-V assembly language.

It is truly assembly in the literal sense.

Here is the ADD opcode:

The reason for choosing RISC-V is that the ZK-EVM prover currently being built typically proves RISC-V and works by compiling Ethereum clients to RISC-V. So, if you write an EVM implementation directly in RISC-V, theoretically, it should be the fastest implementation you can get. RISC-V can also be efficiently simulated on a regular computer, and RISC-V laptops already exist. Of course, to achieve true end-to-end, you still need to formally verify the RISC-V implementation itself or the arithmetic representation of the prover. However, do not worry—such work already exists.

Writing code directly in assembly is something we used to do fifty years ago. Since then, we have gradually moved towards 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, much faster understanding of others' code—which 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, let AI write assembly code, then write a formal proof to verify that this assembly code has the properties we want. At the very least, this target property can be: it is entirely equivalent to an implementation written in some human-friendly high-level language optimized for readability.

As a result, 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 for efficiency only, and adjusted according to the specific execution environment's requirements; the other is the security claim, or high-level language implementation, optimized only for readability. Then, we use a mathematical proof to prove the equivalence between the two. Users can automatically verify this proof once; thereafter, they only need to run the 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 ancient as the formal methods themselves: criticizing formal methods, or more broadly, criticizing reliance on "proof." There is a large volume of practical cases in the relevant literature. Let's start with those simpler handwritten proofs from the early days of cryptography. Menezes and Koblitz criticized them in 2004:

In 1979, Rabin proposed an encryption scheme that was, in a sense, "provably" secure, meaning it had a kind of reducibility security property.

The so-called reducibility security assertion is that anyone able to extract the message m from the ciphertext y must also be able to factorize n.

Shortly after Rabin proposed his encryption scheme, Rivest pointed out the irony that the very feature that brought it additional security would also lead to a total system compromise when faced with another type of attacker known as a "chosen ciphertext" attacker. Specifically, suppose an attacker can somehow induce Alice to decrypt a piece of ciphertext chosen by the attacker. Then, the attacker can proceed to factorize n using the same process Sam used in the previous paragraph.

Menezes and Koblitz later provided several examples that collectively exhibited a pattern: designing cryptographic protocols around "provable ease" often led to protocols that were less "natural" and more susceptible to failure in scenarios the designers hadn't even considered.

Now, let's return to machine-verifiable proofs and code. Here's an example from a 2011 paper where the authors found a bug in a formally verified C compiler:

Our second CompCert issue we encountered lies in two bugs. These two bugs would generate code like the following: stwu r1, -44432(r1)

Here, a large PowerPC stack frame is being allocated. The issue arises from a 16-bit shift field overflowing. CompCert's PPC semantics do not prescribe constraints on the immediate value width because it assumes the assembler will catch out-of-range values.

Turning to a paper from 2022:

In CompCert-KVX, commit e2618b31 fixed a bug where the "nand" instruction was being printed as "and"; "nand" is only selected for the rare ~(a & b) pattern. This bug was discovered by compiling randomly generated programs.

Fast forward to today, 2026, when Nadim Kobeissi described a vulnerability in the formally verified software Cryspen:

In November 2025, Filippo Valsorda independently reported that libcrux-ml-dsa v0.0.3, when given the same deterministic input, generates different public keys and signatures on different platforms. The bug lies within the _vxarq_u64 intrinsic function wrapper, which implements the XAR operation used in the Keccak-f permutation of SHA-3. The fallback path passed incorrect parameters to the shift operation, leading to a corruption of the SHA-3 digest on ARM64 platforms without hardware SHA-3 support. This is a Type I failure: the intrinsic function was marked as verified, while the entire NEON backend lacked a runtime security or correctness proof.

Also:

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 instead of propagating the error. A malformed ciphertext can cause the process to crash.

The above four issues can be categorized into two types:

The first type is when only part of the code is verified because verifying the rest is too difficult. The result shows that the unverified code is buggier than the author imagined and these bugs are often more critical.

The second type is when the author forgets to explicitly specify a key property that should have been proven.

Nadim's article classifies failure patterns in formal verification and also lists other failure types. For example, another major type is when the formal specification itself is incorrect, or the proof contains false claims that the built system silently accepts.

Finally, we can also examine formal verification failures occurring at the software-hardware boundary. A common issue here is whether the verification system can resist side-channel attacks. Even if you protect a message with a theoretically secure encryption method, if someone a few meters away can capture electrical fluctuations and extract your private key after hundreds of thousands of encryption operations, you are still insecure.

"Differential Power Analysis" is an example of this type of attack that is now well understood.

1111₇

Differential power analysis is a common side-channel attack. Source: Wikipedia

In the past, some have tried to prove that systems can withstand such attacks. However, any such proof requires a mathematical model of the attacker, and then you can prove security under this model. Sometimes, people use the "d-probing model," which assumes there is a known upper bound on the number of locations an attacker can probe in a circuit. The issue is that some forms of leakage cannot be captured by this model.

A common issue observed in this article is transitional leakage: if the observed signal does not depend on the specific value at a location but on the change in that value, many times you can extract the required information from two values—the old value and the new value—instead of relying on just one value. The article also categorizes other forms of leakage.

For decades, these criticisms of formal verification have, in turn, helped make formal verification better. Compared to the past, we are now more adept at being vigilant about these kinds of issues. However, even today, it is still not perfect.

Stepping back, there is actually a common thread here: formal verification is very powerful. But no matter how marketing may package it as being able to provide "provably correct" results, so-called "provably correct" results fundamentally cannot prove that software or hardware is truly "correct."

For most people, "correct" roughly means: the behavior of this thing aligns with the user's understanding of the developer's intent.

And "secure" roughly means: the behavior of this thing will not deviate from the user's expectations in a way that harms the user's interests.

In both cases, correctness and security ultimately boil down to a comparison: on one side, there is a mathematical object, and on the other side, there is human intent or expectation. Strictly speaking, human intent and expectation themselves are also mathematical objects—after all, the human brain is also part of the universe, and the universe follows physical laws; theoretically, you can simulate them as long as you have enough computing power. But they are extremely complex mathematical objects that neither computers nor ourselves can truly understand or even read. For practical purposes, we can treat them as black boxes. The reason we can still have some understanding of our own intent and expectation is simply because everyone has years of experience observing their own thoughts and inferring the thoughts of others.

Because we cannot directly input raw human intent into a computer, formal verification cannot prove a comparison between a system and human intent. Therefore, "provably correct" and "provably secure" results do not actually prove the "correctness" and "security" as understood by humans—there is no way to truly achieve this until we can simulate the human brain.

So, where is formal verification truly useful?

I tend to view test suites, type systems, and formal verification as different implementations of the same underlying programming language security method—this may also be the only truly plausible way to look at it. Their commonality lies in: redundantly specifying our intent in different ways and then automatically checking if these different specifications are compatible with each other.

For example, consider the following Python code:

Here, you have expressed your intent in three different ways:

First, directly expressed: by implementing the Fibonacci formula in code.

Second, Indirect Expression: Use the type system to indicate that the inputs, outputs, and intermediate steps in the recursive process are all integers.

Third, Adopt a "Case Pack" Approach: Essentially, this refers to test cases.

When you run this file, the system will use these examples to verify if the formula holds true. The type checker can then validate if the types are compatible: adding two integers is a valid operation and will result in another integer. Type systems are also often useful in physical computation: if you are calculating acceleration but the result is in m/s instead of m/s², you know where you went wrong. The "Case Pack" style definition, where test cases are one such example, often aligns more with how humans conceptualize information than direct, explicit definitions.

The more ways you have to express your intent, the better; ideally, these ways should be different enough to force you to think about the problem differently. In this way, if all these expressions end up being compatible with each other, the probability of truly expressing what you want to convey is higher.

The essence of secure programming is to express your intent in multiple different ways and then automatically verify if these expressions are compatible with each other.

Formal verification can further advance this approach. With formal verification, you can describe your intent in almost any number of redundant ways; the program will only pass verification when these descriptions are compatible with each other.

You can simultaneously write an optimized implementation and an inefficient but human-readable implementation, then verify if they are consistent. You can also have ten friends each list the mathematical properties they believe this program should satisfy, and then check if the program meets all of them; if it doesn't, you can further investigate whether it's the program that's wrong or if the mathematical property itself is flawed. AI can make all of the above tasks extremely efficient.

So, How Do I Get Started?

Realistically, you are unlikely to write the proof yourself. The reason formal methods have never really become widespread is that most people find it incredibly challenging to understand how to write these darn proofs.

Can you tell me what the following snippet of code means?

(If you are curious, it is one of many sub-lemmas in a proof. This proof is addressing a specific security claim of a variant of the SPHINCS signature: namely, that unless a hash collision occurs, generating a signature for a certain message that is at least as high up in a hash chain as any other message's signature requires information that cannot be derived from another signature.)

You don't need to handwrite code and proofs anymore; let AI write the program for you — you can write directly in Lean. If you want to prioritize speed, you can also write in assembly and prove various properties along the way.

One advantage of this task is that it is inherently self-verifying, so you don't need to watch over it constantly. You can let AI run continuously for several hours on its own. The worst-case scenario is that it spins in place without making progress, or, as my Leanstral once did, to make its job easier, it directly substituted the statement it was asked to prove.

What you ultimately need to check is whether the proposition it proves is indeed what you intend to prove.

In this variant of the SPHINCS signature scheme, the final statement is as follows:

This is actually quite close to the edge of "readable":

If a number generated by one hash digest (dig1) is not equal to a number generated by another hash digest (dig2), then the following statement is false:

For all digits, each digit of dig1 is less than or equal to the corresponding digit of dig2;

For all digits, each digit of dig2 is less than or equal to the corresponding digit of dig1.

What is being compared here is the "extended number" generated by adding a checksum (checksum). Inevitably, at some positions, dig1's extended number will be higher, while at other positions, dig2's extended number will be higher.

When it comes to writing proofs with large language models, I have found Claude to be good enough, DeepSeek 4 Pro to be quite competent. Leanstral, on the other hand, is a promising alternative: it is a smaller-scale, open-source-weighted model specifically fine-tuned for Lean writing. It has 119 billion parameters, but only activates 60 billion parameters per token, allowing it to run locally, although the speed is relatively slow — approximately 15 tokens per second on my laptop.

Based on benchmarks, Leanstral outperforms many much larger general models:

From my current personal experience, it is slightly weaker than DeepSeek 4 Pro, but still effective.

Formal verification won't solve all our problems. But if we want to establish an Internet security model that doesn't require everyone to trust a few powerful organizations, then we need to be able to trust code instead — even in the face of a powerful AI adversary. AI-assisted formal verification is a crucial step in that direction.

Just like blockchain and ZK-SNARKs, AI and formal verification are highly complementary technologies.

Blockchain brings open verifiability and resistance to censorship at the cost of privacy and scalability, while ZK-SNARKs reintroduce privacy and scalability — in fact, even stronger than before.

AI enables massive-scale code writing but at the expense of accuracy; formal verification then brings back accuracy — indeed, even stronger than before.

By default, AI tends to produce a significant amount of rough code, leading to an increase in bugs. Indeed, in some scenarios, increasing bugs may even be the right trade-off: if the impact of these bugs is minor, then having flawed software is better than having no such software. However, a hopeful future still exists for cybersecurity: software will continue to diverge into "insecure edge components" around a "secure core."

These insecure edge components will run in a sandbox and will only be granted the minimum permissions required to complete their tasks. The secure core will be responsible for managing everything. If the secure core fails, everything fails — your personal data, your money, and much more are affected. But if one of the insecure edge components malfunctions, the secure core can still protect you.

When it comes to the secure core, we won't allow buggy code to spread unchecked. We will actively control the size of the secure core, keeping it small enough, and possibly shrinking it further. Instead, we will invest all the additional capabilities brought by AI into enhancing the security of the secure core itself, enabling it to bear the heavy burden of trust in a highly digitized society.

Your operating system kernel, or at least a part of it, will be one of these secure cores. Ethereum will be another. Ideally, at least for all non-high-performance computing, the hardware you use will also become a third secure core. Certain IoT-related systems will be a fourth.

At least in these secure cores, the old adage — bugs are inevitable, and you can only strive to discover them before attackers do — will no longer hold. It will be replaced by a more hopeful world: where we can achieve true security.

Of course, you still have the freedom to entrust your assets and data to software that is poorly written and may even accidentally send them all into a black hole.

[Original Article]

Welcome to join the official BlockBeats community:

Telegram Subscription Group: https://t.me/theblockbeats

Telegram Discussion Group: https://t.me/BlockBeats_App

Official Twitter Account: https://twitter.com/BlockBeatsAsia