Lý do khiến bằng chứng không kiến thức (zero-knowledge proof) ngày càng được đổi mới và phát triển bền bỉ là gì?

Tác giả: LambdaClass

Biên dịch: mutourend; Yiping, IOSG Ventures

1. Mở đầu

Chứng minh kiến thức không (zero-knowledge succinct non-interactive argument of knowledge - zk-SNARKs) là một nguyên thủy mật mã mạnh mẽ, cho phép người chứng minh thuyết phục người xác minh rằng một khẳng định nào đó là đúng mà không tiết lộ bất kỳ thông tin nào ngoài chính khẳng định đó. Nhờ vào các ứng dụng trong tính toán riêng tư có thể kiểm chứng, chứng minh tính đúng đắn của việc thực thi chương trình máy tính và mở rộng blockchain, zk-SNARKs đã thu hút được sự chú ý rộng rãi. Chúng tôi tin rằng, như mô tả trong bài viết này, zk-SNARKs sẽ có tác động lớn đến việc định hình thế giới. zk-SNARKs bao gồm nhiều loại hệ thống chứng minh khác nhau, sử dụng các lược đồ cam kết đa thức khác nhau, các sơ đồ số học hóa, các chứng minh oracle tương tác hoặc chứng minh xác minh ngẫu nhiên. Tuy nhiên, những ý tưởng cơ bản này có thể bắt nguồn từ giữa những năm 1980.

Kể từ khi Bitcoin và Ethereum ra đời, sự phát triển của zk-SNARKs đã tăng tốc đáng kể vì chúng có khả năng mở rộng bằng cách sử dụng các chứng minh kiến thức không (thường được gọi là bằng chứng hiệu lực cho trường hợp sử dụng cụ thể này). zk-SNARKs đóng vai trò thiết yếu trong việc mở rộng quy mô blockchain. Như Ben-Sasson từng nói, những năm gần đây đã chứng kiến "bùng nổ tiền Cambri" của các bằng chứng mật mã. Mỗi hệ thống chứng minh đều có ưu điểm và nhược điểm riêng, và được thiết kế với những cân nhắc đặc thù. Sự tiến bộ về phần cứng, thuật toán, các bằng chứng mới và công cụ liên tục nâng cao hiệu suất, đồng thời thúc đẩy sự ra đời của các hệ thống mới. Nhiều hệ thống trong số này đã được triển khai thực tế, và chúng ta đang không ngừng phá vỡ các giới hạn. Liệu chúng ta có sở hữu một hệ thống chứng minh chung áp dụng cho mọi ứng dụng, hay sẽ có vài hệ thống phù hợp với các nhu cầu khác nhau? Chúng tôi cho rằng khả năng tồn tại một hệ thống chứng minh chi phối tất cả các hệ thống còn lại là rất nhỏ, lý do bao gồm:

1) Sự đa dạng của các ứng dụng.

2) Các loại hạn chế khác nhau (về bộ nhớ, thời gian xác minh, thời gian tạo chứng minh).

3) Nhu cầu về độ bền vững (nếu một hệ thống chứng minh bị phá vỡ, vẫn còn các hệ thống khác).

Mặc dù các hệ thống chứng minh đã thay đổi rất nhiều, nhưng chúng đều cung cấp một đặc điểm quan trọng: bằng chứng có thể được xác minh nhanh chóng. Việc sở hữu một tầng lớp có thể xác minh bằng chứng và dễ dàng thích nghi với các hệ thống chứng minh mới sẽ giải quyết được những khó khăn liên quan đến việc thay đổi tầng lớp cơ sở (như Ethereum). Bài viết này sẽ tổng quan các đặc điểm khác nhau của SNARKs:

1) Giả định mật mã: hàm băm chống va chạm, bài toán logarit rời rạc trên đường cong elliptic, kiến thức về số mũ.

2) Minh bạch so với thiết lập đáng tin cậy.

3) Thời gian tạo chứng minh: tuyến tính so với siêu tuyến tính.

4) Thời gian xác minh: hằng số, logarit, dưới tuyến tính, tuyến tính.

5) Kích thước bằng chứng.

6) Dễ dàng đệ quy.

7) Sơ đồ số học hóa.

8) Đa thức đơn biến so với đa thức đa biến.

