A new form of computing

Every result a computer produces comes with an implicit question: did the program run as claimed and produce correct outputs? Today, answering that question often requires a degree of trust alongside verification. We trust the operator, the vendor, the counterparty, or the agent, and we rely on contracts, audits, and logs to establish that trust. 

Zero-knowledge proofs offer a fundamentally different approach to establishing trust. A program runs, and along with its output it produces a short proof, a cryptographic certificate that this program, on these inputs, produced this output. The proof is small and fast to check. Whoever receives it can confirm the result in milliseconds without rerunning the program, and can pass the proof on to anyone else who needs the same assurance. With the zero-knowledge property, the proof also reveals nothing about inputs that should stay private.

This changes what correctness means in the real world. A result no longer has to be trusted because of who produced it. It can be checked because of what accompanies it. An AI agent acting on someone’s behalf could attach a proof that each action complied with the policy it was given. Regulated financial institutions could prove that transactions were processed correctly without making their transactions public. These become possible once producing a proof is as routine as running the program.

Three grand challenges

Zero-knowledge proofs were invented in the 1980s, and the ideas behind proving program execution have been around nearly as long. What has kept them from becoming a general tool is three challenges that have resisted being solved at the same time.

Efficiency. Producing a proof has historically taken millions of times more computation than running the program itself. Years of research have brought that overhead down, but the fastest systems have achieved their speed by making compromises elsewhere.

Generality and usability. Many proof systems require developers to manually rewrite their program as a cryptographic circuit, which is a fixed arithmetic description of that exact computation. This takes months. Every change to the application means a new circuit, and the translation is itself a frequent source of security bugs. A general-purpose alternative is to prove the execution of an ordinary processor, so that any compiled program can be proven as written. Until recently, that generality came at a steep cost in speed or security. 

Security. A proof is only as strong as the cryptography beneath it. Many proof systems rest on elliptic curves, which can be broken by a sufficiently powerful quantum computer. Microsoft is addressing this problem with its Quantum Safe Program, which will move its products and services to post-quantum cryptography, a goal it recently accelerated to 2029. Post-quantum proof systems already exist, but some rest on lattice assumptions, and most rest on new cryptographic functions invented to reduce the cost of proving. These new cryptographic functions have not faced the decades of scrutiny given to the cryptography protecting today’s internet, and some rest on mathematical conjectures about error-correcting codes that have not been proven. They have bought their speed with strong assumptions. 

PODCAST SERIES

AI Testing and Evaluation: Learnings from Science and Industry

Discover how Microsoft is learning from other domains to advance evaluation and testing as a pillar of AI governance.

Listen now

Opens in a new tab

More than a decade of work

For more than a decade, Microsoft Research has worked on making zero-knowledge proofs and verifiable computing practical. Early research followed two approaches, both practical only for small programs. The first (opens in new tab) (opens in new tab)lets a verifier check a long computation through a short conversation with the prover using a technique called the sum-check protocol (opens in new tab), but this applied only to computations with a particular layered structure. The second (opens in new tab) (opens in new tab)used elliptic-curve cryptography to create very small proofs for almost any computation. But this requires a one-time trusted setup involving secret information which, if leaked, could allow anyone to forge proofs. This approach is also vulnerable to quantum computers.

In 2019, a new zero-knowledge proof system called Spartan returned to the sum-check approach and made it work for general-purpose programs without a trusted setup. Spartan can also be instantiated with different cryptographic building blocks. That flexibility is what later allowed the proof system to be built on hash functions alone. A sequence of results then filled in the remaining pieces: 

