gavin.codes

We ported a significant fragment of libexpat to Lean. This provides significantly higher confidence in security.

This is what a software verification stack *should* look like. If we had this, we could have high assurance and *fast* software. Without this we are going to be playing wack-a-mole with software security.

We have parity with Node 22 for concurrency in Lean!

Can you write a concurrency library directly in a theorem prover? Can you write real software with it, perhaps a webserver? Can it be similar in performance to servers used in industrial production? What language should I use for Vericoding? Yes, yes and yes! And Lean clearly viable.

Theorem provers can do mutation too!

Hot Take: Theorem provers are ready to do most of what you're currently doing with programming languages and they can often do it a lot better.

Consciousness is as methodologically interesting as revelations from God. Thomas Paine noted revelation can only have validity to the recipient. Beyond that is hearsay. The state of "consciousness" as an experience makes sense only to the one experiencing it.

scidonia.aiUnderstanding Software in the Large: Contracts and Compositionality | ScidoniaA 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 thi...

There are no measurements to make which identify the state. As such it is completely vacuous as a scientific category.

gavin.codes reposted

Scidonia

@scidonia.bsky.social

14 July

The gap between what written code and human understanding is widening due to AI code generation. Merging software verification with design by contract offers a way out. Top-level contracts for humans, sub-contracts for the machine prover. Full breakdown: scidonia.ai/blog/contrac...

gavin.codes reposted

Scidonia

@scidonia.bsky.social

18 June

We used LLMs to prove PCF type preservation in Rocq from scratch. The cost? As low as $0.06. When a mechanised proof costs less than a bug report, vericoding (using AI to write code and a prover to guarantee it) becomes the new standard. scidonia.ai/blog/proof-a...

scidonia.aiProof as Commodity | ScidoniaWe 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 minu...

18 June

$0.06 for a non-trivial proof about programming languages. This is going to change everything.

scidonia.ai/blog/proof-a...

18 June

Type preservation for PCF+Ref now at 4c on DeepSeek + Opencode + Rocqpiler 4 cents ... proof is cheaper than bananas

The approach to Vericoding in axiomander in a nutshell

1/2 Can we safely let AIs do almost all of the coding? What do we need to avoid getting mountains of slop? * Small control surface [Specification] * Deterministic proof of correctness [Proof assistant]

This is essentially a "compiler" for specifications — the dream of declarative programming. The change will be as big as shift as the shift away from assembly. But is this feasible? YES! We've already shown how it can be used for contracts on sequential python. This is the answer to AI slop.

15 June

This is really a rough draft of the future. Specification as control surface, code as disposable and organisations of AIs with specific responsibilities.

Dmytri Kleiner@dmytri.to

Ahoy, #SlopPunk, put this in your pi: github.com/dmytri/sh... The simplest/stupidest/most portable spec-driven workflow with context isolation for any agent. This is still *very new* and *very stupid*, so ymmv. > Specs are durable. Code is disposable. Agents are replaceable.

11 June

Proving properties of software has historically been hard because proof is hard. But if we don't do the proofs, then the hard problem resolves to getting the right specification. This will remain hard, but it will probably also be the main activity in the near future. Time to take this seriously!

10 June

Just tried to run my "benchmark" proof (PCF+ref type preservation) on Fable 5. It took 10 minutes and did not make ONE SINGLE ERROR. No tactics out of place, no iteration. Just full Rocq proofs the first time. This is mental.

4 June

1/3 Proving very basic properties of software can have huge impacts. The NASA Mars Climate Orbiter failed due to a mismatch between Pound-seconds (Imperial) and Newton-seconds (Metric). This mistake cost $327 Million.

4 June

2/3 Theorems which use dimensional analysis are absolutely trivial to prove and can be discharged 100% of the time as they fall into decidable theory: linear algebra. We can adorn python with units and get iron-clad assurance of correctness with no runtime cost and no additional code.

4 June

3/3 Axiomander, our MCP for proving properties of python, shows how easy it is to augment python with this capability. Why isn't everyone already doing this?

scidonia.aiCode Will Become Opaque — And That's Fine | ScidoniaMost 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 th...

3 June

Very soon we will be neither reading, nor writing code. Software engineers will be engaged in specification management. The theorem prover is the key ingredient to make this possible. scidonia.ai/blog/opaque-...

1/4 Here is a video of neuro-symbolic theorem proving in action using the (opensource) Rocq-piler MCP (we renamed when updating to Rocq) with the Rocq theorem prover.

3/4 Model: DeepSeek v4 Tokens to completion: 141k Cost: $3.43 Time: 20m (video is at 10x speed)

github.comGitHub - scidonia/rocq-piler: MCP server for Coq LSPMCP server for Coq LSP. Contribute to scidonia/rocq-piler development by creating an account on GitHub.