Bài viết này sẽ khám phá nguồn gốc của SNARKs, một số khối xây dựng cơ bản cũng như sự trỗi dậy (và suy giảm) của các hệ thống chứng minh khác nhau. Bài viết không nhằm mục đích phân tích toàn diện các hệ thống chứng minh. Thay vào đó, chỉ tập trung vào những hệ thống có ảnh hưởng đối với chúng tôi. Tất nhiên, những bước phát triển này chỉ có thể xảy ra nhờ vào công việc và ý tưởng tuyệt vời của các tiên phong trong lĩnh vực này.

2. Kiến thức nền tảng

Chứng minh kiến thức không không phải là khái niệm mới. Các định nghĩa, nền tảng, định lý quan trọng, thậm chí cả các giao thức then chốt đều được thiết lập từ giữa những năm 1980. Một số ý tưởng và giao thức then chốt dùng để xây dựng SNARK hiện đại được đề xuất vào những năm 1990 (giao thức sumcheck), thậm chí trước cả khi Bitcoin ra đời (GKR năm 2007). Vấn đề chính khi sử dụng chúng lúc đó là thiếu các trường hợp sử dụng mạnh mẽ (Internet chưa phát triển mạnh vào những năm 1990) và yêu cầu về năng lực tính toán cần thiết.

1) Chứng minh kiến thức không: nguồn gốc (1985/1989).

Lĩnh vực chứng minh kiến thức không xuất hiện trong văn liệu học thuật qua bài báo của Goldwasser, Micali và Rackoff với tựa đề "The knowledge complexity of interactive proof systems". Để tìm hiểu thêm về nguồn gốc, có thể xem video ZKP MOOC Lecture 1: Introduction and History of ZKP (tháng 1 năm 2023). Bài báo này giới thiệu các khái niệm hoàn thiện, đáng tin cậy và tính chất kiến thức không, đồng thời đưa ra các cấu trúc cho quadratic residuosity và quadratic non-residuosity.

2) Giao thức Sumcheck (1992).

Giao thức sumcheck được Lund, Fortnow, Karloff và Nisan đề xuất trong bài báo "Algebraic Methods for Interactive Proof Systems" năm 1992. Đây là một trong những khối xây dựng quan trọng nhất cho các chứng minh tương tác ngắn gọn. Nó giúp giảm yêu cầu tính tổng giá trị đánh giá (evaluate) của một đa thức đa biến xuống còn một lần đánh giá duy nhất tại một điểm ngẫu nhiên.

3) Goldwasser-Kalai-Rothblum (GKR) (2007).

Giao thức GKR (xem bài báo "Delegating Computation: interactive Proofs for Muggles") là một giao thức tương tác, trong đó người chứng minh chạy tuyến tính theo số cổng của mạch, trong khi người xác minh chạy dưới tuyến tính theo kích thước mạch. Trong giao thức, người chứng minh và người xác minh đồng thuận về một mạch hữu hạn trường với độ sâu d dd, fan-in hai phép toán, trong đó tầng d dd tương ứng với tầng đầu vào, tầng 0 00 tương ứng với tầng đầu ra. Giao thức bắt đầu từ một tuyên bố về đầu ra của mạch, sau đó được giản lược thành tuyên bố về các giá trị ở tầng trước. Sử dụng đệ quy, nó có thể chuyển đổi thành tuyên bố về đầu vào của mạch, từ đó dễ dàng kiểm tra. Những bước giản lược này được thực hiện thông qua giao thức sumcheck.

4) Sơ đồ cam kết đa thức KZG (2010).

Kate, Zaverucha và Goldberg giới thiệu sơ đồ cam kết đa thức sử dụng nhóm ghép đôi song tuyến tính trong bài báo "Constant-Size Commitments to Polynomials and Their Applications" năm 2010. Cam kết bao gồm một phần tử nhóm duy nhất, và người cam kết có thể hiệu quả mở cam kết tại bất kỳ điểm đánh giá đúng nào của đa thức. Ngoài ra, nhờ kỹ thuật batching, có thể mở nhiều lần đánh giá cùng lúc. Cam kết KZG là một trong những khối xây dựng cơ bản cho nhiều SNARK hiệu quả như Pinocchio, Groth16 và Plonk. Nó cũng là cốt lõi của EIP-4844. Để trực quan hóa kỹ thuật batching, có thể tham khảo cầu nối ZK từ Mina sang Ethereum.

3. SNARK thực tiễn sử dụng đường cong elliptic

