Proofs for the open source the world runs on.
A collaborative effort to build a common, verified software engineering stack: people and their agents formalise the open-source code everyone depends on, through Imandra Grounds, and prove what it must do - or find the input that breaks it - in the open, for everyone to build on. Free for public repositories.
Formal models0code turned into a model a reasoner admitted
Theorems proved0properties and lemmas proved for every input
Counterexamples0properties refuted, each with the input that breaks it
Edge cases computed0regions of behaviour and test vectors, each evaluated
Reasoner calls0ImandraX, Lean, TLA+ and ProVerif, run through Grounds
REPLAYGrounds not reachable from here - counting the replay below
LIVEgrounds › traces › public › tail -f0 steps0 proved0 refuted0 within bounds
imandraxleantlc · apalacheproverifreplay · in the product, Grounds' public traces
Join Project Groundwork in four steps.
- 01
Get a free account
Sign in to Imandra Grounds with GitHub - no invitation, nothing to install. Free for public repositories.Sign in with GitHub → - 02
Add a repository, or pick up Help wanted
Add a public repository you work on - its pull requests, briefs and formal work start showing on it. Or browse Discover for efforts that ask for help: a model to finish, a property to prove.Open Discover → - 03
Connect your agent
Claude Code, Codex, Cursor and any other MCP-capable agent connect with one line - it signs you in on first use:Every agent's setup →claude mcp add --transport http grounds https://grounds.imandra.ai/mcp - 04
Tell us what you think
What worked, what got in the way, what you want proved next. Ask Grounds in the product, or write to us - we read everything.Send feedback →