Can Lean improve security for AI-coded software?

A whopping 95% of all code will be AI-generated within the next five years, Microsoft’s chief technology officer, Kevin Scott, predicted recently. Because AI-generated code tends to be security-challenged, that will be a big headache for security teams. One study of more than 100 large language models (LLMs) across Java, Python, C#, and JavaScript found that 45% of the code samples failed security tests and introduced vulnerabilities on the OWASP Top 10.

That’s not just a quality problem, Leonardo de Moura, senior principal applied scientist at Amazon Web Services, wrote recently in a GitHub blog. It’s a systemic risk because AI generates an increasing share of the world’s critical infrastructure — financial systems, medical devices, defense, transportation.

“The problem is not that everything is broken. It is that AI is changing the scale and speed of software production faster than our ability to verify it. What works at human pace may not survive AI pace.”
—Leonardo de Moura

To keep things from getting worse fast, de Moura said, the entire critical software stack needs to be reconstructed with mathematical proofs built in. That’s a task well suited to Lean, he said, a programming language and interactive theorem prover that he created.

Here’s what you need to know about Lean — and what it means for AI-code security.

[ See webinar: Develop Your New Playbook for AI-Driven Software Risk ]

A language doesn’t tell the whole story

The idea is theoretically compelling, said Jeff Williams, CTO and co-founder of Contrast Security and the founder of OWASP.

“If AI can generate both software and machine-checkable proofs, formal verification could become dramatically less expensive. Lean is particularly well suited to that model because it combines programming, specification, and proof in one environment, with a small independent kernel checking the result.”
—Jeff Williams

But while the early examples are impressive, he said, they are still examples — not evidence that we are close to rebuilding the general software ecosystem this way.

The biggest gap, Williams said, isn’t generating code or even proofs.

“It is specifying exactly what the software is supposed to do. Security requirements are often incomplete, ambiguous, and dependent on business context. A proof can establish that an implementation matches its specification, but it cannot establish that the specification reflects what the business really needed.”
—Jeff Williams

AI will help, but it will not make the hard thinking disappear, he added.

Williams also noted that language is only one part of a real implementation decision. “Enterprises need mature platforms for deployment, identity, policy, observability, monitoring, upgrades, and support. Developers need extensive libraries, frameworks, integrations, and reusable components,” he said.

He said Lean has an impressive ecosystem for mathematics and a growing set of verification projects, but that is very different from the enormous application ecosystems surrounding Java, JavaScript, Python, .NET, and cloud-native platforms. “Without those capabilities, even a beautifully verifiable language will remain difficult to use for mainstream development,” he said.

He said Lean makes sense for cryptography, authorization engines, protocols, parsers, and other foundational components where failure is extremely expensive. But rebuilding the world’s software is not going to happen anytime soon. “We have had powerful formal methods for decades, and outside a relatively small number of critical systems, the juice has not been worth the squeeze,” he said.

“AI may improve the economics significantly, but there are still enormous gaps in specifications, tooling, libraries, platforms, skills, and migration. Even with AI, rebuilding the software stack would be a multi-decade project. The practical path is to verify the critical foundations and continue securing everything else with layered testing, analysis, monitoring, and runtime protection.”
—Jeff Williams

Proof is what matters — not plausibility

Organizations should apply defense-in-depth rather than depend on the model to verify its own work, said Christopher Jess, senior R&D manager at Black Duck Software. Defenses should include static application security testing, software composition analysis, secrets and infrastructure-as-code scanning, dynamic testing, fuzzing, property-based tests, and independent human review. “Formal verification can add much stronger assurance for critical components, but it complements rather than replaces these controls,” he said.

Jess also recommended that those checks be embedded in the IDE, pull requests, and CI/CD pipelines so that AI-generated code is evaluated as it is created.

“Organizations also need visibility into copied code, transitive dependencies, AI models, licenses and provenance, not only dependencies declared in manifest files.”
—Christopher Jess

Black Duck’s 2026 Open Source Security and Risk Analysis (OSSRA) report found that 98% of audited codebases contained open-source components, while mean vulnerabilities per codebase rose 107%. It also found that 16% of open-source components required deeper techniques to identify them, such as snippet or binary analysis. “This demonstrates why securing AI-generated software requires comprehensive analysis of the finished application, not just oversight of the coding assistant,” Jess said.

The Lean language is particularly interesting because it combines programming with formal specification and machine-checked proof, Jess said. “Its real security value is not simply that its syntax may be predictable, but that generated proofs are checked by a small trusted kernel rather than accepted because they appear plausible,” he said.

Mitul Chittoory, a member of the Emerging Trends Group of ISACA, said redictability helps an LLM generate syntactically correct code, as low predictability often stems from ambiguous syntax, undefined behaviors, or loose typing.

“In those unpredictable environments, an LLM is statistically more likely to introduce subtle, hidden vulnerabilities such as timing side channels that pass standard tests but fail in edge cases. The real advantage emerges when a highly structured language is paired with formal verification. This reduces hallucinations and forces the LLM to satisfy strict mathematical proofs rather than just guessing the next statistical token.”
—Mitul Chittoory

The traditional view is that manual verification is a slow, expensive tax, Chittoory said. “But when AI generates highly predictable, verified code, that timeline collapses, especially for qualifying critical systems, from months down to days or even mere hours,” he said.

He added that it eliminates “workslop,” where developers spend hours downstream trying to debug AI-generated code, because the predictable nature of the codebase allows for mathematical guarantees of correctness the moment it is generated.

A tool for critical components

Avitesh Kesharwani, a technical architect, AI transformation leader, and senior IEEE member, said that what makes Lean interesting is not just its syntax, but also that it is both a programming language and a theorem prover. “In Lean, developers can express detailed requirements as types and propositions. The model is not simply asked to produce code that looks reasonable. It may be asked to produce a proof that a function has a particular property,” he said.

For example, instead of writing a sorting function and testing it on 10 sample inputs, a developer can ask Lean to verify that the output is sorted and contains exactly the same elements as the input, he said. If the model produces an incomplete or incorrect proof, Lean does not accept it. It returns a type error or an unresolved proof goal. The model can then use that feedback to try again. That creates a useful loop: generate, check, correct, and verify.

“Lean is especially interesting because the verifier is separate from the model. The model can propose a proof, but Lean’s kernel decides whether that proof is valid.”
—Avitesh Kesharwani

In the near term, Kesharwani does not expect most companies to rewrite entire systems in Lean. “A more practical approach would be to use Lean or similar formal methods for the parts of a system where mistakes are especially costly. That could include access control rules, cryptographic protocols, financial calculations, parsers, safety checks, and other high-risk components,” he said.

The surrounding application could still be written in Java, Python, C#, or another mainstream language, while the critical logic receives stronger formal verification, Kesharwani said.

Jacob Krell, senior director for secure AI solutions and cybersecurity at Suzu Labs, said the broader principle is simple. “AI can generate code quickly, but it should not be the final authority on whether that code is safe. The most important factor in AI code quality is the training data,” he said.

Models produce better code in languages where they’ve seen more high-quality examples. Lean has a small corpus compared to Python, Java, or Go. Switching to a niche language for predictability could actually degrade the quality of generated code because the model has less to learn from, Krell said.

“For most teams, the practical path is a mainstream, memory-safe, strongly typed language where the compiler catches errors, combined with formal verification on the security-critical paths. Lean is powerful for that verification step, but it’s the proof that provides the guarantee, not the perplexity.”
—Jacob Krell