Cấu trúc SNARK thực tiễn đầu tiên xuất hiện vào năm 2013. Những cấu trúc này yêu cầu một bước xử lý trước để tạo khóa chứng minh và xác minh, và là đặc thù cho chương trình/mạch cụ thể. Những khóa này có thể rất lớn và phụ thuộc vào các tham số bí mật mà các bên không biết; nếu không, có thể làm giả bằng chứng. Việc chuyển đổi mã thành dạng có thể chứng minh đòi hỏi phải biên dịch mã thành hệ thống ràng buộc đa thức. Ban đầu, điều này phải được thực hiện thủ công, vừa mất thời gian vừa dễ sai sót. Những tiến bộ trong lĩnh vực này cố gắng giải quyết một số vấn đề chính:

1) Có người chứng minh hiệu quả hơn.

2) Giảm lượng xử lý trước.

3) Có các thiết lập phổ quát thay vì riêng biệt cho từng mạch.

4) Tránh sử dụng thiết lập đáng tin cậy.

5) Phát triển phương pháp mô tả mạch bằng ngôn ngữ cấp cao thay vì viết thủ công các ràng buộc đa thức.

Hiện tại, các sơ đồ SNARK thực tiễn sử dụng đường cong elliptic bao gồm:

1) Pinocchio (2013)

2) Groth 16 (2016)

3) Bulletproofs & IPA (2016)

4) Sonic, Marlin, và Plonk (2019)

5) Lookups (2018/2020)

6) Spartan (2019)

7) HyperPlonk (2022)

8) Sơ đồ gấp (Folding schemes) (2008/2021)

3.1 Pinocchio (2013)

Pinocchio (xem bài báo "Pinocchio: Nearly Practical Verifiable Computation") là zk-SNARK thực tiễn và khả dụng đầu tiên. SNARK dựa trên chương trình số học bậc hai (quadratic arithmetic programs - QAP). Kích thước bằng chứng ban đầu là 288 byte. Chuỗi công cụ của Pinocchio cung cấp trình biên dịch từ mã C sang mạch số học, sau đó chuyển tiếp thành QAP. Giao thức yêu cầu người xác minh tạo khóa riêng biệt cho từng mạch. Nó sử dụng ghép đôi đường cong elliptic để kiểm tra phương trình. Độ phức tạp tiệm cận của việc tạo bằng chứng và thiết lập khóa tỷ lệ tuyến tính với kích thước tính toán, trong khi thời gian xác minh tỷ lệ tuyến tính với kích thước đầu vào và đầu ra công cộng.

3.2 Groth 16 (2016)

Bài báo năm 2016 của Groth "On the Size of Pairing-based Non-interactive Arguments" giới thiệu một kiểu lập luận kiến thức mới, cải thiện hiệu suất cho các vấn đề được mô tả bởi R1CS. Nó có kích thước bằng chứng nhỏ nhất (chỉ ba phần tử nhóm) và quá trình xác minh nhanh với ba phép ghép đôi. Nó cũng liên quan đến bước xử lý trước để lấy chuỗi tham chiếu cấu trúc. Nhược điểm chính là mỗi chương trình cần chứng minh đều yêu cầu một thiết lập đáng tin cậy khác nhau, điều này khá bất tiện. Groth16 từng được sử dụng trong ZCash. Chi tiết thêm có thể xem trong blog "An overview of the Groth 16 proof system".

3.3 Bulletproofs & IPA (2016)

Một trong những điểm yếu của PCS KZG là nó cần thiết lập đáng tin cậy. Bootle và cộng sự trong bài báo năm 2016 "Efficient Zero-Knowledge Arguments for Arithmetic Circuits in the Discrete Log Setting" giới thiệu hệ thống lập luận zero-knowledge hiệu quả cho các mở cam kết Pedersen thỏa mãn mối quan hệ tích trong (inner product). Hệ thống chứng minh tích trong có người chứng minh tuyến tính, giao tiếp và tương tác logarithmic, nhưng xác minh mất thời gian tuyến tính. Họ cũng phát triển một sơ đồ cam kết đa thức không cần thiết lập đáng tin cậy. Cả Halo 2 và Kimchi đều áp dụng tư tưởng từ IPA PCS.

3.4 Sonic, Marlin, và Plonk (2019)

