# Scidonia > Scidonia builds vericoding tooling: contracts are the single source of truth, checked by a theorem prover. HTML pages use a trailing slash. `https://scidonia.ai/fasttrack` redirects to `https://scidonia.ai/fasttrack/`; cite the slashed URL. Blog posts are also published as Markdown at the same path with a `.md` suffix, for example https://scidonia.ai/blog/proof-as-commodity.md. ## Pages - [Home](https://scidonia.ai/): Verified software at the cost of a test run. Contracts are the source of truth; a theorem prover checks the code. - [Technology](https://scidonia.ai/technology/): The vericoding toolchain: specsaver, axiomander, and rocq-piler. - [Vericoding](https://scidonia.ai/vericoding/): AI-guided certified program refinement: the specification is the artefact, and a theorem prover certifies the refinement. - [parsebot](https://scidonia.ai/vericoding/parsebot/): Certified parsers from grammars in Rocq, extracted to OCaml. A zero-copy JSON tokenizer, proved equivalent, reaches 267.9 MB/s on gsoc-2018.json. - [SpecAMQP](https://scidonia.ai/vericoding/specamqp/): An open Lean specification of AMQP 1.0: a shared description implementations can prove they comply with, growing into a server that is correct by construction. - [Solutions](https://scidonia.ai/solutions/): Where proof is the difference: money movement, exactly-once fulfilment, inventory, and regulatory compliance. - [Services](https://scidonia.ai/services/): Vericoding services for correctness and speed. You review the specification, and a theorem prover checks that the program meets it. - [FastTrack](https://scidonia.ai/fasttrack/): C and Rust latency refinement. We improve service latency, or there is no fee. Lower compute cost follows. - [Database speedup](https://scidonia.ai/database-speedup/): Certified query replacement for high-volume prepared statements. Compiled code proved to return the same rows, values and errors as the database engine. - [GIS databases](https://scidonia.ai/gis/): Faster spatial queries and lower compute costs for high-volume GIS workloads. Compiled code proved to return the same rows, values and errors as the database engine. - [API workflow verification](https://scidonia.ai/api-workflow-verification/): A review of one critical workflow that spans several systems. We agree the business rules, check failure and concurrency cases, and report the sequences that leave payments, orders or access in the wrong state. - [Verified security](https://scidonia.ai/verified-security/): Reusable formal evidence for security components. Machine-checked proofs of isolation, access control, protocol state or message integrity, adapted for each product's Common Criteria or EUCC evaluation. - [Document workflow](https://scidonia.ai/document-workflow/): Vericoding for document workflows where correctness matters. Each fact is cited from the source document, and the handoff into later processes is specified and checked. - [Products](https://scidonia.ai/products/): PaperBreak, a structured AI knowledge and document platform built on the vericoding toolchain. - [Blog](https://scidonia.ai/blog/): Essays on vericoding, mechanised proof, and high-assurance AI systems. - [About](https://scidonia.ai/about/): What Scidonia builds, and how to get in touch. ## Blog - [AI-Guided Certified Program Refinement](https://scidonia.ai/blog/ai-guided-certified-program-refinement.md): Software's core problem is knowing what it should do. AI-guided certified program refinement — vericoding — makes specification the artefact we tinker with, and lets AI guess program transformations that a theorem prover certifies. - [Darwin's Machines: How do we assess the risk of AI?](https://scidonia.ai/blog/darwins-machines-how-do-we-assess-the-risk-of-ai.md): 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. - [From Vibecoding to Vericoding: A Gradient, Not a Jump](https://scidonia.ai/blog/from-bdd-to-proof.md): 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](https://scidonia.ai/blog/contracts-compositionality.md): 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. - [The Cost of Correctness: Why Formal Verification Is About to Get Cheap](https://scidonia.ai/blog/verification-cost-revolution.md): seL4 took 20 person-years to verify 8,700 lines of C. CompCert produced zero compiler bugs under extensive fuzzing. The guarantees have always been worth it. The cost has not. AI changes that. - [Proof as Commodity](https://scidonia.ai/blog/proof-as-commodity.md): We proved type preservation for PCF — a classic typed lambda calculus benchmark — using two frontier LLMs and rocq-piler. DeepSeek v4 completed it in 21 minutes for $0.06. Claude Opus 4.8 took 14 minutes for $6.80. Either way, mechanised proof is no longer expensive. - [Code Will Become Opaque — And That's Fine](https://scidonia.ai/blog/opaque-code-theorem-proving.md): Most software developers haven't twigged the real potential of automated theorem proving with LLMs. If provers are powerful enough, you no longer need to understand the code — only the contracts at the interface. - [Axiomander: Robots on Rails](https://scidonia.ai/blog/axiomander-vanilla-python-mechanised-proof.md): Contracts as plain assert statements. Verification via Coq and SMT. Zero imports, zero decorators, zero runtime overhead. Bringing theorem-prover-grade verification to real Python programmers. - [Which Model Should Verify Your Extractions? A Cost-Quality Analysis of LLM Checkers](https://scidonia.ai/blog/extraction-checker-cost-quality.md): Every extraction pipeline needs a verification step. We tested eight models as quality scorers and found that for hallucination detection, a model costing 200× less than Claude performs identically. But for events, model quality still matters. - [Why a Structured Ontology Beats a Flat Notepad for LLM Short-Term Memory](https://scidonia.ai/blog/short-term-memory-ontology.md): Giving an LLM a typed, navigable knowledge structure instead of a flat scratchpad changes what it can remember, how it updates facts, and how much context it consumes doing so. - [How Do You Measure an LLM's Memory? Precision and Recall for Conversation Facts](https://scidonia.ai/blog/conversation-memory-eval-methodology.md): String matching cannot tell you whether an LLM remembers what was said in a conversation. We describe the QA-probing methodology we use to measure short-term memory recall and wiki precision, and what our first results reveal. - [Ghost Entities: Why LLM Hallucinations in Entity Extraction Are a Serious Downstream Risk](https://scidonia.ai/blog/hallucinations-in-entity-extraction.md): Hallucinated entities and relationships look identical to real ones inside a knowledge graph. We measured how often frontier models inject facts from parametric memory rather than from your documents — and found rates as high as 73% on a single document. Here is why that matters and what to do about it. - [Which LLM Finds People Best? Benchmarking Claude, GPT-5.4 and Gemini 3 on PERSON Entity Extraction](https://scidonia.ai/blog/llm-entity-extraction-person-comparison.md): We ran three frontier models on 8 open-licence documents and measured how accurately each one identifies named people — before and after cross-checking. The results reveal meaningful differences in hallucination rates and the value of verification. - [Self-Prompt Injection: The Security Threat Nobody Is Talking About](https://scidonia.ai/blog/self-prompt-injection-the-threat-hiding-in-plain-sight.md): You sanitized all your user inputs. Your prompt template is static. You think you're safe from prompt injection. You're not — and the attack vector is the agent itself. ## Optional - [Privacy](https://scidonia.ai/privacy/): How Scidonia handles personal information. - [Full blog text](https://scidonia.ai/llms-full.txt): Blog posts concatenated for a single fetch. - [RSS](https://scidonia.ai/rss.xml): Blog feed. - [JSON Feed](https://scidonia.ai/feed.json): Blog feed as JSON. - [Sitemap](https://scidonia.ai/sitemap.xml): Canonical HTML URLs. - [Agent skill](https://scidonia.ai/.well-known/agent-skills/index.json): Instructions for reading this site.