• Phalanx (opens in new tab), in 2021, showed how to exploit repetition, such as a processor running the same instruction cycle on every step, to prove computations an order of magnitude faster than Spartan. Magnetar’s processor description is built on this idea.  
• Nova (opens in new tab), HyperNova (opens in new tab), NeutronNova (opens in new tab), Neo and SuperNeo (opens in new tab) showed that stopping Spartan’s proving early, and folding the partial results together, makes it practical to prove computations of any size at far lower cost.
• Brakedown (opens in new tab), in 2021, introduced a fast hash-based commitment scheme and combined it with Spartan, giving the first Spartan variant whose security rests on standard hash functions. 
• Spice (opens in new tab), Lasso (opens in new tab), Nebula (opens in new tab), and then Twist and Shout (opens in new tab) made the memory operations at the heart of a general-purpose processor inexpensive to prove, and Jolt (opens in new tab) showed that combining them with Spartan can efficiently prove the execution of a complete processor.
• Earlier this year, Vega (opens in new tab) applied this line of work to digital identity, proving facts from a government credential in under a tenth of a second.
• More recently, BinarySpartan (opens in new tab) brought Spartan to binary fields, where a processor’s logic and standard hash functions can be efficiently expressed. BinarySpartan also relies on Ligerito (opens in new tab), a Brakedown-style commitment scheme with much shorter proofs, and on ring switching (opens in new tab), which makes it efficient to commit to vectors of bits. 

Each of these solved a piece of the problem. Magnetar is where the pieces come together.

Magnetar

Magnetar is a zero-knowledge virtual machine, or zkVM, and it makes major progress on all three challenges at once.

It is general-purpose. Magnetar proves the execution of RISC-V, an open processor architecture with mature compilers for every mainstream language. A developer writes a program in Rust, Go, or C, compiles it as usual, and Magnetar proves it as written. Consider what this means in practice. A business policy, a data pipeline, or an interpreter for the Ethereum Virtual Machine (EVM) is just a program, and the engineers who already maintain it can prove their executions exactly as written. As a result, proving stops being a specialist activity. 

It is faster than prior systems in the same class. Magnetar proves 7.2 to 8.7 million processor instructions per second on a laptop. Across 15 benchmark programs, from cryptographic hashing to token transfers inside a small EVM interpreter, it is 10 to 39 times faster on average than the fastest existing zkVMs on the same machine, and more than 300 times faster than two others on a token-transfer benchmark. An optimized Magnetar proves 9.5–12.8 million cycles per second, which increases each speedup reported here by about 1.3×. Its proofs verify in about 12 milliseconds. 

Its security rests on standard cryptography. Magnetar depends on a standard hash function such as SHA-256 or SHA-3, the same primitives that already protect every organization’s systems. It requires no elliptic curves, no lattices, no special-purpose hash functions, no trusted setup, and no unproven conjecture about error-correcting codes. Hash functions are the most thoroughly studied primitives in the cryptographic toolkit, and they are the basis of the stateless hash-based signatures that NIST standardized as its own conservative post-quantum option. For a system that must still be trustworthy in many decades to come, relying only on standard hash functions removes a cryptographic migration from the roadmap. 

The same design decision pays a second dividend. Checking a Magnetar proof consists mostly of evaluating standard hash functions and binary-field arithmetic, which are exactly the operations Magnetar proves efficiently. Verifying a proof is therefore an ordinary workload for it. This is what allows Magnetar to prove computations of any size, by proving them in pieces and then combining the pieces. This also allows Magnetar to prove a long-running system such as a ledger or a blockchain.

The technical paper gives the full design, security analysis, and measurements.

Looking ahead

Magnetar advances zero-knowledge proofs and verifiable computing to a stage where they can be built on the cryptography that organizations already trust, at speeds that make it usable, by engineers who write normal code. Magnetar enables a future where cryptographic proofs are a routine output of computation. We expect that technology leaders will stop asking whether proofs of execution are practical and focus instead on which results would they prefer to verify rather than taking on trust.

If you’re interested in exploring how zero-knowledge proofs can support your use case, we’d love to hear from you (opens in new tab).

The post Proof-based general-purpose computing with Magnetar appeared first on Microsoft Research.

AI makes it possible to generate code faster than teams can understand and support it. In this episode, Honeycomb cofounder and CTO Charity Majors joined Ben to discuss how that shift changes the work of building reliable software. Charity explained how observability helps teams connect changes with outcomes, why nondeterministic systems need “more rigor, not less,” and how traces can show the decisions agents make along the way. Over their wide-ranging conversation, she and Ben also covered automatic instrumentation with OpenTelemetry, why we should think of ourselves as “owners on the loop,” the limits of AI in debugging and SRE, and broader industry concerns like the pressure AI hype places on engineering teams and why maintenance, not speed, builds “enduring value.”

