Proposal: An official Lean formal semantics for C#

[benaadams]

This is not a proposal for new C# syntax or language constructs. I would like C# to have an officially maintained Lean 4 formal semantics, developed incrementally alongside the language specification.

The aim is a machine-checkable model of C# semantics that verification tools can build on. It would not replace the written specification, require Roslyn or the CLR to be formally verified, or attempt to model the whole language upfront.

Why now?

Formal verification is not new, but AI is changing both the need for it and the cost of using it.

AI is making software dramatically cheaper to produce. Agents can generate, modify and reason over large codebases at a scale that was not previously practical.

The same capability applies offensively. Models are also becoming increasingly capable of understanding unfamiliar code, tracing behaviour across dependencies and searching systematically for vulnerabilities.

That changes the economics of software security.

If code generation scales by orders of magnitude, we cannot assume that human review, conventional testing and manual security analysis will scale with it. At the same time, attackers gain access to increasingly capable automated code analysis.

Tests, fuzzing, analyzers, type systems and code review remain essential, but there is growing value in being able to make a stronger statement about critical properties:

Not merely that we tested them, but that they have been mechanically proven.

AI also changes the other side of that equation. One of the traditional costs of formal verification is constructing the proof. Increasingly capable theorem-proving agents can automate much of that work.

The important distinction is that the AI does not become part of the trusted computing base.

AI can generate the implementation and help construct the proof, while a small deterministic proof kernel independently checks whether the proof is valid.

Conceptually:

code + specification -> AI-assisted proof construction -> deterministic proof checking

is a fundamentally different trust model from:

AI writes code -> AI reviews code -> hopefully both were right

Microsoft Research is already demonstrating exactly this model with production cryptographic software. New Rust implementations in SymCrypt are translated using Aeneas and verified in Lean, with AI agents helping construct proofs which Lean then checks independently.

The question is therefore not simply whether formal verification is useful. AI is making both automated software exploitation and automated proof construction substantially more capable.

C# should have the semantic infrastructure necessary to take advantage of the latter as a defence against the former.

Existing precedent

Other language ecosystems already have useful foundations here.

Rust has Aeneas, which translates Rust programs into representations suitable for proof assistants including Lean. Java has KeY and JML for specification and verification of Java programs. C has CompCert, including formally defined source semantics and a verified compilation chain.

These projects differ substantially in scope and approach, but they give their respective ecosystems roots from which stronger formal tooling can grow.

C# does not currently have an equivalent maintained formal model of the language.

Proposal

Start an official or officially sponsored Lean project covering a useful core of C#.

For example, an initial subset could include:

• primitive integral and Boolean types
• checked and unchecked integer arithmetic
• simple structs
• locals and parameters
• expressions and operators
• methods and calls
• conditionals and loops
• arrays or another small initial memory model

The project would define the type and evaluation semantics for that subset and include conformance examples derived from the C# specification.

That is already enough to verify a meaningful class of algorithms. References, objects, exceptions, generics, unsafe code, async and other features could then be added incrementally.

There should be explicit boundaries where behaviour depends on the CLI or runtime. A useful formal semantics for C# does not require a formal model of the entire CLR as a prerequisite.

Conceptually, the path would be something like:

C# -> formal C# representation -> Lean -> machine-checked properties

Roslyn could eventually provide a bridge from its bound or lowered representation into the formal representation, but I think the semantics themselves should be defined as language infrastructure rather than as undocumented Roslyn behaviour.

Why Lean?

Lean is not the only proof system that could be used, but choosing a concrete target makes this actionable.

It has a small trusted kernel, a strong theorem-proving ecosystem, and relevant existing work around software verification. There is also already experience with Lean and Aeneas in Microsoft Research.

Choosing Lean would not mean that all future C# verification tooling must use Lean. It would establish one maintained, executable formalisation of the language semantics from which tooling can develop.

Why should this be associated with the C# project?

A third party can create a formal model of C# today. The difficult part is establishing that the model actually represents C#.

Language semantics evolve and edge cases matter. An independent model can diverge from the specification or implementation without either side necessarily noticing.

An official or officially sponsored model would give verification projects a common semantic root and a place to resolve ambiguities about the language.

I am not particularly concerned about which repository ultimately owns the Lean sources. A dedicated repository may be more appropriate. What matters is that the model evolves in conjunction with the C# language and specification.

First milestone

I would start small: formalise enough deterministic C# to verify several non-trivial algorithms, and use that prototype to answer:

1. What representation should form the boundary between C# and Lean?
2. How should conformance with the C# specification be tested?
3. Where should semantics that depend on the CLI/runtime be modelled?

If that works well, coverage can grow incrementally with the language.

The proposal is therefore not to formally specify all of C# upfront.

It is to establish a maintained formal foundation so that C# has a first-class path to machine-checked program verification.

[Kryptos-FR]

I only have one question. Why should this work be done at the language level and not from IL, as to include other languages (esp. F#)?

[benaadams]

Maybe, not sure if that would be harder or easier /cc @Julek🤔

Or where to even go to propose it; though is interesting

[CyrusNajmabadi]

It would also make sense, given: derived from Rust MIR

Working at the common representation layer would make the most sense for the .net ecosystem. It could be moved to dotnet/runtime for that.

That said, I don't see this needing first class support. .Net IL is very well documented. So it could be done with anyone using hte appropriate ecma specs.

[benaadams]

I think IL might be better is more constrained and changes less often; at least for the semantics, the formal specs of programs might be harder to write though 🤔

[Atulin]

Why am I getting the feeling that the author is just a meat proxy for some LLM that generated the entirety of this proposal?

[CyrusNajmabadi]

@Jarrich I'm literally saying that as long as posts follow the rules of the repo, it's fine. And to please keep off-topic posts away from here.

We don't want drive-by moderation. Please keep things on topic. In this case: lean and formal semantics for C# and/or .Net.