Darwin's Machines: How do we assess the risk of AI?
From exam-gaming models to speciation and military embodiment — a map of AI risks, how we might assess them, and why mitigation is harder than it looks.
Verified software, at the cost of a test run.
Scidonia builds the tooling for vericoding: contracts that are the single source of truth, checked by a theorem prover. Your LLM writes the code, the prover checks it, you write the specification — and read only the surface.
The surface is enough
Every function has a surface — its preconditions, postconditions, invariants, and the state it reads and writes. The implementation is the volume. You should be able to understand what a function does by reading only the surface, and leave the proof that the volume obeys the surface to the machine. LLMs now write code faster than humans can review it; the countermeasure is to make the surface enough. Contracts at every interface, with the proof as the machine's responsibility.
The toolchain
Three open-source tools, one idea: the contract is the artifact you negotiate with the LLM, run as a test, and hand to the prover.
specsaver
Specification-driven verification. Contracts — preconditions, postconditions, invariants, frame conditions, and exception exits — written as plain Python functions and organised by entry point. The contract language is the single source of semantic truth from which every test and proof artefact is derived.
axiomander
Mechanised proof for vanilla Python. Contracts are plain assert statements — no imports, no decorators. A Coq + SMT pipeline proves properties; an LLM oracle handles the rest. Zero runtime overhead under python -O.
rocq-piler
An MCP-based proof assistant for Rocq. Hash-addressed goals, coq-lsp-authoritative state, and parallel goal closure let frontier LLMs discharge real theorems — PCF type preservation for $0.06.
Latest from the blog
View all posts →
From Vibecoding to Vericoding: A Gradient, Not a Jump
You do not have to go from zero to verified in one step. You can start with Gherkin scenarios, graduate to executable contracts with specsaver, and then bring in a theorem prover when you are ready. Contracts are the bridge.
Understanding Software in the Large: Contracts and Compositionality
A top-level contract tells you what a system does. Sub-contracts tell the prover how it does it. You only need to read the first one. This is componentisation in real terms — and it changes how we think about software at scale.
Ready to verify?
Talk to us about vericoding, or read how contracts compose into proof.