About the Generative AI in the Real World podcast: In 2023, ChatGPT put AI on everyone’s agenda. In 2026, the challenge will be turning those agendas into reality. In Generative AI in the Real World, Ben Lorica interviews leaders who are building with AI. Learn from their experience to help put AI to work in your enterprise.

Check out other episodes of this podcast on the O’Reilly learning platform or follow us on YouTube, Spotify, Apple, or wherever you get your podcasts.

Takeaways

00.59. “Observability is for unknown unknowns.” Monitoring is a way to set thresholds and alert on expected conditions. Observability supports open-ended investigation to answer questions you didn’t know to ask and “find things you didn’t expect.” When AI code generation became capable enough to change software work, observability best practices had to evolve, which is one reason why the second edition of Observability Engineering, which Charity coauthored with Liz Fong-Jones and George Miranda, more than doubled in size.

05.24. Cheap code shifts the work to understanding and support. AI can quickly produce implementation, tests, and documentation, but teams still need to understand what they built and agreed to support, and how their users are experiencing the product. As generating lines of code becomes “effectively free and instant,” validation, review, and operational support can constrain a team’s pace. Of course, Charity wryly noted, so can “every other part of the software development lifecycle.”

06.24. The people who take the credit for AI-assisted work should be able to explain it. AI-generated results (and the papers describing them) complicate authorship, expertise, and the academic training process, something that’s become a particular point of consternation for mathematicians of late. If someone is claiming a result they accomplished with the help of AI, they should be able to present it to peers, Charity and Ben agreed. When AI handles entry-level problems, professions may need new ways for junior practitioners to develop mastery, but Charity is skeptical we’ll run out of problems to solve:

In the same way that I’ve made peace with the idea that cars are faster than I can walk or run, I have made peace with the fact that computers can compute better than I can. . . .That doesn’t mean that there’s no value in the practice, or the discipline, or the learning, or the rigor. It just means that this is one of the things that humans are no longer the best at. But there are a lot of things that we are the best at, and being the best at something isn’t all of what makes it worth doing.

15.56 Nondeterministic systems require “more rigor, not less.” As Charity noted, “The future of software is both determinism and nondeterminism. It really is about using these superpowers that we’ve been given to build those feedback loops. And observability is really the feedback loop of feedback loops.” It’s what connects actions with outcomes and helps teams learn what happened after they make a change. Her analogy:

It’s like we’ve all been riding lawnmowers and just kind of putt-putt, putt-putt, putt-putt along down the road. And now, all of a sudden, our lawnmower has a Ferrari motor in it, and we’re like, “Vroom!” Now we can vroom into the ditch. We can run into a wall. And we have to build structure. We have to build rigor into our system if we want to run down the middle of the street.

18.53 People need to own the loop, and understand the decisions the agents are making. If you need to add observability to your agents, Charity recommends starting with autoinstrumentation with OpenTelemetry and traces that capture agents’ decisions and steps through a task. As for your role, it goes beyond staying “in” the loop. Charity prefers the term “owner on the loop” because it emphasizes the active understanding and control required to manage these systems. AI can amplify experienced debugging and SRE teams, especially when people direct work during rare, high-stakes incidents. Agents have little training data for those situations and can make an incident harder to diagnose. These tools are “not magic,” Charity pointed out. AI “is not a replacement for expertise, but it can be a really powerful adjutant. . .at your side.”

26.00 Different telemetry needs different strategies. Charity distinguished the abundant output from third-party infrastructure from the business-critical telemetry produced by a company’s own code.

There’s observability for infrastructure, which is mostly third-party code. . . .It’s code you didn’t write, but you have to operate it. You can’t change it, but it’s just outputting a lot of logs and metrics into your database logs and your ETLs, or CloudWatch, and all this third-party code is just emitting a lot of stuff. . . .That stuff you should just put someplace that is cheap commodity storage. . . .It shouldn’t be super expensive, just that it’s there when you need it.

