As duas versões estão alinhadas bloco a bloco, pela ordem do texto: título, o essencial e depois parágrafo a parágrafo. Quando a tradução fundiu ou dividiu um parágrafo, a casa correspondente fica vazia — nunca aproximamos duas passagens a olho.
A computer result usually arrives with a question attached: did the program really run as claimed? Today the answer rests on trust in whoever ran it, backed by contracts, audits and logs. Zero-knowledge proofs offer another route. The program runs, and alongside its output it produces a short cryptographic certificate. Anyone holding it can confirm the result in milliseconds, without rerunning the program and without seeing the data it used.
Um resultado informático chega normalmente acompanhado de uma pergunta: o programa correu realmente como foi declarado? Hoje, a resposta assenta na confiança em quem o executou, apoiada em contratos, auditorias e registos. As provas de conhecimento nulo (zero-knowledge) oferecem outro caminho. O programa é executado e, a par do seu resultado, produz um certificado criptográfico curto. Quem o tiver pode confirmar o resultado em milissegundos, sem voltar a executar o programa e sem ver os dados que utilizou.
The idea dates from the 1980s, but three obstacles kept it from becoming a general tool. Producing a proof has historically taken millions of times more computation than running the program itself. Many systems also required developers to rewrite their program by hand as a cryptographic circuit, a fixed arithmetic description of one exact computation, a job that takes months and must be redone with every change. And many proofs rest on elliptic curves, which a sufficiently powerful quantum computer could break. Microsoft's Quantum Safe Program will move its products and services to post-quantum cryptography, a goal it recently accelerated to 2029.
A ideia data dos anos 1980, mas três obstáculos impediram que se tornasse uma ferramenta geral. Produzir uma prova exigiu historicamente milhões de vezes mais cálculo do que executar o próprio programa. Muitos sistemas obrigavam também os programadores a reescrever o programa à mão como circuito criptográfico, uma descrição aritmética fixa de um cálculo exato, tarefa que demora meses e tem de ser refeita a cada alteração. E muitas provas assentam em curvas elípticas, que um computador quântico suficientemente potente poderia quebrar. O Programa Quantum Safe da Microsoft vai migrar os seus produtos e serviços para criptografia pós-quântica, objetivo que foi recentemente acelerado para 2029.
Microsoft Research has worked on the problem for more than a decade. Its 2019 system Spartan returned to the sum-check approach and made it work for general programs without a trusted setup, a secret initial step whose leak would let anyone forge proofs. Phalanx, in 2021, exploited repetition, such as a processor running the same instruction cycle at every step, to prove computations an order of magnitude faster. Magnetar, announced on 15 October 2026, proves programs written in Rust, Go or C and rests its security only on standard hash functions.
A Microsoft Research trabalha no problema há mais de uma década. O seu sistema Spartan, de 2019, voltou à abordagem sum-check e tornou-a aplicável a programas gerais sem configuração de confiança, um passo inicial secreto cuja fuga permitiria a qualquer pessoa forjar provas. O Phalanx, em 2021, explorou a repetição, como um processador que executa o mesmo ciclo de instruções em cada passo, para provar cálculos uma ordem de grandeza mais depressa. O Magnetar, anunciado a 15 de outubro de 2026, prova programas escritos em Rust, Go ou C e assenta a sua segurança apenas em funções de hash padrão.
The headline figure is that Magnetar runs 10 to 39 times faster on average than the prior fastest comparable systems. Those numbers come from Microsoft Research's own announcement. The post describes a research system, and it does not mention any product built on it.
O principal valor é que o Magnetar é 10 a 39 vezes mais rápido, em média, do que os sistemas comparáveis mais rápidos anteriores. Estes números vêm do próprio anúncio da Microsoft Research. A publicação descreve um sistema de investigação e não menciona qualquer produto construído com base nele.
For AI agents acting on someone's behalf, the idea is that each action could carry a proof that it complied with the policy it was given. For regulated financial institutions, it would show that transactions were processed correctly without making them public. Microsoft Research presents both uses as possible once producing a proof is as routine as running the program, and it does not put a date on that point.
Para agentes de IA que atuam em nome de alguém, a ideia é que cada ação possa trazer uma prova de que cumpriu a política que lhe foi atribuída. Para instituições financeiras reguladas, mostraria que as transações foram processadas corretamente sem as tornar públicas. A Microsoft Research apresenta ambas as utilizações como possíveis quando produzir uma prova for tão rotineiro como executar o programa, mas não avança uma data para esse momento.