Sonic, Plonk và Marlin giải quyết vấn đề thiết lập đáng tin cậy cho từng chương trình trong Groth16 bằng cách giới thiệu chuỗi tham chiếu cấu trúc phổ quát và có thể cập nhật. Marlin cung cấp hệ thống chứng minh dựa trên R1CS, là cốt lõi của Aleo.

Plonk giới thiệu một sơ đồ số học hóa mới (sau này gọi là Plonkish), và sử dụng kiểm tra tích lớn (grand-product check) cho các ràng buộc sao chép (copy constraints). Plonkish còn cho phép đưa vào các cổng chuyên biệt cho một số thao tác, còn gọi là cổng tùy chỉnh. Nhiều dự án có phiên bản Plonk tùy chỉnh, bao gồm Aztec, ZK-Sync, Polygon ZKEVM, Kimchi của Mina, Plonky2, Halo 2 và Scroll. Có thể tham khảo blog "All you wanted to know about Plonk".

3.5 Tìm kiếm (Lookups) (2018/2020)

Gabizon và Williamson giới thiệu plookup vào năm 2020, sử dụng kiểm tra tích lớn để chứng minh rằng một giá trị nhất định nằm trong bảng giá trị được tính toán trước. Mặc dù trước đó đã có các lập luận lookup được đề xuất trong Arya, nhưng cấu trúc của nó yêu cầu xác định multiplicity của các lần lookup, kém hiệu quả. Bài báo PlonkUp cho thấy cách đưa lập luận plookup vào Plonk. Vấn đề với các lập luận lookup này là chúng buộc người chứng minh phải trả phí cho toàn bộ bảng, bất kể họ thực hiện bao nhiêu lần tìm kiếm. Điều này có nghĩa chi phí cho các bảng lớn là rất lớn, và đã có rất nhiều nỗ lực nhằm giảm chi phí người chứng minh xuống mức tỷ lệ với số lượng lần lookup được sử dụng.

Haböck giới thiệu LogUp, sử dụng đạo hàm logarit để chuyển đổi kiểm tra tích thành tổng các nghịch đảo. LogUp cực kỳ quan trọng đối với hiệu suất của Polygon plonky2 ZKEVM ("Beyond Limits: Pushing the Boundaries of ZK-EVM"), nơi cần chia toàn bộ bảng thành nhiều mô-đun STARK. Các mô-đun này phải được liên kết đúng cách, và việc tra cứu chéo bảng củng cố thao tác này. Việc ra mắt LogUp-GKR tận dụng giao thức GKR để cải thiện hiệu suất của LogUp. Caulk là lập luận lookup đầu tiên có thời gian người chứng minh dưới tuyến tính so với kích thước bảng, với thời gian xử lý trước là O(N log N) và lưu trữ là O(N), trong đó N là kích thước bảng. Sau đó xuất hiện thêm nhiều sơ đồ khác như Baloo, flookup, cq và caulk+. Lasso đề xuất nhiều cải tiến, tránh việc commit vào bảng khi bảng có cấu trúc nhất định. Hơn nữa, người chứng minh Lasso chỉ trả phí cho các mục bảng mà họ truy cập trong thao tác lookup. Jolt tận dụng Lasso để chứng minh việc thực thi máy ảo thông qua tra cứu.

3.6 Spartan (2019)

Spartan cung cấp IOP cho các mạch được mô tả bằng R1CS, tận dụng các thuộc tính của đa thức đa biến và giao thức sumcheck. Với một sơ đồ cam kết đa thức phù hợp, nó tạo ra SNARK minh bạch có người chứng minh chạy thời gian tuyến tính.

3.7 HyperPlonk (2022)

HyperPlonk được xây dựng dựa trên tư tưởng Plonk sử dụng đa thức đa biến. Thay vì dựa vào thương số để kiểm tra việc thực thi ràng buộc, nó dựa vào giao thức sumcheck. Nó cũng hỗ trợ các ràng buộc bậc cao mà không làm tổn hại đến thời gian chạy của người chứng minh. Vì dựa trên đa thức đa biến, nên không cần thực hiện FFT, và thời gian chạy của người chứng minh tỷ lệ tuyến tính với kích thước mạch. HyperPlonk giới thiệu IOP hoán vị mới phù hợp với các trường nhỏ và giao thức mở batch dựa trên sumcheck, giúp giảm khối lượng công việc của người chứng minh, kích thước bằng chứng và thời gian của người xác minh.