4/4 You can get Rocq-piler here: github.com/scidonia/roc...

1/4 Here is a video of neuro-symbolic theorem proving in action using the (opensource) Rocq-piler MCP (we renamed when updating to Rocq) with the Rocq theorem prover.

2/4 We (at Scidonia) have spent considerable effort to increase the theorem proving ergonomics for LLMs with our MCP and have gotten the following one-shot for a type preservation theorem about the programming language PCF with references (sort of a micro-ML language) on video.

24 May

1/2 One shotted type preservation for PCF+references, including obtaining all necessary lemmata for the proof using the latest version of our MCP for coq (github.com/scidonia/mcp...) using DeepSeek v4.

24 May

2/2 Done with the following prompt: "You are a proof assistant. You need to use only MCP tools to work your way through a coq proof. This proof is in mcp-coq-lsp/test_issues.v. You will need to add lemmata as you discover the need. Please fully close the main theorem."

github.comGitHub - scidonia/mcp-coq-lsp: MCP server for Coq LSPMCP server for Coq LSP. Contribute to scidonia/mcp-coq-lsp development by creating an account on GitHub.

21 May

I'm making good progress on an automated theorem environment for python using only an MCP. But to make that work well, I needed interactive LLM theorem proving. For this I've developed an MCP for the Coq/Rocq theorem prover. github.com/scidonia/mcp...

23 Apr

Software engineering is now mostly robot management. I'm not sure I like it, but that's where it has to go.

16 Apr

Cross-checking generated content increases quality substantially, but what models should I use to *cross-check* generated content. It turns out for entity extraction you can use almost anything! Use the model which is 200x cheaper. See below 👇

scidonia.ai/blog/extract...

16 Apr

scidonia.aiWhich Model Should Verify Your Extractions? A Cost-Quality Analysis of LLM Checkers | ScidoniaEvery 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. B...

14 Apr

Riffing on an idea that is making the rounds of using a wiki knowledge base to drive your LLM, we tried this approach just for chat short term memory. The results were very sensitive to the ontology and organisation, we get better results than raw summary. It works amazingly well! See below 👇

scidonia.ai/blog/short-t...

14 Apr

scidonia.aiWhy a Structured Ontology Beats a Flat Notepad for LLM Short-Term Memory | ScidoniaGiving 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.

13 Apr

Ontologies can be helpful in structuring short term memory for interactive agents. We developed a methodology for short-term memory assessment and demonstrate a comparison between naive summarisation and ontology centric memory. Full discussion and methodology below 👇

scidonia.ai/blog/convers...

13 Apr

scidonia.aiHow Do You Measure an LLM's Memory? Precision and Recall for Conversation Facts | ScidoniaString 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...

10 Apr

Entity extraction from documents can provide huge benefits to organisations. If your model is hallucinating information - it will pollute downstream assets. The key is appropriate provenance tracking and cross checking. Methodology link below 👇

scidonia.ai/blog/halluci...

10 Apr

scidonia.aiGhost Entities: Why LLM Hallucinations in Entity Extraction Are a Serious Downstream Risk | ScidoniaHallucinated 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 ...

gavin.codes reposted

Scidonia

@scidonia.bsky.social

9 Apr

We benchmarked Claude Sonnet 4.6, GPT-5.4, and Gemini 3 Pro on PERSON entity extraction across eight open-licence documents, spanning 18th-century literary prose, research papers, biomedical articles, & Wikipedia. Here is what we found - scidonia.ai/blog/llm-ent...

scidonia.aiWhich LLM Finds People Best? Benchmarking Claude, GPT-5.4 and Gemini 3 on PERSON Entity Extraction | ScidoniaWe 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.

9 Apr

Are you using the right models to analyze your documents? When performing large-context entity extraction, model matters and cross checking has an important impact on precision. It is easier for models to check than to generate, so checking is often worthwhile.

github.comGitHub - scidonia/mcp-coq-lsp: MCP server for Coq LSPMCP server for Coq LSP. Contribute to scidonia/mcp-coq-lsp development by creating an account on GitHub.

22 Dec 2025

Here is concrete example of a Neurosymbolic programming framework using a proof assistant which is also a programming language (Rocq). All you have to do is drop this MCP in your opencode (or similar) coding framework and you can have LLMs write certifiably correct code. github.com/scidonia/mcp...

11 Dec 2025

At bookwyrm.ai we've been performing experiments in Neural-symbolic programming and we're getting amazing results. Generative AI driven by both specification and formal verification.

11 Dec 2025

Generative AI is finally making software verification not just practical, but it a requirement (pun intended). AI slop is a serious problem, but it is also an opportunity.