I’m starting a company that rebuilds enterprise software on algebraic specifications, and I’m looking for one or two technical co-founders.
The short version: the compliance plumbing every enterprise application needs (authentication, audit trails, traceability, data retention, GDPR, API and legacy-format interoperability) gets written once, as open-source formal specifications with generated, verified code. The domain logic on top of it stays proprietary and is sold as SaaS. The first customer is Divizend, a fintech I co-founded in 2020 whose withholding-tax software runs at more than 20,000 private clients and several large institutions, all the way up to the German stock exchange (Clearstream), Euroclear, BNY and Interactive Brokers.
The first milestone is concrete and six months out: Divizend’s audit, auth and data-retention layer, formally specified, with generated code in production. If that works, everything below becomes believable. If it doesn’t, we will have learned the key thing cheaply.
The problem
Every enterprise application in finance, tax and administration rebuilds the same non-functional requirements from scratch, and gets them subtly wrong. Role-based access, audit logs, data lineage, retention and deletion rules, consent handling, export to regulators’ formats: none of it is the product, all of it is where certifications, incidents and sales cycles are lost.
These requirements are also the part that is identical across products. An HR tool, an ERP, a tax-reclaim engine and a wealth-management portal all need the same guarantees, and today each vendor hand-writes them in TypeScript or Java and proves nothing about them beyond a test suite.
The buyers of this software (tax advisors, wealth managers, banks, family offices) don’t care about any of this. They want software that is fast, easy, reliable and, above all, demonstrably compliant. Those four properties are much cheaper to deliver when the compliance layer is specified once, verified once and reused everywhere.
The approach
Algebraic specification is a 40-year-old idea from Joseph Goguen’s OBJ family and the CASL and OMG DOL standards: describe a system as sorts, operations and equations, compose specifications like modules, and derive implementations that provably satisfy them. It never left academia because the tooling was hard to use and the business case was unclear. Both have changed. Proof assistants like Lean are usable by working engineers, and LLMs make writing and checking specifications dramatically cheaper.
The product splits into two layers with different licences:
Open specification layer (open source). Formal specifications of the non-functional requirements above, plus the toolchain that turns them into running code. Anyone can read them, audit them and build on them. This is where trust and adoption come from.
Proprietary domain layer (commercial). The actual business logic: tax rules, reporting frameworks, legal processes, the workflows of specific tools. This is where the revenue comes from, delivered as SaaS or through revenue sharing with partners who own the domain knowledge.
Technically the toolchain has three parts: a publisher that stores specifications in a language-agnostic format (CASL, DOL, Maude or similar), a translator that generates code for a functional host language (for example Haskell or Lean), and a runtime that executes the generated code and defines the effects it may have. Only the first two are needed for the Divizend milestone; the runtime follows once real workloads tell us what effects matter.
Commercially the long-run shape is a composable catalogue: compliant building blocks that a firm assembles into exactly the software it needs instead of stacking a dozen subscriptions. We get there by replicating existing tools closely enough that nobody has to learn new workflows, and pricing well under incumbents. We’re not inventing a market, we’re re-implementing one on a better foundation.
Customer zero: Divizend
Divizend does withholding-tax reclaims for institutional clients and runs today on an ordinary Next.js, MongoDB and Postgres stack. I’ve wanted to rebuild its foundation for a while; this is the reason to do it properly.
It is an unusually good first customer for three reasons:
Real compliance burden. Divizend is ISO 27001 and SOC 2 Type 2 certified. Those controls are a ready-made, externally audited list of the non-functional requirements the open layer has to satisfy.
Clean separation already exists. Divizend’s withholding-tax knowledge stays Divizend’s. The new company supplies the specified, generated infrastructure underneath it, as SaaS or with revenue sharing. That is exactly the open-layer / domain-layer split the whole thesis rests on.
Paying from day one. No pilot, no proof-of-concept purgatory, and production data from real institutions to validate against.
The six-month milestone: Divizend’s authentication, audit-trail and data-retention layer specified in an algebraic specification language, with generated code running in production behind at least one live customer flow, and the specification passing an external review against the SOC 2 control set.
What I bring, and who I’m looking for
I co-founded Divizend in 2020 and have taken it from zero through several international subsidiaries, so I’ve seen every stage of a regulated fintech: funding, hiring, certification, enterprise sales, and the long tail of keeping institutions happy. The software I built there processes withholding-tax reclaims for a large share of global cross-border dividend flows. I bring the customer, the domain, the distribution into banks and advisors, and the operating experience. I’m currently learning Lean and working through the algebraic-specification literature from scratch.
What I don’t bring is a decade in formal methods, and that is the first co-founder I’m looking for:
A formal-methods engineer. Someone who has shipped with Lean, Coq, Isabelle, Maude or similar outside a paper, has opinions about where algebraic specification breaks down in practice, and wants to build the translator layer. Previous exposure to CASL or Hets is a plus, not a requirement.
A functional-systems engineer. Someone who has run Haskell, OCaml or Scala in production, cares about effect systems and runtimes, and can own the generated-code path from specification to deployed service.
One person covering both is ideal; two who overlap is fine. Location is flexible, with a slight preference for the German-speaking region where Divizend and the first customers are. This is a founding role with equity, not a job, and the first six months are about the Divizend milestone and nothing else.
Longer term I believe this should become a federated company: one team per domain (for example German and Swiss tax, real estate, environmental compliance, HR tooling, Industry 4.0), all on the same open specification core. Whether that happens depends entirely on the core being stable first. It isn’t something I’m asking a co-founder to sign up for today.
Get in touch
If this is you, or you know who it is, write to me. Tell me what you’ve built with formal methods or functional systems, and what you think is wrong with the plan above. I’d rather start with the hardest objection than with a pitch.