Then there are your crown jewels: your code, the code that makes you the company. . . .You should instrument in such a way that preserves as many of the relationships between the data points as possible: arbitrarily wide structured-data blobs, structured logs, and/or traces with lots of spans. Because the most valuable part of your data is the relationships. . . .You don’t want to spread it out into hundreds or thousands of individual metrics or log lines. You want to keep it together so that you can correlate: when this happened, that happened; or when this happened, that was true; or when this happened, it was part of this long event. . . .This is the most important data you have. And for that, it should go someplace. . .that preserves those relationships and opens it up for explorability by you or your agents.

Imagine an update that does not interrupt your work

Restart to update on idle: A practical step you can take today

Why faster updates matter

When protection can't wait, Edge can move faster

For organizations: Security Update Alerts help admins close update gaps faster

A Pulumi ESC environment can now mint a short-lived OpenID Connect (OIDC) token for any service that accepts one.

Every pipeline and agent that touches your infrastructure eventually needs credentials for services beyond your cloud: a package registry such as Cloudsmith or JFrog Artifactory, or a workload access platform such as Aembit. The default historically has been to store a long-lived API key that sits in an environment, which presents a much higher risk of exposure than short-lived credentials.

With the new fn::open::oidc provider, ESC signs a short-lived token for the audience you choose when you open the environment. The service named in that audience checks the signature and exchanges the token for a credential of its own. The token expires within the hour, and ESC stores nothing.

Why the stored key is the weak link

A stored key for a registry or an access platform sits in ESC until someone rotates it. It works for anyone who reads it, from any machine, for as long as it exists. If it leaks, you rotate it, and every consumer of the environment breaks until it picks up the new one.

An OIDC token works the other way around. ESC mints it at the moment you open the environment, signs it with a key only Pulumi holds, and stamps it with an expiry. The service checks it against the trust policy you configured and issues a credential with its own lifetime. You store nothing, so you rotate nothing.

Why this matters for agents

An AI agent that opens an environment gets whatever the environment holds. A stored key works from anywhere until someone rotates it, and one bad prompt can copy it out. A fn::open::oidc token is tightly scoped and short-lived so your agents will only access what they need and nothing more.

How it works

Declare the provider in an environment, name the audience the service expects, and export the token:

values:
 aembit:
 login:
 fn::open::oidc:
 audience: https://acme.aembit.io
 duration: 15m
 identityToken:
 version: v2
 environmentVariables:
 AEMBIT_OIDC_TOKEN: ${aembit.login}

The provider takes three inputs. audience becomes the token’s aud claim, the name the service checks. identityToken.version: v2 selects the token format. duration sets the lifetime, from one minute to one hour, and defaults to one hour. ESC refuses any other input.

Opening the environment yields a signed token. Decoded and trimmed, its claims look like this:

{
 "iss": "https://api.pulumi.com/oidc/v2",
 "sub": "pulumi:org:8a4f0c2e-91d3-4b6a-b7e0-5c2f8d1a9e44:env:2c9d7f61-3e58-4a02-9b8f-6d4e0a7c3b15",
 "aud": "https://acme.aembit.io",
 "exp": 1789000900,
 "https://pulumi.com/org": "acme",
 "https://pulumi.com/current_env": "aembit/login",
 "https://pulumi.com/actor": "alice",
 "https://pulumi.com/actor_id": "5f3a9c0d-7e21-4b8a-9d6c-1e0f2a3b4c5d"
}

The issuer publishes its signing keys through the standard discovery document at https://api.pulumi.com/oidc/v2/.well-known/openid-configuration, so most services need only the issuer URL. The subject names your organization and the environment that declares the block, by ID. IDs survive renames, and Pulumi never reuses one, so a trust policy that pins the subject keeps working and cannot be claimed by a later environment with the same name. The readable names travel in the https://pulumi.com/ claims for your logs.

To see the exact claims before you touch a trust policy, swap in debug-oidc-claims with the same inputs. It returns the claims as plain values and signs nothing.

Pin the subject

Pin the subject in every trust policy you write. Configure the policy with the issuer, the audience, and the subject. The service checks the signature against the issuer’s published keys. The issuer and the audience confirm the token came from Pulumi and was meant for this service, and the subject confirms it came from your environment. Without the subject, the policy accepts a token from any Pulumi organization that typed the same audience string, since every organization shares the /oidc/v2 issuer. Pulumi Cloud shows the subject above the environment editor with a copy button, so you never assemble it by hand.