3.8 Sơ đồ gấp (Folding schemes) (2008/2021)

Nova giới thiệu tư tưởng về sơ đồ gấp, một phương pháp mới để thực hiện tính toán có thể kiểm chứng tăng dần (IVC). Khái niệm IVC có thể bắt nguồn từ Valiant, người đã chỉ ra cách kết hợp 2 bằng chứng dài k kk thành một bằng chứng dài k kk. Ý tưởng là có thể chứng minh bất kỳ phép tính chạy lâu dài nào bằng cách chứng minh đệ quy rằng việc thực thi từ bước i ii đến bước i+1 i+1i+1 là đúng, đồng thời xác minh rằng bằng chứng chuyển tiếp từ bước i−1 i-1i−1 đến bước i ii là đúng.

Nova xử lý tốt các phép tính đồng nhất; sau đó được mở rộng để xử lý các loại mạch khác nhau thông qua việc giới thiệu Supernova. Nova sử dụng phiên bản lỏng lẻo của R1CS và hoạt động trên các đường cong elliptic thân thiện. Việc sử dụng các chu kỳ đường cong thân thiện (ví dụ: đường cong Pasta) để thực hiện IVC cũng được áp dụng trong Pickles, khối xây dựng chính của Mina nhằm đạt được trạng thái ngắn gọn. Tuy nhiên, tư tưởng gấp khác với việc xác minh SNARK đệ quy. Tư tưởng tích lũy (accumulator) liên hệ sâu sắc hơn với khái niệm batching proofs. Halo giới thiệu khái niệm tích lũy như một giải pháp thay thế cho việc kết hợp chứng minh đệ quy. Protostar cung cấp sơ đồ IVC không đồng nhất cho Plonk, hỗ trợ các cổng bậc cao và tra cứu vector.

4. SNARK sử dụng hàm băm chống va chạm

Cùng thời điểm với việc phát triển Pinocchio, xuất hiện một số ý tưởng tạo ra sơ đồ mạch/số học có thể chứng minh tính đúng đắn của việc thực thi máy ảo. Mặc dù việc số học hóa máy ảo có thể phức tạp hoặc kém hiệu quả hơn so với việc viết mạch chuyên dụng cho một số chương trình nhất định, nhưng nó mang lại một lợi ích: bất kỳ chương trình nào, dù phức tạp đến đâu, cũng có thể được chứng minh bằng cách chứng minh rằng nó được thực thi đúng trong máy ảo. Ý tưởng trong TinyRAM sau này được cải tiến thông qua việc thiết kế Cairo vm và các máy ảo tiếp theo (như zk-evms hoặc zkvms phổ quát). Việc sử dụng hàm băm chống va chạm loại bỏ nhu cầu về thiết lập đáng tin cậy hoặc sử dụng các phép toán đường cong elliptic, nhưng đổi lại là các bằng chứng dài hơn.

1) TinyRAM (2013)

Trong "SNARKs for C", một SNARK dựa trên PCP đã được phát triển để chứng minh tính đúng đắn của việc thực thi chương trình C, chương trình này được biên dịch thành TinyRAM (máy tính tập lệnh rút gọn). Máy tính này sử dụng kiến trúc Harvard, với bộ nhớ truy cập ngẫu nhiên cấp byte. Tận dụng tính không tất định, kích thước mạch có quan hệ tựa tuyến tính (quasilinear) với kích thước tính toán, do đó hiệu quả xử lý các vòng lặp tùy ý, luồng điều khiển và truy cập bộ nhớ phụ thuộc dữ liệu.

2) STARKs (2018)

STARKs được đề xuất bởi Ben Sasson và cộng sự vào năm 2018. Chúng đạt được kích thước bằng chứng O(log²n), có người chứng minh và người xác minh nhanh, không cần thiết lập đáng tin cậy, và được coi là an toàn hậu lượng tử. STARKs lần đầu tiên được sử dụng bởi Starkware/Starknet cùng với máy ảo Cairo. Các thành phần then chốt bao gồm:

• Biểu diễn trung gian đại số (AIR)

• Và giao thức FRI (Fast Reed-Solomon Interactive Oracle Proof of Proximity).

STARKs cũng được sử dụng bởi các dự án khác (Polygon Miden, Risc0, Winterfell, Neptune), hoặc các biến thể của nó (Boojum của ZK-Sync, Plonky2, Starky).

