{"id":26183,"date":"2026-09-21T15:13:59","date_gmt":"2026-09-21T23:13:59","guid":{"rendered":"https:\/\/www.palada.net\/index.php\/2026\/09\/21\/can-lean-improve-security-for-ai-coded-software\/"},"modified":"2026-09-21T15:13:59","modified_gmt":"2026-09-21T23:13:59","slug":"can-lean-improve-security-for-ai-coded-software","status":"publish","type":"post","link":"http:\/\/www.palada.net\/index.php\/2026\/09\/21\/can-lean-improve-security-for-ai-coded-software\/","title":{"rendered":"Can Lean improve security for AI-coded software?"},"content":{"rendered":"
\n
\n

A whopping 95% of all code will be AI-generated within the next five years, Microsoft\u2019s chief technology officer, Kevin Scott, predicted recently<\/span><\/a>. Because AI-generated code tends to be security-challenged, that will be a big headache for security teams. One study<\/span><\/a> 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.<\/p>\n

That\u2019s not just a quality problem, Leonardo de Moura, senior principal applied scientist at Amazon Web Services, wrote recently in a GitHub blog<\/span><\/a>. It\u2019s a systemic risk because AI generates an increasing share of the world\u2019s critical infrastructure \u2014 financial systems, medical devices, defense, transportation.<\/p>\n

\u201cThe 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.\u201d<\/em>
\u2014<\/em>Leonardo de Moura<\/span><\/a><\/p>\n

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\u2019s a task well suited to Lean, he said, a programming language and interactive theorem prover that he created.<\/p>\n

Here\u2019s what you need to know about Lean \u2014\u00a0and what it means for AI-code security.<\/p>\n

[ See webinar: <\/strong>Develop Your New Playbook for AI-Driven Software Risk<\/strong><\/a> ]<\/strong><\/p>\n

A language doesn\u2019t tell the whole story<\/h2>\n

The idea is theoretically compelling, said Jeff Williams, CTO and co-founder of Contrast Security and the founder of OWASP.<\/p>\n

\u201cIf 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.\u201d<\/em>
\u2014<\/em>Jeff Williams<\/span><\/a><\/p>\n

But while the early examples are impressive, he said, they are still examples \u2014 not evidence that we are close to rebuilding the general software ecosystem this way.<\/p>\n

The biggest gap, Williams said, isn\u2019t generating code or even proofs.<\/p>\n

\u201cIt 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.\u201d<\/em>
\u2014<\/em>Jeff Williams<\/p>\n

AI will help, but it will not make the hard thinking disappear, he added.<\/p>\n

Williams also noted that language is only one part of a real implementation decision. \u201cEnterprises need mature platforms for deployment, identity, policy, observability, monitoring, upgrades, and support. Developers need extensive libraries, frameworks, integrations, and reusable components,\u201d he said.<\/p>\n

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. \u201cWithout those capabilities, even a beautifully verifiable language will remain difficult to use for mainstream development,\u201d he said.<\/p>\n

He said Lean makes sense for cryptography, authorization engines, protocols, parsers, and other foundational components where failure is extremely expensive. But rebuilding the world\u2019s software is not going to happen anytime soon. \u201cWe have had powerful formal methods for decades, and outside a relatively small number of critical systems, the juice has not been worth the squeeze,\u201d he said.<\/p>\n

\u201cAI 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.\u201d<\/em>
\u2014<\/em>Jeff Williams<\/p>\n

Proof is what matters \u2014 not plausibility<\/h2>\n

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. \u201cFormal verification can add much stronger assurance for critical components, but it complements rather than replaces these controls,\u201d he said.<\/p>\n

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.<\/p>\n

\u201cOrganizations also need visibility into copied code, transitive dependencies, AI models, licenses and provenance, not only dependencies declared in manifest files.\u201d<\/em>
\u2014Christopher Jess<\/span><\/a><\/p>\n

Black Duck\u2019s 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. \u201cThis demonstrates why securing AI-generated software requires comprehensive analysis of the finished application, not just oversight of the coding assistant,\u201d Jess said.<\/p>\n

The Lean language is particularly interesting because it combines programming with formal specification and machine-checked proof, Jess said. \u201cIts 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,\u201d he said.<\/p>\n

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.<\/p>\n

\u201cIn 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.\u201d<\/em>
\u2014<\/em>Mitul Chittoory<\/span><\/a><\/p>\n

The traditional view is that manual verification is a slow, expensive tax, Chittoory said. \u201cBut when AI generates highly predictable, verified code, that timeline collapses, especially for qualifying critical systems, from months down to days or even mere hours,\u201d he said.<\/p>\n

He added that it eliminates \u201cworkslop,\u201d 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.<\/p>\n

A tool for critical components<\/h2>\n

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. \u201cIn 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,\u201d he said.<\/p>\n

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.<\/p>\n

\u201cLean is especially interesting because the verifier is separate from the model. The model can propose a proof, but Lean\u2019s kernel decides whether that proof is valid.\u201d<\/em>
\u2014<\/em>Avitesh Kesharwani<\/span><\/a><\/p>\n

In the near term, Kesharwani does not expect most companies to rewrite entire systems in Lean. \u201cA 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,\u201d he said.<\/p>\n

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.<\/p>\n

Jacob Krell, senior director for secure AI solutions and cybersecurity at Suzu Labs, said the broader principle is simple. \u201cAI 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,\u201d he said.<\/p>\n

Models produce better code in languages where they\u2019ve 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.<\/p>\n

\u201cFor 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\u2019s the proof that provides the guarantee, not the perplexity.\u201d<\/em>
\u2014<\/em>Jacob Krell<\/span><\/a><\/p>\n<\/p>\n<\/div>\n<\/div>\n","protected":false},"excerpt":{"rendered":"

A whopping 95% of all code will be AI-generated within the next five years, Microsoft\u2019s 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 studyof 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\u2019s not just a quality problem, Leonardo d<\/p>\n","protected":false},"author":4,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"colormag_page_container_layout":"default_layout","colormag_page_sidebar_layout":"default_layout","footnotes":""},"categories":[32775],"tags":[],"class_list":["post-26183","post","type-post","status-publish","format-standard","hentry","category-reversinglabs"],"_links":{"self":[{"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/posts\/26183","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/comments?post=26183"}],"version-history":[{"count":0,"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/posts\/26183\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/media?parent=26183"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/categories?post=26183"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.palada.net\/index.php\/wp-json\/wp\/v2\/tags?post=26183"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}