Example: Aembit

Aembit identifies a workload by its OIDC token and then hands it the credentials its access policy allows. In your Aembit tenant, create a trust provider of type OIDC ID Token that discovers keys from https://api.pulumi.com/oidc/v2, with match rules for the issuer, the audience from the environment, and the environment’s subject. Then create a client workload identified by OIDC ID Token Subject with the same subject, and an access policy that joins the two to the credential provider the workload needs.

Open the environment and send the token to the Aembit Edge API at https://<tenant>.ec.<region>.aembit.io/edge/v1/auth, together with your Edge SDK client ID:

{
 "clientId": "<client-id>",
 "client": {
 "oidc": {
 "identityToken": "<value of AEMBIT_OIDC_TOKEN>"
 }
 }
}

Aembit answers with an accessToken for its later calls, and the ESC token has done its job. Cloudsmith and JFrog Artifactory follow the same shape, and the relying-party guide walks through each of them.

Define it once, import it everywhere

The subject belongs to the environment that declares the block. Put fn::open::oidc in one environment, import it from the environments that need the token, and each of them presents the same subject. Your trust policy stays at one entry. ESC checks open permission on every environment it loads, imports included, so only someone who can open the declaring environment can mint a token with that subject. Each token ESC mints adds an environment-oidc-token-issued entry to your organization’s audit log with the subject, the audience, the environment, and the lifetime.

What stays the same

The aws-login, azure-login, gcp-login, and vault-login providers keep using the https://api.pulumi.com/oidc issuer with its own keys, so your existing trust relationships keep working. Use them when ESC can do the exchange for you, and fn::open::oidc when you need the token itself.

Get started

fn::open::oidc is available now in every Pulumi Cloud organization.

1. Add a fn::open::oidc block with the service’s audience and identityToken.version: v2, and save the environment.
2. Copy the OIDC subject shown above the environment editor into the service’s trust policy, together with the https://api.pulumi.com/oidc/v2 issuer and the audience.
3. Open the environment with pulumi env run and exchange the token.

The provider reference lists the inputs and the troubleshooting steps, and the relying-party guide walks through Cloudsmith, JFrog Artifactory, and Aembit. Questions and feedback are welcome in the Pulumi Community Slack.

Set up Claude Code for a .NET solution on Windows, understand native and WSL environments, check SDK visibility, and separate terminal use from IDE support.

Getting started with .NET on macOS and Linux has historically meant navigating a plethora of options: system package managers like apt or brew, platform-specific tarballs, or standalone shell scripts like dotnet-install.sh. While those methods have served us well, they often collide with administrative permissions, leave files scattered across root directories, or make keeping multiple runtime versions side-by-side more awkward than it should be.

That’s why we’re introducing the public preview of dotnetup, a new .NET toolchain manager built to install, manage, and update .NET SDKs and runtimes directly in your user account.

Why dotnetup?

If you’ve spent time in ecosystems like Rust (rustup) or Node (nvm), you’re already familiar with the power of a dedicated toolchain manager. The core goal of dotnetup is to drastically reduce concept count and friction when getting a .NET environment running:

• Consistent ux: The same commands and tools across every platform, regardless of the details of the installation
• Non-admin by default: Everything lives comfortably in user-owned folders, not system-owned – meaning zero need for elevated permissions.
• Side-by-side runtime management: Keep multiple servicing versions, preview channels, and daily builds installed at once without them stepping on each other’s toes.
• Track intent: Instead of managing versions, track majors or feature bands and let the tools keep you updated each month
• Respect for project pinning: Works seamlessly with your existing global.json files so team builds remain predictable and deterministic.

Let’s walk through how to get started and how to use dotnetup for common day-to-day tasks.

Installing dotnetup and getting started

To get dotnetup on macOS or Linux, run the bootstrap script in your terminal:

macOS (Zsh):

curl -fsSL https://aka.ms/dotnetup/get-dotnetup.sh | zsh

Linux (Bash):

curl -fsSL https://aka.ms/dotnetup/get-dotnetup.sh | bash

PowerShell (pwsh):