3) Ligero (2017)

• Ligero giới thiệu một hệ thống chứng minh có kích thước bằng chứng O(√n), trong đó n là kích thước mạch. Nó sắp xếp các hệ số đa thức thành dạng ma trận và sử dụng các mã tuyến tính (linear codes).

• Brakedown được xây dựng dựa trên Ligero và giới thiệu tư tưởng về sơ đồ cam kết đa thức độc lập với miền.

5. Một số tiến triển mới trong ZKP

Việc sử dụng các hệ thống chứng minh khác nhau trong sản xuất đã cho thấy ưu điểm của từng phương pháp và dẫn đến các phát triển mới. Ví dụ, số học Plonkish cung cấp một cách đơn giản để bao gồm các cổng tùy chỉnh và các lập luận lookup; FRI với tư cách là PCS thể hiện hiệu suất vượt trội, dẫn đầu Plonky. Tương tự, việc sử dụng kiểm tra tích lớn trong AIR (dẫn đến AIR ngẫu nhiên có xử lý trước) đã cải thiện hiệu suất và đơn giản hóa các lập luận truy cập bộ nhớ. Các cam kết dựa trên hàm băm đã trở nên phổ biến — nhờ tốc độ hàm băm trong phần cứng hoặc việc giới thiệu các hàm băm thân thiện với SNARK mới.

1) Các sơ đồ cam kết đa thức mới (2023)

Cùng với sự xuất hiện của các SNARK hiệu quả dựa trên đa thức đa biến (như Spartan hoặc HyperPlonk), ngày càng có nhiều sự quan tâm đến các sơ đồ cam kết mới phù hợp với loại đa thức này. Binius, Zeromorph và Basefold đều đề xuất các hình thức mới tập trung vào đa thức đa tuyến tính. Binius có ưu điểm là không tốn chi phí để biểu diễn các kiểu dữ liệu (trong khi nhiều hệ thống chứng minh sử dụng ít nhất các phần tử trường 32 bit để biểu diễn một bit đơn lẻ) và hoạt động trên trường nhị phân. Cam kết Binius dựa trên Brakedown, được thiết kế để độc lập với miền. Basefold mở rộng FRI ra ngoài các mã Reed-Solomon, từ đó tạo thành PCS độc lập với miền.

2) Hệ thống ràng buộc tùy chỉnh được (Customizable Constraint Systems - CCS) (2023)

CCS khái quát hóa R1CS, đồng thời nắm bắt được số học R1CS, Plonkish và AIR mà không cần chi phí bổ sung. Kết hợp CCS với IOP Spartan tạo ra SuperSpartan, hỗ trợ các ràng buộc bậc cao mà không khiến người chứng minh phải chịu chi phí mật mã tăng theo bậc ràng buộc. Đặc biệt, SuperSpartan tạo ra SNARK cho AIR với người chứng minh thời gian tuyến tính.

6. Kết luận

Bài viết này mô tả sự tiến bộ của SNARK kể từ giữa những năm 1980. Những bước tiến trong khoa học máy tính, toán học và phần cứng, cộng với sự ra đời của blockchain, đã thúc đẩy sự ra đời của các SNARK mới và hiệu quả hơn, mở ra cánh cửa cho nhiều ứng dụng có thể thay đổi xã hội chúng ta. Các nhà nghiên cứu và kỹ sư đã đề xuất các cải tiến và điều chỉnh SNARK theo nhu cầu riêng của họ, tập trung vào kích thước bằng chứng, sử dụng bộ nhớ, thiết lập minh bạch, an toàn hậu lượng tử, thời gian người chứng minh và thời gian người xác minh.

Mặc dù ban đầu có hai dòng chính (SNARK và STARK), ranh giới giữa chúng đã bắt đầu mờ nhòa, với nỗ lực kết hợp ưu điểm của các hệ thống chứng minh khác nhau. Ví dụ, kết hợp các sơ đồ số học khác nhau với các sơ đồ cam kết đa thức mới. Có thể dự đoán rằng các hệ thống chứng minh mới sẽ tiếp tục xuất hiện với hiệu suất ngày càng cao, trong khi các hệ thống cần thời gian để thích nghi sẽ khó theo kịp những phát triển này, trừ khi các công cụ có thể dễ dàng sử dụng mà không cần thay đổi một số cơ sở hạ tầng cốt lõi.