Systems whose guarantees hold without trusting whoever runs them — or whatever built them.

Yak Software — independent engineering and research, Andorra.

Software is now cheap to write and increasingly acts on its own. The hard part is knowing what it may do, what it did, and which of those claims can be checked. Yak works on that in dictation, coding agents, consensus protocols and financial infrastructure.

Diane · today 09:370:28 · 2.1 s · GPU

Read the reports, check the patches, and try to figure out what might still be valuable from that, and put what you think yourself might still be useful later as a number of files in the same folder under shared, so we can pick it up later.

typed into Slack2 words contested · available → valuable

yak.ad/diane

Diane

Dictation of the highest quality, into any application on any device, that stays confidential. Three speech models transcribe the same audio on your own machine; a reconciler produces one clean text — and learns from your corrections.

builtmeasuredin daily use

agent-cage · relay1:42 PM

/agents1:42 PM ✓✓

cage-barecage-podetheron-pod

[cage-pod] cage-pod — running · up 122h
NOT LOGGED IN — send /auth
0 sessions · 10 processes
last command ran as the executor 8d ago1:43 PM

yak.ad/agent-cage

agent-cage

Run AI coding agents on your own servers, unattended, from a chat. Each agent gets exactly the permissions it needs and nothing more; the chat manages secrets and upgrades; every model runs in its maker’s own harness.

builtin active use · public release 1 October

Financial systems

yak.finance →

LedgerRecords that stay correct — and private — even when someone inside the company, human or AI, has access to every server. Seven independent operators, machine-checked consensus and zero-knowledge certificates, behind an integration surface shaped like a database driver.designedin development Molt PetitThe consensus protocol beneath Ledger: simple enough to explain in a minute, with deterministic fast finality, and a thorough treatment of rotated, stolen and briefly exposed keys as the distinct events they are. Safety is a machine-checked theorem.provenpreprint · machine-checked artifact

Research

thesis

Proof-driven developmentAI agents change the economics of formal verification: proof search and iteration become cheap, and the trust stays with the checker. For the parts of a system that must never fail, that shifts the work from tests that sample behaviour to properties proved about the artifact that ships. Molt Petit is the first example.more work intended

Consulting

limited capacity

Architecture, protocols and systems that need to keep workingYak Software works on distributed systems, networking, consensus, blockchain and cryptography, including zero-knowledge systems. Engagements range from architecture and technical leadership to building critical parts directly.Current work includes an ongoing engagement with o1Labs; earlier consulting included five years delivering projects for Serokell's clients.about the practice →