irm https://aka.ms/dotnetup/get-dotnetup.ps1 | iex

Once the script pulls down the binary, initialize your environment:

dotnetup init

The init command sets up your shell profile so that dotnet is immediately available in your terminal sessions and fetches the latest stable .NET SDK.

Let’s check what’s installed in our local environment:

dotnetup list

You’ll see a clean inventory of the SDKs and runtimes currently managed by dotnetup right in your home folder.

Keeping runtimes fresh month-over-month

Every month the .NET team ships servicing updates with security fixes and quality improvements. Keeping your local dev machine up to date helps you build and test against those fixes. For self-contained applications, you also need to republish and redeploy with the updated runtime. Updating your machine does not patch applications you have already shipped.

When using system installs, you may not be in control of your ability to update. With dotnetup, staying current is a one-liner:

dotnetup update

This command resolves your tracked SDK and runtime channels again and installs the latest matching versions. For example, 10.0 tracks updates within .NET 10, while latest follows the latest stable SDK, including new major releases. Exact-version requirements stay pinned, so an installation requested as 10.0.3 will not advance during an update.

If you only want to install or refresh a specific runtime flavor, like the ASP.NET Core runtime on .NET 10, you can target it cleanly:

dotnetup runtime install aspnetcore@10.0

After a successful update, dotnetup automatically removes installed components that no remaining requirement needs. Versions that another channel or exact-version requirement still needs stay installed.

When you no longer need a tracked channel or exact version, remove that requirement with the corresponding sdk uninstall or runtime uninstall command. dotnetup then cleans up the installations that are no longer needed. See updating tracked installations for more details.

Testing nightly and preview builds

Beyond routine monthly servicing, many developers want to test bug fixes or check out new runtime capabilities before they hit stable release channels. Previously, testing a nightly runtime build meant hunting down raw installer tarballs from GitHub, manually unpacking them into custom directories, and tweaking environment variables by hand.

dotnetup treats previews and nightlies as first-class citizens. You can install preview SDKs side-by-side with your stable setup:

dotnetup sdk install preview

Or pull down the latest daily runtime build to verify an issue fix:

dotnetup runtime install daily

Or grab an entire SDK to check out the entire toolchain:

dotnetup sdk install daily

You get the flexibility to test daily builds across your user account and clean them up easily!

Updating dotnetup itself

We’ll be pushing features and fixes to dotnetup over time, and you can get them easily:

dotnetup self update

Common questions

Here are quick answers to a few questions you might have:

I could do all of this with dotnet-install.[sh|ps1]

That’s not a question.

But yeah, you could do most of this with the install scripts. What you miss out on is

• management of the installed SDKs and Runtimes
• signature and checksum validation of the installed SDKs and Runtimes
• faster installation of multiple SDKs and Runtimes
• a unified CLI surface for doing this on every platform

Does dotnetup need sudo or root rights?

Nope. dotnetup is currently built for non-admin, user-local operation. All SDKs, runtimes, and metadata live entirely within your user directory.

In a future release we’ll be adding support for managing the system-level installs on Windows because of how prevalent those are on that operating system.

Can I use dotnetup in CI pipelines?

Absolutely. Because dotnetup doesn’t require root privileges and runs smoothly non-interactively, it’s a great fit for containerized or ephemeral CI workers where you need to spin up specific SDK or nightly runtime versions on the fly.

What’s on the roadmap for dotnetup?

As mentioned, we’ll be looking into support for Windows admin installers, but we also want to integrate dotnetup into CI/CD systems like GitHub Actions and Azure DevOps – ideally through replacing parts of the implementations of those tools today that rely on the dotnet-install scripts.

We also want to iterate on the user experience to better fit how you all use the tool, and flesh out agent skills so that automated assistants use the tooling more naturally and reach for it by default.

Where should I go for more details?

For the full CLI reference, advanced configuration options, and deep dives, head over to the dotnetup documentation on Microsoft Learn.

If you have feedback, run into bugs, or want to share your thoughts on the experience, please drop by the dotnet/sdk discussions on GitHub. We’d love to hear how it works for you, or how we can make it better!

The post Introducing dotnetup: A toolchain manager for .NET appeared first on .NET Blog.