Accelerating the development of LemmaScript through adoption, real-world use, and a training corpus that makes verification-first programming the default for future AI
Accelerating the development of LemmaScript through adoption, real-world use, and a training corpus that makes verification-first programming the default for future AI
Project Details
Updated 07/23/26 · Edited by orgThis project is the first significant step toward a future where AI generated code is correct by default. We have developed LemmaScript, a verification toolchain for TypeScript that extends correctness from type-checking to behavioral contracts that can be formally verified. That means that, even before compiling the code, an entire class of bugs is eliminated by construction. We are building this toolchain for a future where agents write nearly 100% of implementation code. LemmaScript is a step toward a system that lives outside of AI judgment so that code generated and pushed by fully-autonomous agents carry guarantees of correctness established by an external verifier. In this case, the reduction in x-risk comes from the prevention of errors in critical code that could lead to catastrophic large-scale outcomes.
The proof-of-concept is strong and we are working toward a stable version (1.0). This project aims to tackle the adoption/development cycle. When we say “adoption,” we mean by both people and agents. To accelerate development of the toolchain and develop a robust ecosystem, we need human adoption and feedback. To make verification-first programming the default to agents, we need a large corpus of training materials for the next family of AI.
We can achieve both of these goals with similar activities:
1. Hold a hackathon
Output: 100s of new adopters + real-world projects built with LemmaScript
-
Run webinars and workshops focused on the concept of verification-first programming
Output: all materials made public, gather feedback, developer data + develop partnerships with larger organizations on similar tracks -
Develop and distribute learning materials: documentation, tutorials, developer trainings, and community support to decrease the friction of getting started with the tooling and technology
Output: A full body of LemmaScript materials (case studies, docs, guides, examples, videos, etc).
- In parallel to the previous 3 activities, continue to expand the LemmaScript ecosystem and its capabilities
Output: Release a stable version
Who’s involved:
Nada Amin: Drives the technical development of LemmaScript
Fernanda Graciolli: Informs toolchain design, and drives adoption and developer relations
Theory of Impact
Updated 07/23/26 · By grantmaking.aiIn this case, the reduction in x-risk comes from the prevention of errors in critical code that could lead to catastrophic large-scale outcomes. Currently, much of AI-generated code is human-reviewed, but we are quickly moving toward a world where agents are the primary generators and reviewers of code, and as such, are given more and more autonomy to push production code that affects large groups of people. We already see a rising number of security breaches (e.g., CVEs) and buggy software (albeit lower-stakes) due to AI-generated code. In the near future, AI will inevitably be adopted in workflows that touch higher-stakes domains: critical infrastructure, authorization, financial systems, etc. In those domains, certain critical bugs mean catastrophic losses — in terms of how many are affected, in terms of the depth of the effect, or both. The development and adoption of formal external verifiers must begin long before AI is integrated into these critical paths, so that when they inevitably are integrated, we are equipped to prevent catastrophic mistakes altogether.
Furthermore, LemmaScript allows us to further explore agent safety by verifying the agents themselves: instead of relying on soft guardrails, LemmaScript allows us to embed hard contracts into agent actions that make it, not unlikely, but impossible that an agent will perform a forbidden action.
People
Updated 07/09/26 · Edited by orgTeam Member
Team Member
Discussion
No comments yet. Be the first to share your thoughts.