Extract an Allium specification from an existing codebase. Use when the user has existing code and wants to distil behaviour into a spec, reverse engineer a specification from implementation, generate a spec from code, turn implementation into a behavioural specification, or document what a codebase does in Allium terms.
This guide covers extracting Allium specifications from existing codebases. The core challenge is the same as forward elicitation: finding the right level of abstraction. In elicitation you filter out implementation ideas as they arise. In distillation you filter out implementation details that already exist. Both require the same judgement about what matters at the domain level.
Code tells you how something works. A specification captures what it does and why it matters. The skill is asking "why does the stakeholder care about this?" and "could this be different while still being the same system?"
Before diving into code, establish what you are trying to specify. Not every line of code deserves a place in the spec.
"What subset of this codebase are we specifying?" Mono repos often contain multiple distinct systems. You may only need a spec for one service or domain. Clarify boundaries explicitly before starting.
"Is there code we should deliberately exclude?"
"Who owns this spec?" Different teams may own different parts of a mono repo. Each team's spec should focus on their domain.
For any code path you encounter, ask: "If we rebuilt this system from scratch, would this be in the requirements?"
At the top of a distilled spec, document what is included and excluded:
-- allium: 3
-- interview-scheduling.allium
-- Scope: Interview scheduling flow only
-- Includes: Candidacy, Interview, InterviewSlot, Invitation, Feedback
-- Excludes:
-- - User authentication (use auth library spec)
-- - Analytics/reporting (separate spec)
-- - Legacy V1 API (deprecated, not specified)
-- - Greenhouse sync (use greenhouse library spec)
The version marker (-- allium: N) must be the first line of every .allium file. Use the current language version number.
Distillation and elicitation share the same fundamental challenge: choosing what to include. The tests below work in both directions, whether you are hearing a stakeholder describe a feature or reading code that implements it.
For every detail in the code, ask: "Why does the stakeholder care about this?"
| Code detail | Why? | Include? |
|---|---|---|
| Invitation expires in 7 days | Affects candidate experience | Yes |
| Token is 32 bytes URL-safe | Security implementation | No |
| Sessions stored in Redis | Performance choice | No |
| Uses PostgreSQL JSONB | Database implementation | No |
| Slot status changes to 'proposed' | Affects what candidate sees | Yes |
| Email sent when invitation accepted | Communication requirement | Yes |
If you cannot articulate why a stakeholder would care, it is probably implementation.
Ask: "Could this be implemented differently while still being the same system?"
| Detail | Could be different? | Include? |
|---|---|---|
secrets.token_urlsafe(32) | Yes, any secure token generation | No |
| 7-day invitation expiry | No, this is the design decision | Yes |
| PostgreSQL database | Yes, any database | No |
| "Pending, Confirmed, Completed" states | No, this is the workflow | Yes |
Is this a category of thing, or a specific instance?
| Instance (often implementation) | Template (often domain-level) |
|---|---|
| Google OAuth | Authentication provider |
| Slack webhook | Notification channel |
| SendGrid API | Email delivery |
timedelta(hours=3) | Confirmation deadline |
Sometimes the instance IS the domain concern. See "The concrete detail problem" below.
Every line of code makes decisions that might not matter at the domain level:
# Code tells you:
def send_invitation(candidate_id: int, slot_ids: List[int]) -> Invitation:
candidate = db.session.query(Candidate).get(candidate_id)
slots = db.session.query(InterviewSlot).filter(
InterviewSlot.id.in_(slot_ids),
InterviewSlot.status == 'confirmed'
).all()
invitation = Invitation(
candidate_id=candidate_id,
token=secrets.token_urlsafe(32),
expires_at=datetime.utcnow() + timedelta(days=7),
status='pending'
)
db.session.add(invitation)
for slot in slots:
slot.status = 'proposed'
invitation.slots.append(slot)
db.session.commit()
send_email(
to=candidate.email,
template='interview_invitation',
context={'invitation': invitation, 'slots': slots}
)
return invitation
-- Specification should say:
rule SendInvitation {
when: SendInvitation(candidacy, slots)
requires: slots.all(s => s.status = confirmed)
ensures:
for s in slots:
s.status = proposed
ensures: Invitation.created(
candidacy: candidacy,
slots: slots,
expires_at: now + 7.days,
status: pending
)
ensures: Email.created(
to: candidacy.candidate.email,
template: interview_invitation
)
}
What we dropped:
candidate_id: int became just candidacydb.session.query(...) became relationship traversalsecrets.token_urlsafe(32) removed entirely (token is implementation)datetime.utcnow() + timedelta(...) became now + 7.daysdb.session.add/commit implied by createdinvitation.slots.append(slot) implied by relationshipFor every detail in the code, ask:
| Code detail | Product owner cares? | Include? |
|---|---|---|
| Invitation expires in 7 days | Yes, affects candidate experience | Yes |
| Token is 32 bytes URL-safe | No, security implementation | No |
| Uses SQLAlchemy ORM | No, persistence mechanism | No |
| Email template name | Maybe, if templates are design decisions | Maybe |
| Slot status changes to 'proposed' | Yes, affects what candidate sees | Yes |
| Database transaction commits | No, implementation detail | No |
Means: how the code achieves something. Ends: what outcome the system needs.
| Means (code) | Ends (spec) |
|---|---|
requests.post('https://slack.com/api/...') | Notification.created(channel: slack) |
candidate.oauth_token = google.exchange(code) | Candidate authenticated |
redis.setex(f'session:{id}', 86400, data) | Session.created(expires: 24.hours) |
for slot in slots: slot.status = 'cancelled' | for s in slots: s.status = cancelled |
The hardest judgement call: when is a concrete detail part of the domain vs just implementation?
You find this code:
OAUTH_PROVIDERS = {
'google': GoogleOAuthProvider(client_id=..., client_secret=...),
}
def authenticate(provider: str, code: str) -> User:
return OAUTH_PROVIDERS[provider].authenticate(code)
Question: Is "Google OAuth" domain-level or implementation?
It is implementation if:
It is domain-level if:
How to tell: Look at the UI and user flows. If users see "Sign in with Google" as a choice, it is domain-level. If they just see "Sign in" and Google happens to be behind it, it is implementation.
You find PostgreSQL-specific code:
from sqlalchemy.dialects.postgresql import JSONB, ARRAY
class Candidate(Base):
skills = Column(ARRAY(String))
metadata = Column(JSONB)
Almost always implementation. The spec should say:
entity Candidate {
skills: Set<String>
metadata: String? -- or model specific fields
}
The specific database is rarely domain-level. Exception: if the system explicitly promises PostgreSQL compatibility or specific PostgreSQL features to users.
You find Greenhouse ATS integration:
class GreenhouseSync:
def import_candidate(self, greenhouse_id: str) -> Candidate:
data = self.client.get_candidate(greenhouse_id)
return Candidate(
name=data['name'],
email=data['email'],
greenhouse_id=greenhouse_id,
source='greenhouse'
)
Could be either:
Implementation if:
Spec:
external entity Candidate {
name: String
email: String
source: CandidateSource
}
Product-level if:
Spec:
external entity Candidate {
name: String
email: String
greenhouse_id: String? -- explicitly modeled
}
rule SyncFromGreenhouse {
when: GreenhouseWebhookReceived(candidate_data)
ensures: Candidate.created(
...
greenhouse_id: candidate_data.id
)
}
Look for variation in the codebase:
The presence of multiple implementations suggests the variation itself is a domain concern.
Before extracting any specification, understand the codebase structure:
models/, entities/, domain/.Create a rough map:
Entry points:
- API: /api/candidates/*, /api/interviews/*, /api/invitations/*
- Webhooks: /webhooks/greenhouse, /webhooks/calendar
- Jobs: send_reminders, expire_invitations, sync_calendars
Models:
- Candidate, Interview, InterviewSlot, Invitation, Feedback
Services:
- SchedulingService, NotificationService, CalendarService
Integrations:
- Google Calendar, Slack, Greenhouse, SendGrid
Look at enum fields and status columns:
class Invitation(Base):
status = Column(Enum('pending', 'accepted', 'declined', 'expired'))
Becomes:
entity Invitation {
status: pending | accepted | declined | expired
}
Look for enum definitions, status or state columns, constants like STATUS_PENDING = 'pending', and state machine libraries (e.g. transitions, django-fsm).
Find where status changes happen:
def accept_invitation(invitation_id: int, slot_id: int):
invitation = get_invitation(invitation_id)
if invitation.status != 'pending':
raise InvalidStateError()
if invitation.expires_at < datetime.utcnow():
raise ExpiredError()
slot = get_slot(slot_id)
if slot not in invitation.slots:
raise InvalidSlotError()
invitation.status = 'accepted'
slot.status = 'booked'
# Release other slots
for other_slot in invitation.slots:
if other_slot.id != slot_id:
other_slot.status = 'available'
# Create the interview
interview = Interview(
candidate_id=invitation.candidate_id,
slot_id=slot_id,
status='scheduled'
)
notify_interviewers(interview)
send_confirmation_email(invitation.candidate, interview)
Extract:
rule CandidateAcceptsInvitation {
when: CandidateAccepts(invitation, slot)
requires: invitation.status = pending
requires: invitation.expires_at > now
requires: slot in invitation.slots
ensures: invitation.status = accepted
ensures: slot.status = booked
ensures:
for s in invitation.slots:
if s != slot: s.status = available
ensures: Interview.created(
candidacy: invitation.candidacy,
slot: slot,
status: scheduled
)
ensures: Notification.created(to: slot.interviewers, ...)
ensures: Email.created(to: invitation.candidate.email, ...)
}
Key extraction patterns:
| Code pattern | Spec pattern |
|---|---|
if x.status != 'pending': raise | requires: x.status = pending |
if x.expires_at < now: raise | requires: x.expires_at > now |
if item not in collection: raise | requires: item in collection |
x.status = 'accepted' | ensures: x.status = accepted |
Model.create(...) | ensures: Model.created(...) |
send_email(...) | ensures: Email.created(...) |
notify(...) | ensures: Notification.created(...) |
Assertions, checks and validations found in code (e.g. assert balance >= 0, class-level validators) may map to expression-bearing invariants rather than rule preconditions. Consider whether they describe a system-wide property or a rule-specific guard.
Look for scheduled jobs and time-based logic:
# In celery tasks or cron jobs
@app.task
def expire_invitations():
expired = Invitation.query.filter(
Invitation.status == 'pending',
Invitation.expires_at < datetime.utcnow()
).all()
for invitation in expired:
invitation.status = 'expired'
for slot in invitation.slots:
slot.status = 'available'
notify_candidate_expired(invitation)
@app.task
def send_reminders():
upcoming = Interview.query.filter(
Interview.status == 'scheduled',
Interview.slot.time.between(
datetime.utcnow() + timedelta(hours=1),
datetime.utcnow() + timedelta(hours=2)
)
).all()
for interview in upcoming:
send_reminder_notification(interview)
Extract:
rule InvitationExpires {
when: invitation: Invitation.expires_at <= now
requires: invitation.status = pending
ensures: invitation.status = expired
ensures:
for s in invitation.slots:
s.status = available
ensures: CandidateInformed(candidate: invitation.candidate, about: invitation_expired)
}
rule InterviewReminder {
when: interview: Interview.slot.time - 1.hour <= now
requires: interview.status = scheduled
ensures: Notification.created(to: interview.interviewers, template: reminder)
}
Look for third-party API calls, webhook handlers, import/export functions, and data that is read but never written (or vice versa).
These often indicate external entities:
# Candidate data comes from Greenhouse, we don't create it
def import_from_greenhouse(webhook_data):
candidate = Candidate.query.filter_by(
greenhouse_id=webhook_data['id']
).first()
if not candidate:
candidate = Candidate(greenhouse_id=webhook_data['id'])
candidate.name = webhook_data['name']
candidate.email = webhook_data['email']
Suggests:
external entity Candidate {
name: String
email: String
}
When repeated interface patterns appear across service boundaries (e.g. the same serialisation contract expected by multiple consumers), these suggest contract declarations for reuse rather than duplicated inline obligation blocks.
Now make a pass through your extracted spec and remove implementation details.
Before (too concrete):
entity Invitation {
candidate_id: Integer
token: String(32)
created_at: DateTime
expires_at: DateTime
status: pending | accepted | declined | expired
}
After (domain-level):
entity Invitation {
candidacy: Candidacy
created_at: Timestamp
expires_at: Timestamp
status: pending | accepted | declined | expired
is_expired: expires_at <= now
}
Changes:
candidate_id: Integer became candidacy: Candidacy (relationship, not FK)token: String(32) removed (implementation)DateTime became Timestamp (domain type)is_expired for clarityConfig values that derive from other config values (e.g. extended_timeout = base_timeout * 2) should use qualified references or expression-form defaults in the config block rather than independent literal values.
The extracted spec is a hypothesis. Validate it:
Common findings:
During distillation, stay alert for code that implements generic integration patterns rather than application-specific logic. These belong in library specs, not your main specification.
The same principle applies in elicitation. When a stakeholder describes "we use Google for login" or "payments go through Stripe", pause and consider whether this is a library spec.
Third-party integration modules:
# Finding code like this suggests a library spec
class StripeWebhookHandler:
def handle_invoice_paid(self, event):
...
def handle_subscription_cancelled(self, event):
...
class GoogleOAuthProvider:
def exchange_code(self, code):
...
def refresh_token(self, refresh_token):
...
Generic patterns with specific providers:
Configuration-driven integrations:
# Heavy configuration suggests the integration itself is separable
OAUTH_CONFIG = {
'google': {'client_id': ..., 'scopes': ...},
'microsoft': {'client_id': ..., 'scopes': ...},
}
"Is this integration logic, or application logic?" Integration: how to talk to Stripe. Application: what to do when payment succeeds.
"Would another application integrate the same way?" If yes, library spec candidate. If no, probably application-specific.
"Does the code separate integration from application concerns?" If cleanly separated, easy to extract to library spec. If tangled, might need refactoring first (but the spec should still separate them).
Option 1: Reference an existing library spec
If a standard library spec exists for this integration:
use "github.com/allium-specs/stripe-billing/abc123" as stripe
-- Application responds to Stripe events
rule ActivateSubscription {
when: stripe/PaymentSucceeded(invoice)
...
}
Option 2: Create a separate library spec
If no standard spec exists but the integration is generic:
-- greenhouse-ats.allium (library spec)
-- Specifies: Greenhouse webhook events, candidate sync, etc.
-- interview-scheduling.allium (application spec)
use "./greenhouse-ats.allium" as greenhouse
rule ImportCandidate {
when: greenhouse/CandidateCreated(data)
ensures: Candidacy.created(...)
}
Option 3: Abstract and move on
If the integration is minor, just abstract it:
-- Don't specify Slack details, just: